Hi. > 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.
Yes, it will behave exactly as defined, klee_assume(false) terminates the state and the klee_assume(true) does nothing. Using this functionality it is possible to exclude all paths, where index != 3 , from the generation, to terminate all states where index != 3 , and to keep one state where index == 3. This should generate the required input. As far as i see, usage of those 2 operators and plus logical conditions allows to modify code in this way, that only required set of inputs is generated. I am terribly sorry, but i still think that usage of klee_assume() function can be reasonable for input generation. And not in this case only, i had made set of experiments on input generation by dynamical modification of the code using adding/removing klee_assume(...) function to the code and processing it by the KLEE. Unfortunately nothing is published, as far as no meaningful experimental results were achieved, but usage of KLEE klee_assume(...) function still can be extremely useful. Urmas Repinski. > Date: Thu, 10 Apr 2014 13:13:27 +0100 > From: [email protected] > To: [email protected]; [email protected]; [email protected] > Subject: Re: [klee-dev] Direct Search Towards Assertion > > 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
