Hi Alvin,
On Tue, Nov 17, 2009 at 10:31 PM, Alvin Cheung <alvin.cheung at gmail.com>
wrote:
> Hello,
>
> I am trying to use the klee symbolic file system to explore all paths in a
> simple program:
>
> char buf[10];
> FILE * file = fopen(argv[1], "r");
>
> if (file != NULL) {
> ? fread(buf, sizeof(char), 1, file);
> ? if (buf[0] == 'a') printf("path 0\n");
> ? else printf("path 1\n");
> }
> else printf("path 2\n");
>
> I invoked klee with --libc=uclibc --posix-runtime --init-env prog.bc
> --sym-arg 1
> and it explored 3 paths: path 1, and path 2 for 2 times. ?I am wondering why
> path 0 is not explored in this case? ?I thought buf would be symbolic given
> that
> it was read from a symbolic file?
You need to also pass "--sym-files 1 32" (create stdin and up to 1
files as symbolic, with up to 32 bytes of data).
Otherwise looks fine to me.
- Daniel
> Thanks,
> Alvin
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
