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

[General Email]

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
-------------- next part --------------
HTML attachment scrubbed and removed