[klee-dev] Constant array declarations for klee_print_expr

[Cristian Cadar]

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