[klee-dev] KLEE does not maintain a private environment for each state?

[Paul Marinescu]

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 <bwzhou at gmail.com> 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 at 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev