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-boun...@imperial.ac.uk <klee-dev-boun...@imperial.ac.uk> on
behalf of Frank Busse <f.bu...@imperial.ac.uk>
Sent: Wednesday, 5 October 2022 13:05
Cc: klee-dev@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.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.
>
>
> 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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
