[klee-dev] Regarding getting variable names from KLEE

[Frank Busse]

Hi,


On Wed, 5 Oct 2022 09:26:35 +0000
"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.
> 
> 
> For example : From the below C code I want to get the buffer variable
> name is it possible or not.
> 
> 
> int main(int argc, char *argv[])
> {
>        char *buffer = malloc(5);
>        buffer[6] = 'a';
>        return 0;
> }

There are at least two options:

1) you compile your code with debug information (-g) and recover the
   information from there (LLVM API):

!15 = !DILocalVariable(name: "buffer", scope: !10, file: !1, line: 4, type: !16)

2) or you tell clang to keep variable names (-fno-discard-value-names)
   and it will generate bitcode like:

%buffer = alloca i8*, align 8
store i8* %call, i8** %buffer, align 8
%0 = load i8*, i8** %buffer, align 8

   instead of:

%2 = alloca i8*, align 8
store i8* %3, i8** %2, align 8
%4 = load i8*, i8** %2, align 8


Kind regards,

Frank