Hi
The best you can do is not use -search=dfs. The current default search
strategy is generally better than dfs and uses a combination of
randomness and the minimum distance to an uncovered instruction
(nurs:covnew).
See klee --help for available search strategies (nurs:md2u is another
candidate).
You should keep in mind however that these search strategies will try
the shortest static path to an uncovered instruction. If that path
proves to be infeasible, they're gonna try the next shortest path and so
on. While your example is fairly straightforward, generating that single
path may not be.
You may want to search for 'directed symbolic execution'. There are
several tools (including one based on KLEE on which I worked
http://srg.doc.ic.ac.uk/projects/katch/) but the general problem is
undecidable.
Paul
On 10/04/14 09:25, Kirill Bogdanov wrote:
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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
