[klee-dev] How to get the the trace from the symbolic execution process?

[Paul Marinescu]

Hello AK,
You can use klee-replay and gcov, as explained in the KLEE tutorial at http://klee.llvm.org/TestingCoreutils.html (step 6).

Paul

On 29 Mar 2013, at 12:44, General Email wrote:

> I'm interested in is the value returned as the result from the execution process. For example if I have the following small program
> --------------------------------------------------
> int globalVar1=100;
> char* globalVar2="";
> void myFunction(int k) {
>    if (k > 0)
>   {
>     globalVar1 = k;
>     globalVar2 = "Message1";
>   }
>   else
>   {
>     globalVar2 = "Message2";
>   }
> } 
> 
> int main() {
>   int k;
>   klee_make_symbolic(&k, sizeof(k), "k");
>   get_sign(k);
> }
> --------------------------------------------------
> With klee I got the following two paths, each of which has to satisfy one of the following constraints:
> 1)
> array k[4] : w32 -> w8 = symbolic
> (query [(Eq false
>             (Slt 0
>                  (ReadLSB w32 0 k)))]
>        false)
> 
> 2)
> array k[4] : w32 -> w8 = symbolic
> (query [(Slt 0
>              (ReadLSB w32 0 k))]
>        false)
> 
> 
> How can I get the symbolic statements associated with each path. For instance I need to know that in the second path, globalVar1 and globalVar2 are changed respectively to "some symbolic value" and "Message1".
> 
>  
> Any suggestions?
> Thanks
> AK
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed