k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

Re: [[K-user] ] --pattern parameter

From: "Saxena, Manasvi" <msaxena2 AT illinois.edu>
To: "daparpon AT dsic.upv.es" <daparpon AT dsic.upv.es>
Cc: "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
Subject: Re: [[K-user] ] --pattern parameter
Date: Thu, 16 Feb 2017 12:26:58 +0000
Accept-language: en-US

Hi Daniel,

This may be occurring if you’re not on the latest version of K. Can you try
building the latest version from the repository, and see if it fixes the
issue?

Manasvi
> On Feb 16, 2017, at 6:09 AM,
> daparpon AT dsic.upv.es
> wrote:
>
> Hi, Manasvi. I tried to replicate your example to see how symbolic execution
> in K 4.0 works, but I cannot get the constraints of the final states to
> appear. I mean, with the same specification you propose, I get the following
> results:
>
> Search results:
>
> Solution 1:
> <k> "negative" </k>
>
> Solution 2:
> <k> "positive" </k>
>
> Is there something more that I have to do in order to make visible the path
> condition associated to each state?
>
> Thanks in advance,
> Daniel

[[K-user] ] --pattern parameter, Alex, 02/14/2017
- Re: [[K-user] ] --pattern parameter, Saxena, Manasvi, 02/14/2017
  - Re: [[K-user] ] --pattern parameter, Alex, 02/14/2017
    - Re: [[K-user] ] --pattern parameter, Saxena, Manasvi, 02/14/2017
      - Re: [[K-user] ] --pattern parameter, Dorel Lucanu, 02/15/2017
        
        Re: [[K-user] ] --pattern parameter, Alex, 02/15/2017
      - Re: [[K-user] ] --pattern parameter, daparpon, 02/16/2017
        
        Re: [[K-user] ] --pattern parameter, Saxena, Manasvi, 02/16/2017
        
        Re: [[K-user] ] --pattern parameter, daparpon, 02/17/2017
        
        Re: [[K-user] ] --pattern parameter, Saxena, Manasvi, 02/17/2017