[klee-dev] Adding assignments to state constraints

[Kuchta, Tomasz]

Hi Felicia,

Why would you like to add assignments to the constraints?
What do you want to achieve?
In your example, if ‘x' is later on present in a branch condition, e.g. if (x < 5) , the symbolic expression that you quote
will be incorporated in the condition instead of ‘x’. As a result you should end up with having something like
(Add w32 1 (ReadLSB w32 0 x)) < 5 added to your constraint set (on the “then” side of the branch).

Kind regards,

Tomek


> On 4 Nov 2015, at 08:18, felicia <felicia at comp.nus.edu.sg> wrote:
> 
> Hi,
> 
> I would like to ask on how to collect assignments in the state's constraints.
> Because currently KLEE only collect the constraints at the branch condition.
> I have tried to add the assignment expression in the state constraints.
> For example, x = x + 1 has assignment expression like this (Add w32 1 (ReadLSB w32 0 x)).
> Then, I add (Add w32 1 (ReadLSB w32 0 x)) at state constraints.
> However, this way always give me an assertion error.Please let me know if you have any suggestion regarding this.
> 
> Thank you.
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 4267 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20151104/6c72880c/attachment.bin>