When my target program causes an external call to segfault, that also causes KLEE to crash. Is there a "proper" way to deal with this?
klee@9b5f058c9891:/ubuntu/sim-fuzz-1$ klee --optimize --libc=uclibc --posix-runtime --allow-external-sym-calls toy.bc A --sym-files 1 100 KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca KLEE: NOTE: Using model: /home/klee/klee_build/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca KLEE: output directory is "/ubuntu/sim-fuzz-1/klee-out-1088" Using STP solver backend KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 47161680) KLEE: WARNING ONCE: ioctl: (TCGETS) symbolic file, incomplete model KLEE: WARNING ONCE: calling external: printf(45836352, (ReadLSB w32 12 A-data)) File timestamp: 0 File timestamp: 0 Entry: bar = �������������������������, Unknown type 0 intdata = 0 KLEE: WARNING ONCE: silently concretizing (reason: floating point) expression (ReadLSB w32 36 A-data) to value 0 (/ubuntu/sim-fuzz-1/toy.c:65) fdata = 0.000000 KLEE: ERROR: /ubuntu/sim-fuzz-1/toy.c:63: failed external call: printf KLEE: NOTE: now ignoring this error at this location Entry: bar = �������������������������, Unknown type 0 intdata = 0 Segmentation fault (core dumped) Thanks, David Manouchehri (Originally asked at https://github.com/klee/klee/issues/432)
toy.c
Description: Binary data
toy.bc
Description: Binary data
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
