[klee-dev] Constant array declarations for klee_print_expr

David Andrews dandrews at cs.queensu.ca
Tue Apr 18 19:00:28 BST 2017


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.



More information about the klee-dev mailing list