Hi Ridwan,
I think you can do this using klee_print_expr() without modifying KLEE.For
example (from [klee-dev] question about klee_print_expr):
|
|
| |
[klee-dev] question about klee_print_expr
|
|
|
#include <klee/klee.h>
int main(int arc, char **argv)
{
int a,b;
klee_make_symbolic(&a,sizeof(a),"a");
if(a>0)
b=a+10;
else
b=-a+10;
klee_print_expr("b=",b);
return 0;
}
Running KLEE with this program as input gives you the following output:
$ klee example.bc
KLEE: output directory is "/home/dcsandr/projects/klee/klee-out-0"
KLEE: Using STP solver backend
b=:(Add w32 10
(ReadLSB w32 0 a))
b=:(Sub w32 10
(ReadLSB w32 0 a))
KLEE: done: total instructions = 27
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2
Each printed value of b represetns the valueof b at the end of one of the two
execution paths.
I hope that helps.
Best,Andrew
On Thursday, 31 May 2018, 2:30:03 PM SGT, Ridwan Shariffdeen
<[email protected]> wrote:
Hi
I want to obtain the symbolic expression for a given variable at the end of an
execution of a program. Is this possible with the current implementation? or do
I need to modify klee for this? If so can you point out in which direction I
should look into?
Appreciate any help in this regards
Thanks!Ridwan
_______________________________________________
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
