Hello All,
I am trying to add a new search algorithm, so that the states where a certain
variable change happens are selected for exploration over the others, and only
fall back to the BFS/DFS when this given criteria does not exist in any of the
possible states. For example, in this code I would like to select the path with
`a > 0`, since `b` is changing in that path and stop exploring the `else`
branch:
```
int main() {
int a;
klee_make_symbolic(&a, sizeof(a), “a”);
int b = 0;
klee_subscribe_changing(&b, …, “b”);
if (a > 0) {
b++;
.
.
.
} else {
a++;
.
.
.
}
return 0;
}
```
I have already tried creating a vector of subscribed MemoryObjects in the
ExecutionState class (similar to symbolics), but I have not been able to find a
way to mark changes. I would appreciate it if anyone could tell me how I can
mark these value changes (and more generally how I should approach this
problem).
Thank you for your help.
Sincerely Yours,
Hossein_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
