On Wed, 5 Oct 2022 at 10:28, Nazir, Tareq Mohammed <tareq.na...@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 _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
