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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
