[klee-dev] Handling segmentation fault in external call?

[David Manouchehri]

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 at 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)
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: toy.c
Type: application/octet-stream
Size: 2478 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20160925/5f694cb7/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: toy.bc
Type: application/octet-stream
Size: 9420 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20160925/5f694cb7/attachment-0001.obj>