Hi Daniel, Thank you! Using the --use-forked-stp option, Klee works well despite many STP errors.
Regards, Wujie Daniel Dunbar wrote: > Hi Wujie, > > The warning message is probably right. Unfortunately STP is recursive and can > end up blowing the stack with very large arrays. > > Try using --max-sym-array-size or --use-forked-stp. > > The second problem is some kind of KLEE bug; if I had to guess probably > related to non-deterministic malloc. > > - Daniel > > > On May 13, 2010, at 23:03, Wujie Zheng <wjzheng at cse.cuhk.edu.hk> wrote: > > >> Hi, >> >> When running klee on programs, I sometimes run into the problem of >> segmentation fault, especially when using --optimize. For example, here >> is the output when I try to test grep v2.5.1, >> >> grep/obj-llvm/src# klee --optimize --libc=uclibc --posix-runtime >> --init-env ./grep.bc --sym-args 1 3 6 --sym-files 2 8 >> KLEE: NOTE: Using model: /work/klee/Release/lib/libkleeRuntimePOSIX.bca >> KLEE: output directory = "klee-out-17" >> WARNING: While resolving call to function '__user_main' arguments were >> dropped! >> KLEE: WARNING: undefined reference to function: __xpg_strerror_r >> KLEE: WARNING: undefined reference to function: __xstat64 >> KLEE: WARNING: undefined reference to function: gettext >> KLEE: WARNING: executable has module level assembly (ignoring) >> KLEE: WARNING: calling external: syscall(54, 0, 21505, 165501504) >> KLEE: WARNING: calling external: __xstat64(3, 165915040, 171126272) >> KLEE: WARNING: calling external: gettext(171516456) >> KLEE: WARNING: calling external: getpagesize() >> KLEE: WARNING: flushing 36865 bytes on read, may be slow and/or crash: >> MO25992[36865] allocated at grepfile(): %37 = call noalias i8* >> @malloc(i32 %36) nounwind ; <i8*> [#uses=2] >> Segmentation fault >> >> I am wondering what are the causes of this problem and how to avoid it >> (removing --optimize makes klee increase coverage of the PUT very slowly)? >> >> >> In addition, when specifying --sym-args with the same value for lower >> and upper bounds of the number of arguments (i.e., fixing the number of >> arguments), klee generates tests normally but klee-replay fails to >> replay the generated tests with the following error message: >> >> grep/obj-llvm/src# klee --libc=uclibc --posix-runtime --init-env >> ./grep.bc --sym-args 3 3 6 --sym-files 2 8 >> ... >> grep/obj-gcov/src# klee-replay ./grep ../../obj-llvm/src/klee-last/*.ktest >> make_symbolic mismatch, different sizes: 7 in input file, 4 in code >> >> Regards, >> Wujie >> _______________________________________________ >> klee-dev mailing list >> klee-dev at keeda.stanford.edu >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> > >
