bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--memstick--core--ms_block.ko-entry_point_true-unreach-call.cil.out.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.: 163 210 1884 10440
Removed infinite loop in msb_read_bad_block_table
Removed infinite loop in msb_read_oob
Removed infinite loop in h_msb_send_command
Removed infinite loop in h_msb_read_page
Removed infinite loop in sg_page
Removed infinite loop in sg_mark_end
Removed infinite loop in sg_assign_page
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in h_msb_parallel_switch
Removed infinite loop in h_msb_reset
Removed infinite loop in msb_write_block
Removed infinite loop in h_msb_write_block
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.506162881851
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 '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'sg_init_table' (function is undefined)
Removed calls to 'set_disk_ro' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'add_disk' (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 'mutex_lock' (function is undefined)
Removed calls to 'sg_init_one' (function is undefined)
Defining function printk as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'memstick_init_req' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'memstick_new_req' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'complete' (function is undefined)
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'memstick_init_req_sg' (function is undefined)
Defining function sg_next as symbolic
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'sg_miter_start' (function is undefined)
Removed calls to 'sg_miter_stop' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Defining function sg_nents as symbolic
Defining function sg_miter_next as symbolic
Defining function del_timer_sync as symbolic
Removed calls to 'blk_stop_queue' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'blk_requeue_request' (function is undefined)
Defining function blk_fetch_request as symbolic
Defining function blk_rq_map_sg as symbolic
Defining function __blk_end_request as symbolic
Removed calls to 'get_random_bytes' (function is undefined)
Defining function sg_copy_to_buffer as symbolic
Defining function mod_timer as symbolic
Defining function find_next_zero_bit as symbolic
Defining function sg_copy_from_buffer as symbolic
Defining function idr_alloc as symbolic
Defining function alloc_disk as symbolic
Removed calls to '__blk_end_request_all' (function is undefined)
Defining function blk_init_queue as symbolic
Removed calls to 'blk_dump_rq_flags' (function is undefined)
Defining function sprintf as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'memstick_unregister_driver' (function is undefined)
Removed calls to 'unregister_blkdev' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Defining function register_blkdev as symbolic
Defining function memstick_register_driver as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __kmalloc
  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.486213922501
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 153 192 1063 5605
INFO: Starting verification
KLEE: WARNING ONCE: function "msb_init_card" has inline asm
KLEE: WARNING ONCE: function "msb_read_page" has inline asm
KLEE: WARNING ONCE: function "msb_read_bad_block_table" has inline asm
KLEE: WARNING ONCE: function "msb_mark_block_used" has inline asm
KLEE: WARNING ONCE: function "h_msb_read_page" has inline asm
KLEE: WARNING ONCE: function "msb_erase_block" has inline asm
KLEE: WARNING ONCE: function "h_msb_send_command" has inline asm
KLEE: WARNING ONCE: function "msb_sg_copy" has inline asm
KLEE: WARNING ONCE: function "sg_page" has inline asm
KLEE: WARNING ONCE: function "sg_set_page" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "h_msb_parallel_switch" has inline asm
KLEE: WARNING ONCE: function "h_msb_reset" has inline asm
KLEE: WARNING ONCE: function "msb_io_work" has inline asm
KLEE: WARNING ONCE: function "msb_cache_flush" has inline asm
KLEE: WARNING ONCE: function "msb_cache_write" has inline asm
KLEE: WARNING ONCE: function "msb_update_block" has inline asm
KLEE: WARNING ONCE: function "h_msb_write_block" 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_e88beb77-a7ea-4224-8646-d1a5a75d7a7e/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PaVRD8/linux-4.2-rc1.tar.xz-32_7a-drivers--memstick--core--ms_block.ko-entry_point_true-unreach-call.cil.out.c:7403: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PaVRD8/linux-4.2-rc1.tar.xz-32_7a-drivers--memstick--core--ms_block.ko-entry_point_true-unreach-call.cil.out.c:7028: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 18737 states (over memory cap)
KLEE: WARNING: killing 15652 states (over memory cap)
KLEE: WARNING: killing 14989 states (over memory cap)
KLEE: WARNING: killing 14802 states (over memory cap)
KLEE: WARNING: killing 14391 states (over memory cap)
KLEE: WARNING: killing 14926 states (over memory cap)
KLEE: WARNING: killing 15101 states (over memory cap)
KLEE: WARNING: killing 14928 states (over memory cap)
KLEE: WARNING: killing 15579 states (over memory cap)
KLEE: WARNING: killing 15523 states (over memory cap)
KLEE: WARNING: killing 15828 states (over memory cap)
KLEE: WARNING: killing 15898 states (over memory cap)
KLEE: WARNING: killing 15611 states (over memory cap)
KLEE: WARNING: killing 16494 states (over memory cap)
KLEE: WARNING: killing 15872 states (over memory cap)
KLEE: WARNING: killing 16057 states (over memory cap)
KLEE: WARNING: killing 16017 states (over memory cap)
KLEE: WARNING: killing 16549 states (over memory cap)
KLEE: WARNING: killing 16279 states (over memory cap)
KLEE: WARNING: killing 16013 states (over memory cap)
KLEE: WARNING: killing 16195 states (over memory cap)
KLEE: WARNING: killing 16044 states (over memory cap)
KLEE: WARNING: killing 15666 states (over memory cap)
KLEE: WARNING: killing 15627 states (over memory cap)
KLEE: WARNING: killing 16029 states (over memory cap)
KLEE: WARNING: killing 15537 states (over memory cap)
KLEE: WARNING: killing 15498 states (over memory cap)
KLEE: WARNING: killing 15342 states (over memory cap)
KLEE: WARNING: killing 15749 states (over memory cap)
KLEE: WARNING: killing 15479 states (over memory cap)
KLEE: WARNING: killing 15221 states (over memory cap)
KLEE: WARNING: killing 15956 states (over memory cap)
KLEE: WARNING: killing 16141 states (over memory cap)
KLEE: WARNING: killing 15779 states (over memory cap)
KLEE: WARNING: killing 15515 states (over memory cap)
KLEE: WARNING: killing 15917 states (over memory cap)
KLEE: WARNING: killing 15548 states (over memory cap)
KLEE: WARNING: killing 15626 states (over memory cap)
KLEE: WARNING: killing 16132 states (over memory cap)
KLEE: WARNING: killing 15882 states (over memory cap)
KLEE: WARNING: killing 15736 states (over memory cap)
KLEE: WARNING: killing 15921 states (over memory cap)
KLEE: WARNING: killing 15988 states (over memory cap)
KLEE: WARNING: killing 16061 states (over memory cap)
KLEE: WARNING: killing 16345 states (over memory cap)
KLEE: WARNING: killing 15778 states (over memory cap)
KLEE: WARNING: killing 15750 states (over memory cap)
KLEE: WARNING: killing 16351 states (over memory cap)
KLEE: WARNING: killing 15892 states (over memory cap)
KLEE: WARNING: killing 15645 states (over memory cap)
KLEE: WARNING: killing 15935 states (over memory cap)
KLEE: WARNING: killing 16217 states (over memory cap)
KLEE: WARNING: killing 15873 states (over memory cap)
KLEE: WARNING: killing 15508 states (over memory cap)
KLEE: WARNING: killing 15897 states (over memory cap)
KLEE: WARNING: killing 15866 states (over memory cap)
KLEE: WARNING: killing 15721 states (over memory cap)
KLEE: WARNING: killing 16001 states (over memory cap)
KLEE: WARNING: killing 15660 states (over memory cap)
KLEE: WARNING: killing 15629 states (over memory cap)
KLEE: WARNING: killing 16114 states (over memory cap)
KLEE: WARNING: killing 15976 states (over memory cap)
KLEE: WARNING: killing 16355 states (over memory cap)
KLEE: WARNING: killing 16127 states (over memory cap)
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: WARNING: killing 16163 states (over memory cap)
KLEE: WARNING: killing 15723 states (over memory cap)
KLEE: WARNING: killing 16104 states (over memory cap)
KLEE: WARNING: killing 15553 states (over memory cap)
KLEE: WARNING: killing 15414 states (over memory cap)
KLEE: WARNING: killing 15899 states (over memory cap)
KLEE: WARNING: killing 16071 states (over memory cap)
KLEE: WARNING: killing 16237 states (over memory cap)
KLEE: WARNING: killing 16010 states (over memory cap)
KLEE: WARNING: killing 16273 states (over memory cap)
KLEE: WARNING: killing 15536 states (over memory cap)
KLEE: WARNING: killing 15913 states (over memory cap)
KLEE: WARNING: killing 15673 states (over memory cap)
KLEE: WARNING: killing 15844 states (over memory cap)
KLEE: WARNING: killing 16016 states (over memory cap)
KLEE: WARNING: killing 15792 states (over memory cap)
KLEE: WARNING: killing 15859 states (over memory cap)
KLEE: WARNING: killing 15433 states (over memory cap)
KLEE: WARNING: killing 15993 states (over memory cap)
KLEE: WARNING: killing 15569 states (over memory cap)
KLEE: WARNING: killing 15542 states (over memory cap)
KLEE: WARNING: killing 16104 states (over memory cap)
KLEE: WARNING: killing 16169 states (over memory cap)
KLEE: WARNING: killing 15748 states (over memory cap)
KLEE: WARNING: killing 15819 states (over memory cap)
KLEE: WARNING: killing 16280 states (over memory cap)
KLEE: WARNING: killing 16046 states (over memory cap)
KLEE: WARNING: killing 15524 states (over memory cap)
KLEE: WARNING: killing 15597 states (over memory cap)
KLEE: WARNING: killing 15560 states (over memory cap)
KLEE: WARNING: killing 15827 states (over memory cap)
KLEE: WARNING: killing 16090 states (over memory cap)
KLEE: WARNING: killing 16065 states (over memory cap)
KLEE: WARNING: killing 15648 states (over memory cap)
KLEE: WARNING: killing 15709 states (over memory cap)
KLEE: WARNING: killing 15968 states (over memory cap)
KLEE: WARNING: killing 16131 states (over memory cap)
KLEE: WARNING: killing 16297 states (over memory cap)
KLEE: WARNING: killing 15688 states (over memory cap)
KLEE: WARNING: killing 15855 states (over memory cap)
KLEE: WARNING: killing 15921 states (over memory cap)
KLEE: WARNING: killing 15892 states (over memory cap)
KLEE: WARNING: killing 15856 states (over memory cap)
KLEE: WARNING: killing 15830 states (over memory cap)
KLEE: WARNING: killing 16185 states (over memory cap)
KLEE: WARNING: killing 15869 states (over memory cap)
KLEE: WARNING: killing 15642 states (over memory cap)
KLEE: WARNING: killing 15429 states (over memory cap)
KLEE: WARNING: killing 15777 states (over memory cap)
KLEE: WARNING: killing 15368 states (over memory cap)
KLEE: WARNING: killing 15998 states (over memory cap)
KLEE: WARNING: killing 15593 states (over memory cap)
KLEE: WARNING: killing 15660 states (over memory cap)
KLEE: WARNING: killing 15914 states (over memory cap)
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: WARNING: killing 15851 states (over memory cap)
