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
