[klee-dev] how to get this constraint in klee

[Andrew Santosa]

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 <sumit686215 at gmail.com> 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
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


  
-------------- next part --------------
HTML attachment scrubbed and removed