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
