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
