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

[Cristian Cadar]

Hi, you should also set --libc (e.g, --libc=uclibc).

Cristian

On 11/03/2013 22:33, Bowen Zhou 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