Unfortunately, this does not affect the way paths are explored. In
general, it doesn't make sense to use klee_assume(false) and
klee_assume(true). The first one terminates the state (klee_assert or
klee_report_error are more appropriate for that) and the second one does
nothing.
Paul
On 10/04/14 12:51, Urmas Repinski wrote:
Hi.
Sorry mistake in the 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_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 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_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 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
_______________________________________________
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
