Hi Lionel, Each call to klee_make_symbolic() creates a new symbolic object, which is completely unconstrained. I hope this clarifies KLEE's behavior on this program.
Best, Cristian On 04/24/2012 04:01 PM, Lionel PRAT wrote: > Hi, > > I find it hard to understand, why in the example below, klee turns to > infinity ... Is this normal? > Thank you > > Lionel > > #include<stdio.h> > #include<string.h> > #define PASSWD "test" > int bla(){ > char *x = (char*)malloc(10 * sizeof(char*)); > free(x); > return x[5]; > } > > int main() > { > char buff[100]; > int z=0; > do > { > klee_make_symbolic(&buff,sizeof(buff),"read"); > } > while(strncmp(PASSWD,buff,strlen(PASSWD))); > printf("fin boucle\n"); > z=bla(); > exit(0); > } > _______________________________________________ > klee-dev mailing list > klee-dev@keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list klee-dev@keeda.stanford.edu http://keeda.Stanford.EDU/mailman/listinfo/klee-dev