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

[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

Post by 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);
}
--------------------------------------------------
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev