Thank you David. Are we able to query the values of parameters in each function call by KLEE? Using the line numbers generated by KLEE to identify the invokes tree is easy, but to get the parameter values parsed into each function I'm not sure.
Regards, On Tue, Oct 29, 2013 at 2:29 AM, DAVID LIGHTSTONE < [email protected]> wrote: > Sorry, I used the wrong nomenclature > > It's not a call tree, rather it is the tree created when Klee invokes fork > > ------------------------------ > * From: * DAVID LIGHTSTONE <[email protected]>; > * To: * Loi Luu <[email protected]>; <[email protected]>; > * Subject: * Re: [klee-dev] Collect functions and values of parameters > * Sent: * Mon, Oct 28, 2013 6:01:09 PM > > Take a look at your favorite debugger. Ask the question - how does it > figure the call tree? > > When KLEE writes out the test case, walk the call tree in the same fashion > as the debugger until you get to main. > > You probably need a debug version of the code to get the symbols needed to > play this game, but it should work. Use the line numbers to identify the > branch locations, there may not be symbols at those locations > > Dave Lightstone > > ------------------------------ > * From: * Loi Luu <[email protected]>; > * To: * klee-dev <[email protected]>; > * Subject: * Re: [klee-dev] Collect functions and values of parameters > * Sent: * Mon, Oct 28, 2013 4:34:20 PM > > I posted this question on StackOverflow with an illustrating example > http://stackoverflow.com/questions/19634022/program-analysis-with-given-input > > Thanks, > > > On Mon, Oct 28, 2013 at 6:54 PM, Loi Luu <[email protected]> wrote: > >> Hi, >> >> Given a program path, I wanna track all libc functions (in path >> condition) with their corresponding parameters in each execution path. For >> example, given the branch condition if (strcmp(s, s1)) in which s is >> symbolic, s1 is concrete; I wanna get the function name (strcmp), the value >> of s1 and the return value of this function. Which part of KLEE should I >> modify to get it stored in each execution state and printed in somewhere >> like .pc file. >> >> Thanks, >> >> -- >> Loi, Luu The (Mr.) >> RA at Security Lab, SoC, NUS >> > > > > -- > Loi, Luu The (Mr.) > RA at Security Lab, SoC, NUS > -- Loi, Luu The (Mr.) RA at Security Lab, SoC, NUS
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
