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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
