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
