bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-commit-tester/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.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 4234
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.218784093857
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.194592952728
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 48 34 238 2019
INFO: Starting verification
KLEE: WARNING ONCE: function "opl3_command" has inline asm
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3638: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3759: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3666: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3368: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3079: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3459: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:2855: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:2906: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3484: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3308: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:2732: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:2721: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.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/vcloud-vcloud-master/worker/working_dir_120b80e2-7f0f-4d7f-b7ff-2c6206c6ccf8/symbiotic/lib/verifier/__VERIFIER_error.c:9: ASSERTION FAIL: verifier assertion failed
KLEE: NOTE: now ignoring this error at this location
Error found.
RESULT: false(unreach-call)

 --- Error trace ---

Error: ASSERTION FAIL: verifier assertion failed
File: /tmp/vcloud-vcloud-master/worker/working_dir_120b80e2-7f0f-4d7f-b7ff-2c6206c6ccf8/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 304
Stack: 
	#000000304 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_120b80e2-7f0f-4d7f-b7ff-2c6206c6ccf8/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100002111 in ldv_copy_from_user_7 (, , ) at /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:6304
	#200001612 in main () at /tmp/symbiotic-mFAdp6/m0_false-unreach-call_sound-oss-opl3-ko--111_1a--42f9f8d-1.c:3436

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_120b80e2-7f0f-4d7f-b7ff-2c6206c6ccf8/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 4 bytes, |4 times 0x0|
nondet:1 := len 8 bytes, |8 times 0x0|
nondet:2 := len 8 bytes, |8 times 0x0|
nondet:3 := len 8 bytes, |8 times 0x0|
nondet:4 := len 8 bytes, |8 times 0x0|
nondet:5 := len 1 bytes, |0x0|
nondet:6 := len 8 bytes, |8 times 0x0|
nondet:7 := len 8 bytes, |8 times 0x0|
nondet:8 := len 40 bytes, |40 times 0x0|
nondet:9 := len 8 bytes, |8 times 0x0|
nondet:10 := len 8 bytes, |8 times 0x0|
nondet:11 := len 4 bytes, |0x29|3 times 0x0|
extern-global:__this_module := len 608 bytes, |608 times 0x0|
extern-global:synth_devs := len 88 bytes, |88 times 0x0|
extern-global:ioport_resource := len 56 bytes, |56 times 0x0|
main:tmp___1:6227 := len 4 bytes, |4 times 0x1|
main:tmp___0:6135 := len 4 bytes, |0x8|3 times 0x0|
 -- ---- --
INFO: Total time elapsed: 1.77672600746
