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
