[klee-dev] Direct Search Towards Assertion

[Urmas Repinski]

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: 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 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: 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 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
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 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed