[klee-dev] Question about KLEE Implementation on Collecting Symbolic Variables

[Nowack, Martin]

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