Hi.
Sorry mistake in the code.
#define n 10int 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_assume(false);
//klee_assert(false); }
klee_assume(true); return 0;}
Urmas.
From: [email protected]
To: [email protected]; [email protected]
Date: Thu, 10 Apr 2014 14:49:32 +0300
Subject: Re: [klee-dev] Direct Search Towards Assertion
Hi, Kirill.
As far as during generation paths, where klee_assume(false) occur, are not
processed, then i suggest to try following:
If you require input when index == 3 to be generated, then it is possible to
disable all paths where index != 3, and to launch generation.
This should make generation of the input with properties you require.
Try this one:
#define n 10int 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_assume(false);
//klee_assert(false); }
klee_assume(false); return 0;}
This should help,
Urmas Repinski.
Date: Thu, 10 Apr 2014 09:25:10 +0100
From: [email protected]
To: [email protected]
Subject: [klee-dev] Direct Search Towards Assertion
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 10int 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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
