[klee-dev] Direct Search Towards Assertion

[Kirill Bogdanov]

Hello everyone.

I have a simple example, with the list of symbolic integers, and I am
searching for the smallest one. At the end of the code I am checking if
element at position [3] was the smallest one, and assert.
code:

#define n 10
int main() {

int a[n];
klee_make_symbolic(&a, sizeof(a), "a");

int index = 0;
for (int i = 1; i<n;i++){
if (a[i] < a[index])
index = i;

}
printf("index: %i\n", index);

if (index == 3){
klee_assert(false);
}

return 0;
}

I am running with "-search=dfs" argument. In this example KLEE generates
2^(n-1) code paths in the for loop by trying all different combinations of
input data.

Question: I do not really care to cover all possible code paths in the for
loop, I only care that the smallest element is not at position=3. I expect
this assertion to produce constrain something like: a[3] < a[0] && a[3] <
a[1] etc. Which should be easy to resolve.
How can I "ask" KLEE to try to trigger this assertion as quick as possible
at the beginning of the search?

Thank you.
Kirill
-------------- next part --------------
HTML attachment scrubbed and removed