Hi Tareq, I can highly recommend you the following documents to get an understanding of the internal details of debug information and LLVM that KLEE uses in the first place: * https://llvm.org/docs/SourceLevelDebugging.html * https://llvm.org/docs/HowToUpdateDebugInfo.html
For the examples that you asked for, a good starting point for me are often the transformation passes of LLVM, i.e. (llvm-project/llvm/lib/Transforms/) to get an idea how different concepts are implemented and might work. (Just one example: https://github.com/llvm/llvm-project/blob/53dc0f107877acad44824b1426986c7f88f4bc50/llvm/lib/Transforms/IPO/MergeFunctions.cpp#L566) A good IDE support makes a huge difference in working through the source code and makes it slightly less painful. Best, Martin > On 5. Oct 2022, at 20:58, Nazir, Tareq Mohammed <tareq.na...@aau.at> wrote: > > 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 _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
