bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko_false-unreach-call.cil.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.: 145 487 1724 11234
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_linux_kernel_module_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.488399982452
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'blk_queue_prep_rq' (function is undefined)
Removed calls to 'blk_queue_bounce_limit' (function is undefined)
Removed calls to 'blk_queue_max_hw_sectors' (function is undefined)
Removed calls to 'blk_queue_max_segments' (function is undefined)
Removed calls to 'blk_queue_max_segment_size' (function is undefined)
Removed calls to 'blk_queue_logical_block_size' (function is undefined)
Removed calls to 'add_disk' (function is undefined)
Removed calls to '__ldv_linux_kernel_locking_spinlock_spin_lock' (function is undefined)
Removed calls to 'blk_start_queue' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'del_gendisk' (function is undefined)
Removed calls to 'blk_cleanup_queue' (function is undefined)
Removed calls to 'blk_stop_queue' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'memstick_init_req' (function is undefined)
Removed calls to 'memstick_new_req' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'sg_init_one' (function is undefined)
Defining function memstick_set_rw_addr as symbolic
Defining function printk as symbolic
Defining function snprintf as symbolic
Defining function scnprintf as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'complete_all' (function is undefined)
Defining function __blk_end_request as symbolic
Defining function blk_rq_map_sg as symbolic
Defining function __blk_end_request_cur as symbolic
Defining function blk_fetch_request as symbolic
Removed calls to 'blk_dump_rq_flags' (function is undefined)
Defining function sprintf as symbolic
Defining function blk_init_queue as symbolic
Defining function alloc_disk as symbolic
Removed calls to 'memstick_unregister_driver' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Defining function register_blkdev as symbolic
Defining function memstick_register_driver as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  memcmp
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.521921157837
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 213 432 1535 6959
INFO: Starting verification
KLEE: WARNING ONCE: function "h_mspro_block_transfer_data" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5c9bd985-b353-407c-ac99-ed81426265ba/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wHlMdN/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko_false-unreach-call.cil.c:4946: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5c9bd985-b353-407c-ac99-ed81426265ba/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_5c9bd985-b353-407c-ac99-ed81426265ba/symbiotic/lib/verifier/__VERIFIER_error.c
Line: 9
assembly.ll line: 686
Stack: 
	#000000686 in __VERIFIER_error () at /tmp/vcloud-vcloud-master/worker/working_dir_5c9bd985-b353-407c-ac99-ed81426265ba/symbiotic/lib/verifier/__VERIFIER_error.c:9
	#100005182 in ldv_linux_lib_idr_idr_destroy_mspro_block_disk_idr () at /tmp/symbiotic-wHlMdN/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko_false-unreach-call.cil.c:12362
	#200005169 in ldv_EMGentry_exit_mspro_block_exit_3_2 (=0) at /tmp/symbiotic-wHlMdN/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko_false-unreach-call.cil.c:8141
	#300005696 in ldv_entry_EMGentry_3 (=0) at /tmp/symbiotic-wHlMdN/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko_false-unreach-call.cil.c:7469
	#400006509 in main () at /tmp/symbiotic-wHlMdN/linux-4.0-rc1---drivers--memstick--core--mspro_block.ko_false-unreach-call.cil.c:7485

 --- ----------- ---
Generating witness: /tmp/vcloud-vcloud-master/worker/working_dir_5c9bd985-b353-407c-ac99-ed81426265ba/symbiotic/witness.graphml
 -- ---- --
Symbolic objects:
nondet := len 8 bytes, |8 times 0x0|
nondet:1 := len 8 bytes, |8 times 0x0|
nondet:2 := len 8 bytes, |8 times 0x0|
nondet:3 := len 1 bytes, |0x0|
nondet:4 := len 8 bytes, |8 times 0x0|
nondet:5 := len 4 bytes, |4 times 0x0|
nondet:6 := len 8 bytes, |8 times 0x0|
nondet:7 := len 8 bytes, |8 times 0x0|
nondet:8 := len 8 bytes, |8 times 0x0|
nondet:9 := len 8 bytes, |8 times 0x0|
nondet:10 := len 8 bytes, |8 times 0x0|
nondet:11 := len 8 bytes, |8 times 0x0|
nondet:12 := len 8 bytes, |8 times 0x0|
nondet:13 := len 8 bytes, |8 times 0x0|
nondet:14 := len 8 bytes, |8 times 0x0|
nondet:15 := len 8 bytes, |8 times 0x0|
nondet:16 := len 8 bytes, |8 times 0x0|
nondet:17 := len 8 bytes, |8 times 0x0|
nondet:18 := len 8 bytes, |8 times 0x0|
nondet:19 := len 8 bytes, |8 times 0x0|
nondet:20 := len 8 bytes, |8 times 0x0|
nondet:21 := len 40 bytes, |40 times 0x0|
nondet:22 := len 1 bytes, |0x0|
nondet:23 := len 16 bytes, |16 times 0x0|
nondet:24 := len 8 bytes, |8 times 0x0|
nondet:25 := len 2 bytes, |2 times 0x0|
nondet:26 := len 8 bytes, |8 times 0x0|
nondet:27 := len 12 bytes, |12 times 0x0|
nondet:28 := len 1 bytes, |0x0|
nondet:29 := len 8 bytes, |8 times 0x0|
nondet:30 := len 4 bytes, |4 times 0x0|
nondet:31 := len 40 bytes, |40 times 0x0|
nondet:32 := len 8 bytes, |8 times 0x0|
nondet:33 := len 8 bytes, |8 times 0x0|
nondet:34 := len 4 bytes, |4 times 0x0|
extern-global:nr_cpu_ids := len 4 bytes, |3 times 0xff|0x7f|
extern-global:__this_module := len 856 bytes, |856 times 0x0|
ldv_undef_int:tmp:10453 := len 4 bytes, |4 times 0x1|
malloc0 := len 16 bytes, |16 times 0x0|
malloc0:1 := len 480 bytes, |480 times 0x0|
malloc0:2 := len 1736 bytes, |1736 times 0x0|
malloc0:3 := len 16 bytes, |16 times 0x0|
malloc0:4 := len 1608 bytes, |1608 times 0x0|
ldv_undef_int:tmp:10453:1 := len 4 bytes, |4 times 0x0|
ldv_undef_int:tmp:10453:2 := len 4 bytes, |4 times 0x0|
 -- ---- --
INFO: Total time elapsed: 5.57026600838
