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-43_2a-drivers--scsi--osst.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.: 214 144 3125 20462
Removed infinite loop in sg_page
Removed infinite loop in sg_assign_page
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.654796123505
Defining function snprintf as symbolic
Removed calls to '_raw_write_lock' (function is undefined)
Removed calls to '_raw_write_unlock' (function is undefined)
Removed calls to 'panic' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'sdev_prefix_printk' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'put_disk' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Defining function alloc_disk as symbolic
Defining function printk as symbolic
Defining function sprintf as symbolic
Defining function device_create as symbolic
Defining function device_create_file as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'scsi_device_put' (function is undefined)
Defining function scsi_set_medium_removal as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'blk_rq_set_block_pc' (function is undefined)
Removed calls to 'blk_put_request' (function is undefined)
Removed calls to 'blk_execute_rq_nowait' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to '__scsi_print_sense' (function is undefined)
Defining function scsi_normalize_sense as symbolic
Defining function scsi_get_sense_info_fld as symbolic
Defining function scsi_sense_desc_find as symbolic
Defining function blk_get_request as symbolic
Defining function sg_next as symbolic
Defining function blk_rq_map_user as symbolic
Defining function blk_rq_map_kern as symbolic
Removed calls to 'complete' (function is undefined)
Removed calls to '__blk_put_request' (function is undefined)
Defining function blk_rq_unmap_user as symbolic
Defining function jiffies_to_msecs as symbolic
Defining function schedule_timeout_interruptible as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function scsi_device_get as symbolic
Defining function scsi_block_when_processing_errors as symbolic
Defining function strlcpy as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function scsi_ioctl_block_when_processing_errors as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function capable as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function scsi_ioctl as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'driver_remove_file' (function is undefined)
Removed calls to 'driver_unregister' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function scsi_register_driver as symbolic
Defining function driver_create_file as symbolic
Defining function __register_chrdev as symbolic
Defining function __class_create as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  strlen
  strncmp
  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.705615997314
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 308 131 1712 11121
INFO: Starting verification
KLEE: WARNING ONCE: function "sg_page" has inline asm
KLEE: WARNING ONCE: function "osst_do_scsi" has inline asm
KLEE: WARNING ONCE: function "sg_set_page" 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_0261588b-9929-4e70-8106-31b8f0e2310e/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-w_dCQV/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--osst.ko-entry_point_true-unreach-call.cil.out.c:8795: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-w_dCQV/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--osst.ko-entry_point_true-unreach-call.cil.out.c:11932: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-w_dCQV/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--osst.ko-entry_point_true-unreach-call.cil.out.c:10504: 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 20947 states (over memory cap)
KLEE: WARNING: killing 14161 states (over memory cap)
KLEE: WARNING: killing 13903 states (over memory cap)
KLEE: WARNING: killing 13795 states (over memory cap)
KLEE: WARNING: killing 13164 states (over memory cap)
KLEE: WARNING: killing 13574 states (over memory cap)
KLEE: WARNING: killing 12808 states (over memory cap)
KLEE: WARNING: killing 13148 states (over memory cap)
KLEE: WARNING: killing 13635 states (over memory cap)
KLEE: WARNING: killing 14121 states (over memory cap)
KLEE: WARNING: killing 14754 states (over memory cap)
KLEE: WARNING: killing 14367 states (over memory cap)
KLEE: WARNING: killing 15660 states (over memory cap)
KLEE: WARNING: killing 15426 states (over memory cap)
KLEE: WARNING: killing 15332 states (over memory cap)
KLEE: WARNING: killing 15460 states (over memory cap)
KLEE: WARNING: killing 15293 states (over memory cap)
KLEE: WARNING: killing 15931 states (over memory cap)
KLEE: WARNING: killing 14462 states (over memory cap)
KLEE: WARNING: killing 15820 states (over memory cap)
KLEE: WARNING: killing 15439 states (over memory cap)
KLEE: WARNING: killing 14843 states (over memory cap)
KLEE: WARNING: killing 15113 states (over memory cap)
KLEE: WARNING: killing 15449 states (over memory cap)
KLEE: WARNING: killing 14568 states (over memory cap)
KLEE: WARNING: killing 14546 states (over memory cap)
KLEE: WARNING: killing 14816 states (over memory cap)
KLEE: WARNING: killing 14504 states (over memory cap)
KLEE: WARNING: killing 15060 states (over memory cap)
KLEE: WARNING: killing 14539 states (over memory cap)
KLEE: WARNING: killing 14305 states (over memory cap)
KLEE: WARNING: killing 14565 states (over memory cap)
KLEE: WARNING: killing 14333 states (over memory cap)
KLEE: WARNING: killing 14882 states (over memory cap)
KLEE: WARNING: killing 14935 states (over memory cap)
KLEE: WARNING: killing 14416 states (over memory cap)
KLEE: WARNING: killing 14613 states (over memory cap)
KLEE: WARNING: killing 14807 states (over memory cap)
KLEE: WARNING: killing 14650 states (over memory cap)
KLEE: WARNING: killing 14412 states (over memory cap)
KLEE: WARNING: killing 15458 states (over memory cap)
KLEE: WARNING: killing 15306 states (over memory cap)
KLEE: WARNING: killing 14867 states (over memory cap)
KLEE: WARNING: killing 15059 states (over memory cap)
KLEE: WARNING: killing 14829 states (over memory cap)
KLEE: WARNING: killing 15301 states (over memory cap)
KLEE: WARNING: killing 14652 states (over memory cap)
KLEE: WARNING: killing 15197 states (over memory cap)
KLEE: WARNING: killing 14973 states (over memory cap)
KLEE: WARNING: killing 14676 states (over memory cap)
KLEE: WARNING: killing 13889 states (over memory cap)
KLEE: WARNING: killing 15548 states (over memory cap)
KLEE: WARNING: killing 14272 states (over memory cap)
KLEE: WARNING: killing 15094 states (over memory cap)
KLEE: WARNING: killing 15075 states (over memory cap)
KLEE: WARNING: killing 14849 states (over memory cap)
KLEE: WARNING: killing 14490 states (over memory cap)
KLEE: WARNING: killing 15236 states (over memory cap)
KLEE: WARNING: killing 14732 states (over memory cap)
KLEE: WARNING: killing 14649 states (over memory cap)
KLEE: WARNING: killing 14285 states (over memory cap)
KLEE: WARNING: killing 15166 states (over memory cap)
KLEE: WARNING: killing 15006 states (over memory cap)
KLEE: WARNING: killing 14851 states (over memory cap)
KLEE: WARNING: killing 14980 states (over memory cap)
KLEE: WARNING: killing 14754 states (over memory cap)
KLEE: WARNING: killing 14674 states (over memory cap)
KLEE: WARNING: killing 14525 states (over memory cap)
KLEE: WARNING: killing 14922 states (over memory cap)
KLEE: WARNING: killing 14836 states (over memory cap)
KLEE: WARNING: killing 14889 states (over memory cap)
KLEE: WARNING: killing 15628 states (over memory cap)
KLEE: WARNING: killing 14719 states (over memory cap)
KLEE: WARNING: killing 14501 states (over memory cap)
KLEE: WARNING: killing 15098 states (over memory cap)
KLEE: WARNING: killing 14947 states (over memory cap)
KLEE: WARNING: killing 14458 states (over memory cap)
KLEE: WARNING: killing 15329 states (over memory cap)
KLEE: WARNING: killing 14229 states (over memory cap)
KLEE: WARNING: killing 15306 states (over memory cap)
KLEE: WARNING: killing 14746 states (over memory cap)
KLEE: WARNING: killing 14597 states (over memory cap)
KLEE: WARNING: killing 15392 states (over memory cap)
KLEE: WARNING: killing 14573 states (over memory cap)
KLEE: WARNING: killing 14626 states (over memory cap)
KLEE: WARNING: killing 15145 states (over memory cap)
KLEE: WARNING: killing 14527 states (over memory cap)
KLEE: WARNING: killing 14704 states (over memory cap)
KLEE: WARNING: killing 14695 states (over memory cap)
KLEE: WARNING: killing 15010 states (over memory cap)
KLEE: WARNING: killing 14261 states (over memory cap)
KLEE: WARNING: killing 15115 states (over memory cap)
KLEE: WARNING: killing 15040 states (over memory cap)
KLEE: WARNING: killing 15097 states (over memory cap)
KLEE: WARNING: killing 14610 states (over memory cap)
KLEE: WARNING: killing 14661 states (over memory cap)
KLEE: WARNING: killing 15123 states (over memory cap)
KLEE: WARNING: killing 14837 states (over memory cap)
KLEE: WARNING: killing 15093 states (over memory cap)
KLEE: WARNING: killing 14746 states (over memory cap)
KLEE: WARNING: killing 14601 states (over memory cap)
KLEE: WARNING: killing 14652 states (over memory cap)
KLEE: WARNING: killing 15373 states (over memory cap)
KLEE: WARNING: killing 15234 states (over memory cap)
KLEE: WARNING: killing 14748 states (over memory cap)
KLEE: WARNING: killing 15204 states (over memory cap)
KLEE: WARNING: killing 14995 states (over memory cap)
KLEE: WARNING: killing 14183 states (over memory cap)
KLEE: WARNING: killing 14565 states (over memory cap)
KLEE: WARNING: killing 15282 states (over memory cap)
KLEE: WARNING: killing 14543 states (over memory cap)
KLEE: WARNING: killing 14723 states (over memory cap)
KLEE: WARNING: killing 14514 states (over memory cap)
KLEE: WARNING: killing 14893 states (over memory cap)
KLEE: WARNING: killing 14488 states (over memory cap)
KLEE: WARNING: killing 15595 states (over memory cap)
KLEE: WARNING: killing 15057 states (over memory cap)
KLEE: WARNING: killing 14718 states (over memory cap)
KLEE: WARNING: killing 14312 states (over memory cap)
KLEE: WARNING: killing 14954 states (over memory cap)
KLEE: WARNING: killing 14483 states (over memory cap)
KLEE: WARNING: killing 15262 states (over memory cap)
KLEE: WARNING: killing 14853 states (over memory cap)
KLEE: WARNING: killing 14315 states (over memory cap)
KLEE: WARNING: killing 14558 states (over memory cap)
KLEE: WARNING: killing 14481 states (over memory cap)
KLEE: WARNING: killing 15189 states (over memory cap)
KLEE: WARNING: killing 15109 states (over memory cap)
KLEE: WARNING: killing 14768 states (over memory cap)
KLEE: WARNING: killing 14953 states (over memory cap)
KLEE: WARNING: killing 14815 states (over memory cap)
KLEE: WARNING: killing 15391 states (over memory cap)
KLEE: WARNING: killing 14601 states (over memory cap)
KLEE: WARNING: killing 14653 states (over memory cap)
KLEE: WARNING: killing 15157 states (over memory cap)
KLEE: WARNING: killing 14819 states (over memory cap)
KLEE: WARNING: killing 14030 states (over memory cap)
KLEE: WARNING: killing 14993 states (over memory cap)
KLEE: WARNING: killing 15041 states (over memory cap)
KLEE: WARNING: killing 15484 states (over memory cap)
KLEE: WARNING: killing 14692 states (over memory cap)
KLEE: WARNING: killing 14551 states (over memory cap)
KLEE: WARNING: killing 14735 states (over memory cap)
KLEE: WARNING: killing 14786 states (over memory cap)
KLEE: WARNING: killing 14836 states (over memory cap)
KLEE: WARNING: killing 15012 states (over memory cap)
KLEE: WARNING: killing 15137 states (over memory cap)
KLEE: WARNING: killing 15188 states (over memory cap)
KLEE: WARNING: killing 14790 states (over memory cap)
KLEE: WARNING: killing 14715 states (over memory cap)
KLEE: WARNING: killing 14901 states (over memory cap)
KLEE: WARNING: killing 14569 states (over memory cap)
KLEE: WARNING: killing 15449 states (over memory cap)
KLEE: WARNING: killing 14799 states (over memory cap)
KLEE: WARNING: killing 14656 states (over memory cap)
KLEE: WARNING: killing 14258 states (over memory cap)
KLEE: WARNING: killing 15643 states (over memory cap)
KLEE: WARNING: killing 14677 states (over memory cap)
KLEE: WARNING: killing 14543 states (over memory cap)
KLEE: WARNING: killing 14277 states (over memory cap)
KLEE: WARNING: killing 14644 states (over memory cap)
KLEE: WARNING: killing 14821 states (over memory cap)
KLEE: WARNING: killing 15136 states (over memory cap)
KLEE: WARNING: killing 15564 states (over memory cap)
KLEE: WARNING: killing 14726 states (over memory cap)
KLEE: WARNING: killing 14968 states (over memory cap)
KLEE: WARNING: killing 14893 states (over memory cap)
KLEE: WARNING: killing 14558 states (over memory cap)
KLEE: WARNING: killing 14806 states (over memory cap)
KLEE: WARNING: killing 14595 states (over memory cap)
KLEE: WARNING: killing 15086 states (over memory cap)
KLEE: WARNING: killing 14575 states (over memory cap)
KLEE: WARNING: killing 14625 states (over memory cap)
KLEE: WARNING: killing 15310 states (over memory cap)
KLEE: WARNING: killing 14921 states (over memory cap)
KLEE: WARNING: killing 15226 states (over memory cap)
KLEE: WARNING: killing 14964 states (over memory cap)
KLEE: WARNING: killing 14505 states (over memory cap)
KLEE: WARNING: killing 15242 states (over memory cap)
KLEE: WARNING: killing 14542 states (over memory cap)
KLEE: WARNING: killing 15156 states (over memory cap)
KLEE: WARNING: killing 14575 states (over memory cap)
KLEE: WARNING: killing 14750 states (over memory cap)
KLEE: WARNING: killing 14739 states (over memory cap)
KLEE: WARNING: killing 14972 states (over memory cap)
KLEE: WARNING: killing 15028 states (over memory cap)
KLEE: WARNING: killing 15018 states (over memory cap)
KLEE: WARNING: killing 14942 states (over memory cap)
KLEE: WARNING: killing 14739 states (over memory cap)
KLEE: WARNING: killing 14536 states (over memory cap)
KLEE: WARNING: killing 14404 states (over memory cap)
KLEE: WARNING: killing 14828 states (over memory cap)
KLEE: WARNING: killing 15247 states (over memory cap)
KLEE: WARNING: killing 14368 states (over memory cap)
KLEE: WARNING: killing 15157 states (over memory cap)
KLEE: WARNING: killing 15022 states (over memory cap)
KLEE: WARNING: killing 14518 states (over memory cap)
KLEE: WARNING: killing 14501 states (over memory cap)
KLEE: WARNING: killing 15412 states (over memory cap)
KLEE: WARNING: killing 14479 states (over memory cap)
KLEE: WARNING: killing 14891 states (over memory cap)
KLEE: WARNING: killing 14574 states (over memory cap)
KLEE: WARNING: killing 14986 states (over memory cap)
KLEE: WARNING: killing 14914 states (over memory cap)
