Does KLEE update constraints only at condition statements?

[李永超]

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.