You might like to take a look at the option
--only-output-states-covering-new
Cristian
On 19/06/15 05:15, Saksham Jain wrote:
Sorry, Hit sent by mistake. Here is the continuation from the previous mail.
/* Test is the function I am trying to test through KLEE */
void test( int index_i, int data_i, struct my_struct *my_struct_p )
{
switch(index_i) {
case 0: { <some code which depends on data_i and my_struct_obj
with some assertions>;break; }
case 1: { <some other code which depends on data_i and
my_struct_obj with some assertions>;break; }
...
...
...
case 19: { <some other code which depends on data_i and
my_struct_obj with some assertions>;break; }
default:return
}
}
#define MAX_COUNT 10
struct my_struct { <some definition> };
int main {
int i;
int index[ MAX_COUNT ];
int data[ MAX_COUNT ];
klee_make_symbolic( &index,MAX_COUNT *sizeof( int ),"index");
klee_make_symbolic( &data, MAX_COUNT *sizeof( int ), "data");
klee_assume( index < 20 );
klee_assume( index >= 0 );
my_struct my_struct_obj;
init( &my_struct_obj ); /* Does some initialization (with zeros)*/
for ( i=0 ;i<MAX_COUNT ;i++) {
test(index[i], data[i] ,&my_struct_obj);
}
}
The explosion is because: if MAX_COUNT is 1: Test cases created is
roughly 20,
if MAX_COUNT is 2: Test count is roughly 400 (multiplication factor of
20 with each increase of MAX_COUNT)
and so on. For MAX COUNT 10, KLEE wouldn't be able to make test cases.
Can someone point me in some direction to reduce the number of test
cases being generated?
I would ideally like KLEE to construct test cases covering every line in
test function first. Or to terminate after the line coverage/branch
coverage in test function is 100%.
I can also deal with less than 100% coverage but I don't want test cases
explosion.
Are there any sim-args in KLEE for doing anything of this sort.?
Regards,
Saksham Jain
On Fri, Jun 19, 2015 at 9:22 AM, Saksham Jain <[email protected]
<mailto:[email protected]>> wrote:
Hi,
I am facing the problem of path explosion but I am facing it at
exponential rate. I am trying to test a function 'test' as shown below.
int main () {
_______________________________________________
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
