[klee-dev] Retrieve concrete values of variables from an execution path

[Seemanta Saha]

Hello,



Need help to retrieve concrete values of variables from an execution path.



I can retrieve information like path constraint, number of instructions
stepped for a symbolic path using the ExecutionState class. Is it possible
to retrieve concrete values of variables of an execution state using the
ExecutionState class?



For example, Consider this following program:

int base = 8;

int checked_copy (unsigned int i ) {

int v;

if ( i < 16)

v = base + i ;

else

v = base;

return v;

}





If I execute this program symbolically, I am going to get 17 path
constraints but 16 distinct values for v (8 to 23). When symbolically
executing, value of v will be represented as a symbolic expression and all
I can retrieve is the path constraint. But, I want to retrieve the concrete
values for v for each execution path. How can I do that?





Regards

Seemanta


-- 
Regards
Seemanta Saha
Verification Lab (V-Lab)
University of California Santa Barbara
-------------- next part --------------
HTML attachment scrubbed and removed