Hi Kapil,
You might be able to get around the issue by also setting 
--max-sym-array-size to a reasonable value. For example
/klee.cde --optimize --libc=uclibc --posix-runtime --init-env 
--max-sym-array-size=512 ./mknod.bc -sym-args 0 2 2

Paul

On 18/06/12 18:02, Kapil Anand wrote:
> Hi all,
>
> I downloaded Klee pre-built package and was trying to run the coreutils
> case study. However, I receive a segmentation fault while running KLEE
> on a bunch of coreutils programs. I didn't modify the code at all and
> was just running the pre-built Codeutils present in obj-llvm folder
> through the klee.cde present in bin folder.
>
> Command:
>
> /klee.cde --optimize --libc=uclibc --posix-runtime --init-env ./mknod.bc
> -sym-args 0 2 2/
> /
> /
> /
> /
> OUTPUT:
>
> /KLEE: NOTE: Using model:
> /home/pgbovine/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca/
> /KLEE: output directory = "klee-out-4"/
> /WARNING: While resolving call to function '__user_main' arguments were
> dropped!/
> /KLEE: WARNING: function "vasnprintf" has inline asm/
> /KLEE: WARNING: undefined reference to function: klee_get_valuel/
> /KLEE: WARNING: undefined reference to function: signbitl/
> /KLEE: WARNING: executable has module level assembly (ignoring)/
> /KLEE: WARNING: calling external: syscall(54, 0, 21505, 4149029928)/
> /missing operand/
> /KLEE: WARNING: calling external: vprintf(4140390016, 4140507000)/
> /Try `./mknod.bc --help' for more information./
> /KLEE: WARNING: calling close_stdout with extra arguments./
> /missing operand after `\n'/
> /Try `./mknod.bc --help' for more information./
> /missing operand after `\n'/
> /Try `./mknod.bc --help' for more information./
> /missing operand after `\n\a'/
> /Try `./mknod.bc --help' for more information./
> /missing operand after `\n\n'/
> /Try `./mknod.bc --help' for more information./
> /missing operand after `\n'/
> /Try `./mknod.bc --help' for more information./
> /KLEE: WARNING: flushing 255800 bytes on read, may be slow and/or crash:
> MO197[255800] allocated at global:locale_mmap/
> /+++ killed by SIGSEGV +++/
> /Segmentation fault/
>
>
> Thanks!
>
> --Kapil
>
>
> _______________________________________________
> klee-dev mailing list
> [email protected]
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>


_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev

Reply via email to