[klee-dev] Regarding getting variable names from KLEE

[J. Ryan Stinnett]

On Wed, 5 Oct 2022 at 10:28, Nazir, Tareq Mohammed <Tareq.Nazir at aau.at> wrote:
> I would like to know if I can get variable names of the source code in KLEE engine. Would also like to know if KLEE engine is storing the variable name information while executing the llvm bitcode symbolically.

KLEE currently thinks in terms of names at the LLVM IR level only, so
this means it does not know about source-level local variables such as
`buffer` in your example.

When you compile with debug info enabled (e.g. the `-g` option with
Clang), the IR does include additional DWARF-like metadata that maps
back to source-level concepts. My current research involves using KLEE
to test this debug info, and as part of that work, I've been enhancing
KLEE so that it can think in terms of source-level info using this
metadata. I hope to eventually add this enhancement to upstream KLEE,
but it may be a few months before I can do so.

It sounds like this enhancement would be useful to you as well. Do you
need only the source-level variable names, or other source-level info
as well?

- Ryan