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

[Cristian Cadar]

Hi Seemanta,

Since you didn't include a full program, it's not clear what you want to 
do exactly.  But at a higher level, note that KLEE is not a concolic 
execution engine, although it has some concolic execution features. 
However, it uses a counterexample cache, so you could adapt the code 
from there to retrieve concrete values.

Best,
Cristian

On 03/11/2020 16:29, Seemanta Saha wrote:
> 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
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>