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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
