Hi Martin,
Thanks for the quick response. Our question was slightly different, let
me clarify. Given an instance of the Expr object, we want to obtain the
set of symbolic names used in that instance. ExprPPrinter does it, for
example, but in a very specific way and, frankly, we struggled to
understand how it works. We were wondering if there is a generic way to
do it. I was expecting a visitor in the Expr hierarchy, or something
similar, but could not find it.
Thanks again,
Oleg
On 12/12/23 05:42, Nowack, Martin wrote:
Hi Haozhi Fan,
The symbolic names are generated using the call `klee_make_symbolic` indirectly
or directly in your software under test.
KLEE tracks the memory object that have been associated with these calls
(https://github.com/klee/klee/blob/fc83f06b17221bf5ef20e30d9da1ccff927beb17/lib/Core/Executor.cpp*L4435)
and assigns it an array that has the same name or similar name that is unique.
Reading from this memory will result in read expressions that reference this
array and are later used as part of the solver calls.
Best,
Martin
On 11. Dec 2023, at 20:07, Haozhi Fan <h3...@seas.upenn.edu> wrote:
Dear klee-dev members,
I was wondering if you could share some insight into how KLEE collects the set
of symbolic names from an expression? Namely, how does KLEE generate the kquery
for a specific path condition and from which files should I be looking for the
details of such implementation? Thank you!
Best regards,
Haozhi Fan
_______________________________________________
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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
