[klee-dev] how to dampen ktest exuberance with symbolic index into symbolic array

[Richard Rutledge]

Consider the following program:

//-----------------------------------------------------------------
#include <stdlib.h>
#include <klee/klee.h>

#define BUFFER_SIZE 16

int main(int argc, char *argv[]) {

   char *buffer = malloc(BUFFER_SIZE);
   int index;

   klee_make_symbolic(buffer, BUFFER_SIZE, "buffer");
   klee_make_symbolic(&index, sizeof(index), "index");

   if (buffer[index] == '\0') {
     return 1;
   }
   return 0;
}

//-----------------------------------------------------------------

Given this program, klee generates approx 180 test cases (the actual 
number seems to vary). I understand from prior correspondence here that 
klee forks a path for each object which can be referenced. The forking 
occurs in Executor::executeMemoryOperation().

My objective is to only generate inbounds values of buffer and index 
that induce each of the two paths through the program. My attempts to 
modify AddressSpace::resolve to only return the single desired memory 
object have so far been disappointing (i.e. abject failure).

Any suggestions as to how I should proceed?

Thanks!

Rick Rutledge