Hi,
I know that when executing a condition statement like if(a[1] == 0), KLEE
updates the path constraint of the true branch by adding constraint a[1] == 0
(for false branch it is a[1] != 0) to it.
But how about others like assigning statements and so on, e.g., a[2] = b(where
b is symbolic variable, so is a)?
After KLEE executes this statement, will it add constraint a[2] == b to the
path constraint?
For more complicated example, consider following code:
int main() {
char a[2], b[5];
klee_make_symbolic(a, 2, "a");
klee_make_symbolic(b, 5, "b");
if(b[1] == 0 && a[1] == 0) {
strcat(b, a);
strcpy(a, b);
}
return 0;
}
After executing strcat(b, a), will the constraint on b be updated? Say, in this
situation, b[2] == 0.
Thanks,
Yongchao Li._______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
