[klee-dev] Regarding getting variable names from KLEE

[J. Ryan Stinnett]

On Wed, 5 Oct 2022 at 14:10, Nazir, Tareq Mohammed <Tareq.Nazir at aau.at> wrote:
> Yes I would be needing the source-level variable names and source-level info. We are currently trying to understand the vulnerabilities such as heap overflow that can be present in the source code. We are able to understand the how KLEE engine is able to detect a vulnerability. But we need a map between the information available to us from Memory space of KLEE to the source code. It would be really helpful if I can get this map between the KLEE memory space and source code.

Makes sense, thanks for the additional detail. This sounds like my
in-progress enhancement should indeed help you follow source-level
state.

As Frank mentioned elsewhere in the thread, you may be able to use
`-fno-discard-value-names` as a workaround for the moment, but that
doesn't encode any of the source-level semantics that e.g. a debugger
would follow; for proper source-level info, KLEE needs to make use of
the debug info when present in the IR.

I did not see any existing issues about this in the KLEE repo, so I
have filed one just now (https://github.com/klee/klee/issues/1552). We
can use that issue to gauge interest in this enhancement and discuss
any finer details as needed.

Thanks,
Ryan