[klee-dev] Collect functions and values of parameters

Loi Luu loi.luuthe at gmail.com
Tue Oct 29 02:20:27 GMT 2013


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 <
david.lightstone at prodigy.net> 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 <david.lightstone at prodigy.net>;
> * To: * Loi Luu <loi.luuthe at gmail.com>; <klee-dev at imperial.ac.uk>;
> * 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 <loi.luuthe at gmail.com>;
> * To: * klee-dev <klee-dev at imperial.ac.uk>;
> * 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 <loi.luuthe at gmail.com> 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
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list