[klee-dev] Regarding getting variable names from KLEE

[Nazir, Tareq Mohammed]

Hi Frank,


Thanks for the reply,


Yes I have used the second option and -fno-discard-value-names and I am able to see the variable name in the llvm bitcode .ll file. But what I need is the access to this variables in KLEE engine. Also I am trying to use DILocalVariable. I would like to know if it is possible to share any example where DILocalVariable can be used to extract the variable name. This would be really helpful.


Thanks and Best Regards,

Tareq Mohammed Nazir

________________________________
From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of Frank Busse <f.busse at imperial.ac.uk>
Sent: Wednesday, 5 October 2022 13:05
Cc: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Regarding getting variable names from KLEE

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

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed