[klee-dev] Direct Search Towards Assertion

[Paul Marinescu]

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: urrimus at hotmail.com
> To: kirill.sc at gmail.com; klee-dev at imperial.ac.uk
> 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: kirill.sc at gmail.com
> To: klee-dev at imperial.ac.uk
> 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
> klee-dev at imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> _______________________________________________ klee-dev mailing list
> klee-dev at imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>