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

[Bowen Zhou]

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