[prev in list] [next in list] [prev in thread] [next in thread] 

List:       klee-dev
Subject:    Re: [klee-dev] Constant array declarations for klee_print_expr
From:       Cristian Cadar <c.cadar () imperial ! ac ! uk>
Date:       2017-04-27 12:45:22
Message-ID: cb750fb1-4bfa-44d0-0574-028fc339eaa6 () imperial ! ac ! uk
[Download RAW message or body]

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
[prev in list] [next in list] [prev in thread] [next in thread]