k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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

From: <daparpon AT dsic.upv.es>
To: k-user AT lists.cs.illinois.edu,msaxena2 AT illinois.edu
Subject: Re: [[K-user] ] --pattern parameter
Date: Thu, 16 Feb 2017 06:09:19 -0600

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