[klee-dev] Reduce Test count of KLEE

[Saksham Jain]

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 <sakjain92.work at gmail.com>
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 () {
>
>
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed