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 <feli...@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@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
