bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-commit-tester/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 31 46 577 4219
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.21728014946
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function compute_finetune as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function printk as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function note_to_freq as symbolic
Defining function _copy_to_user as symbolic
Defining function __copy_user_nocache as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.194628000259
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 48 34 236 2004
INFO: Starting verification
KLEE: WARNING ONCE: function "opl3_command" has inline asm
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:3637: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:3079: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:3665: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:3458: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:3368: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:2906: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:3758: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:3483: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:2855: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:3308: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:2885: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:2721: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-52aKe2/m0_true-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d.c:2732: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 7004 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12544 states (over memory cap)
KLEE: WARNING: killing 11847 states (over memory cap)
KLEE: WARNING: killing 6485 states (over memory cap)
KLEE: WARNING: killing 12244 states (over memory cap)
KLEE: WARNING: killing 11625 states (over memory cap)
KLEE: WARNING: killing 10757 states (over memory cap)
KLEE: WARNING: killing 9894 states (over memory cap)
KLEE: WARNING: killing 9735 states (over memory cap)
KLEE: WARNING: killing 9322 states (over memory cap)
KLEE: WARNING: killing 9293 states (over memory cap)
KLEE: WARNING: killing 9201 states (over memory cap)
KLEE: WARNING: killing 9681 states (over memory cap)
KLEE: WARNING: killing 9530 states (over memory cap)
KLEE: WARNING: killing 9007 states (over memory cap)
KLEE: WARNING: killing 9483 states (over memory cap)
KLEE: WARNING: killing 9960 states (over memory cap)
KLEE: WARNING: killing 9875 states (over memory cap)
KLEE: WARNING: killing 9858 states (over memory cap)
KLEE: WARNING: killing 9897 states (over memory cap)
KLEE: WARNING: killing 9877 states (over memory cap)
KLEE: WARNING: killing 9302 states (over memory cap)
KLEE: WARNING: killing 10268 states (over memory cap)
KLEE: WARNING: killing 10129 states (over memory cap)
KLEE: WARNING: killing 9987 states (over memory cap)
KLEE: WARNING: killing 10156 states (over memory cap)
KLEE: WARNING: killing 9709 states (over memory cap)
KLEE: WARNING: killing 9565 states (over memory cap)
KLEE: WARNING: killing 9422 states (over memory cap)
KLEE: WARNING: killing 9463 states (over memory cap)
KLEE: WARNING: killing 9448 states (over memory cap)
KLEE: WARNING: killing 10092 states (over memory cap)
KLEE: WARNING: killing 9293 states (over memory cap)
KLEE: WARNING: killing 9636 states (over memory cap)
KLEE: WARNING: killing 9317 states (over memory cap)
KLEE: WARNING: killing 9838 states (over memory cap)
KLEE: WARNING: killing 9700 states (over memory cap)
KLEE: WARNING: killing 9803 states (over memory cap)
KLEE: WARNING: killing 9910 states (over memory cap)
KLEE: WARNING: killing 8816 states (over memory cap)
KLEE: WARNING: killing 9751 states (over memory cap)
KLEE: WARNING: killing 10209 states (over memory cap)
KLEE: WARNING: killing 9478 states (over memory cap)
KLEE: WARNING: killing 9047 states (over memory cap)
KLEE: WARNING: killing 9920 states (over memory cap)
KLEE: WARNING: killing 9076 states (over memory cap)
KLEE: WARNING: killing 9355 states (over memory cap)
KLEE: WARNING: killing 10044 states (over memory cap)
KLEE: WARNING: killing 8972 states (over memory cap)
KLEE: WARNING: killing 9658 states (over memory cap)
KLEE: WARNING: killing 9118 states (over memory cap)
KLEE: WARNING: killing 9569 states (over memory cap)
KLEE: WARNING: killing 9555 states (over memory cap)
KLEE: WARNING: killing 9424 states (over memory cap)
KLEE: WARNING: killing 9644 states (over memory cap)
KLEE: WARNING: killing 9631 states (over memory cap)
KLEE: WARNING: killing 9441 states (over memory cap)
KLEE: WARNING: killing 9777 states (over memory cap)
KLEE: WARNING: killing 9356 states (over memory cap)
KLEE: WARNING: killing 9334 states (over memory cap)
KLEE: WARNING: killing 9378 states (over memory cap)
KLEE: WARNING: killing 9131 states (over memory cap)
KLEE: WARNING: killing 9518 states (over memory cap)
KLEE: WARNING: killing 9394 states (over memory cap)
KLEE: WARNING: killing 9148 states (over memory cap)
KLEE: WARNING: killing 9593 states (over memory cap)
KLEE: WARNING: killing 9404 states (over memory cap)
KLEE: WARNING: killing 9395 states (over memory cap)
KLEE: WARNING: killing 9719 states (over memory cap)
KLEE: WARNING: killing 9762 states (over memory cap)
KLEE: WARNING: killing 9177 states (over memory cap)
KLEE: WARNING: killing 9732 states (over memory cap)
KLEE: WARNING: killing 9378 states (over memory cap)
KLEE: WARNING: killing 9647 states (over memory cap)
KLEE: WARNING: killing 9749 states (over memory cap)
KLEE: WARNING: killing 5759 states (over memory cap)
KLEE: WARNING: killing 8942 states (over memory cap)
KLEE: WARNING: killing 9323 states (over memory cap)
KLEE: WARNING: killing 8687 states (over memory cap)
KLEE: WARNING: killing 9684 states (over memory cap)
KLEE: WARNING: killing 9444 states (over memory cap)
KLEE: WARNING: killing 9825 states (over memory cap)
KLEE: WARNING: killing 9755 states (over memory cap)
KLEE: WARNING: killing 9019 states (over memory cap)
KLEE: WARNING: killing 8834 states (over memory cap)
KLEE: WARNING: killing 8979 states (over memory cap)
KLEE: WARNING: killing 9245 states (over memory cap)
KLEE: WARNING: killing 9511 states (over memory cap)
KLEE: WARNING: killing 8778 states (over memory cap)
KLEE: WARNING: killing 9703 states (over memory cap)
KLEE: WARNING: killing 9913 states (over memory cap)
KLEE: WARNING: killing 9901 states (over memory cap)
KLEE: WARNING: killing 9449 states (over memory cap)
KLEE: WARNING: killing 9378 states (over memory cap)
KLEE: WARNING: killing 9196 states (over memory cap)
KLEE: WARNING: killing 9075 states (over memory cap)
KLEE: WARNING: killing 9281 states (over memory cap)
KLEE: WARNING: killing 9376 states (over memory cap)
KLEE: WARNING: killing 9749 states (over memory cap)
KLEE: WARNING: killing 10286 states (over memory cap)
