[klee-dev] Tracking changes of specific variables

[Hossein Monjezi]

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
-------------- next part --------------
HTML attachment scrubbed and removed