[klee-dev] Reduce Test count of KLEE

[Cristian Cadar]

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 <sakjain92.work at gmail.com
> <mailto: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 () {
>
>
>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>