I think you can't.In KLEE, each state is represented as a mapping of program
variables to an expression in terms of initial symbolic values.This is probably
better in terms of performance as the number of program variables is likely to
be smaller than the length of the path. Storingthe transition relation induced
by statements as you propose requires storage of size approximately the length
of the execution path. Butothers who developed KLEE would know better I presume.
I'm working on a somewhat "stateful" version of KLEE where I have to use
strongest postconditions from significant intermediate points alongan execution
path to compute program states (the variable mappings) to be stored as states,
and I need the dataflow dependency (some abstractform of transition relation).
For this, at the moment I go down into LLVM IR level to retrieve the
information.
Andrew
On Thursday, 17 March 2016, 23:36, Sumit Kumar <[email protected]>
wrote:
Hi,
Can anyone please help me. This is what I want to do in KLEE:
'x', 'y' are integer symbolic variables. Now the following statement is
executed:
x = y;
If after this statement any constraint in KLEE involves x then the value of x
is taken as:
"ReadLSB w32 0 y"
but I want that the constraint must be "ReadLSB w32 0 x". How can I do that ?
--
Thanks and Regards
Sumit
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
