Hi David, you are right, klee_print_expr does not include declarations.
You would need to extend its implementation to accomplish this, or rely
solely on the self-contained .pc/.kquery files.
Best,
Cristian
On 18/04/17 19:00, David Andrews wrote:
Hello all,
My question is with regard to our KLEE-related project here at Queen's.
Please excuse me if this has been answered before. I am fairly new to KLEE.
Our project makes use of the results of the "klee_print_expr" intrinsic
and ".pc" files. This works well when the data is scalar and for the
".pc" files in more general cases. However, the output of
"klee_print_expr" does not include the declarations of the array
constants that appear in "versions".
Without the the array constant definitions the output of
"klee_print_expr" appears to be ambiguous.
Is there a way to each associate output with the corresponding constant
set of declarations?
Thanks!
David.
_______________________________________________
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
