Hi,
I am confused about how the symbolic variables are stored with constraints in
memory. For example, we have the following program:
int sum(int a, int b, int c) {
if(a == b - 6){
return a + b - c;
}
else if(c == a - b + 1){
return a + b + c;
}
else{
return a + b + c + 1;
}
}
int main() {
int a, b, c;
klee_make_symbolic(&a, sizeof(a), "x");
klee_make_symbolic(&b, sizeof(b), "y");
klee_make_symbolic(&c, sizeof(c), "z");
sum(a, b, c);
return 0;
}
So for the executionState of first branch where a == b-6, the symbolic
variable a should be x0, and b should be x0 + 6. So for symbolic variable "y",
does klee store y's symbolic value y0 as x0 + 6 in memoryObject? Or it just
stores y0, separately with the constraints?
I am able to print the constraints out at the end of each execution, but I
still want to print the symbolic variables with their symbolic values, such as
a==x0, b==x0+6, c==z0. So I want to know if executionState stores the relations
of symbolic values in memory. I think the solver deals with the relations in
the end before generating test cases, but I am not sure.
What I want to print for the first branch is:
constraints: a == b - 6
symbolic values: a==x0, b==x0+6, c==z0
We can take the picture for example. I want to know if memoryObject stores
information like in the table such as X: α1+α2
Thank you very much!
Best,
Zhongqiu Gao_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
