KLEE's model shares file descriptors between states. However, in your example it seems that fopen fails and fputs crashes because it's called with a NULL pointer. That has nothing to do with KLEE's model.
Paul On 11 Mar 2013, at 22:33, Bowen Zhou <[email protected]> wrote: > Hello, > > For the sample code below: > > #include <stdio.h> > #include <klee/klee.h> > > int > main(int argc, char** argv) > { > int c = 1; > klee_make_symbolic(&c, sizeof(c), "c"); > FILE* fp = fopen("test", "w"); > if (c) > fputs("hello", fp); > fclose(fp); > } > > KLEE outputs: > > bzhou@orion01:~/llvm/klee$ Release+Asserts/bin/klee --posix-runtime > examples/open/open.bc > KLEE: NOTE: Using model: > /home/min/a/bzhou/llvm/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca > KLEE: output directory = "klee-out-12" > KLEE: WARNING: undefined reference to function: __errno_location > KLEE: WARNING: undefined reference to function: fclose > KLEE: WARNING: undefined reference to function: fopen > KLEE: WARNING: undefined reference to function: fputs > KLEE: WARNING: undefined reference to function: fwrite > KLEE: WARNING: undefined reference to variable: stderr > KLEE: WARNING ONCE: calling external: syscall(4, 30457376, 30523328) > KLEE: WARNING ONCE: calling external: fopen(26278016, 30437312) > KLEE: WARNING ONCE: calling external: fclose(0) > KLEE: ERROR: failed external call: fclose > KLEE: NOTE: now ignoring this error at this location > KLEE: WARNING ONCE: calling external: fputs(30437776, 0) > Segmentation fault (core dumped) > > This leads me to suspect that KLEE does not have a private environment for > each state therefore if one state closes a file, the file would be closed for > all the rest states. This is counter-intuitive to me, or did I miss anything? > > Regards > Bowen Zhou > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
