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--scsi--3w-9xxx.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.: 328 197 1672 9986
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.424661159515
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'scsi_scan_host' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'scsi_remove_host' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'scsi_host_put' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Defining function printk as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function pci_bus_write_config_word as symbolic
Defining function pci_set_power_state as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_try_set_mwi as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'scsi_dma_unmap' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function pci_enable_msi_range as symbolic
Defining function request_threaded_irq as symbolic
Defining function sg_copy_from_buffer as symbolic
Defining function sprintf as symbolic
Defining function scsi_dma_map as symbolic
Defining function sg_next as symbolic
Defining function sg_copy_to_buffer as symbolic
Defining function strlcpy as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Defining function __pci_enable_wake as symbolic
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function pci_request_regions as symbolic
Defining function __register_chrdev as symbolic
Defining function scsi_add_host_with_dma as symbolic
Defining function ioremap_nocache as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function scsi_host_alloc as symbolic
Removed calls to 'scsi_cmd_get_serial' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'sdev_prefix_printk' (function is undefined)
Removed calls to 'blk_queue_rq_timeout' (function is undefined)
Defining function scsi_change_queue_depth as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function snprintf as symbolic
Defining function noop_llseek as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Defining function mutex_lock_interruptible as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ldv_suspend_late_3 as symbolic
Defining function ldv_resume_early_3 as symbolic
Defining function ldv_release_5 as symbolic
Defining function __pci_register_driver as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strlen
  __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.425070047379
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 409 183 1064 5612
INFO: Starting verification
KLEE: WARNING ONCE: function "twa_probe" has inline asm
KLEE: WARNING ONCE: function "twa_suspend" has inline asm
KLEE: WARNING ONCE: function "twa_resume" has inline asm
KLEE: WARNING ONCE: function "__twa_shutdown" has inline asm
KLEE: WARNING ONCE: function "twa_post_command_packet" has inline asm
KLEE: WARNING ONCE: function "twa_poll_response" has inline asm
KLEE: WARNING ONCE: function "twa_decode_bits" has inline asm
KLEE: WARNING ONCE: function "twa_reset_sequence" has inline asm
KLEE: WARNING ONCE: function "twa_interrupt" has inline asm
KLEE: WARNING ONCE: function "twa_reset_device_extension" 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_b05801a7-6fa9-4251-b9e6-e950df094e10/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gGqaMh/linux-4.2-rc1.tar.xz-32_7a-drivers--scsi--3w-9xxx.ko-entry_point_true-unreach-call.cil.out.c:5527: 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 10326 states (over memory cap)
KLEE: WARNING: killing 17647 states (over memory cap)
KLEE: WARNING: killing 17177 states (over memory cap)
KLEE: WARNING: killing 17395 states (over memory cap)
KLEE: WARNING: killing 17326 states (over memory cap)
KLEE: WARNING: killing 17253 states (over memory cap)
KLEE: WARNING: killing 18055 states (over memory cap)
KLEE: WARNING: killing 18078 states (over memory cap)
KLEE: WARNING: killing 9912 states (over memory cap)
KLEE: WARNING: killing 9611 states (over memory cap)
KLEE: WARNING: killing 18242 states (over memory cap)
KLEE: WARNING: killing 9757 states (over memory cap)
KLEE: WARNING: killing 9933 states (over memory cap)
KLEE: WARNING: killing 9919 states (over memory cap)
KLEE: WARNING: killing 9526 states (over memory cap)
KLEE: WARNING: killing 9607 states (over memory cap)
KLEE: WARNING: killing 18836 states (over memory cap)
KLEE: WARNING: killing 9948 states (over memory cap)
KLEE: WARNING: killing 18374 states (over memory cap)
KLEE: WARNING: killing 9620 states (over memory cap)
KLEE: WARNING: killing 18579 states (over memory cap)
KLEE: WARNING: killing 9582 states (over memory cap)
KLEE: WARNING: killing 9566 states (over memory cap)
KLEE: WARNING: killing 18009 states (over memory cap)
KLEE: WARNING: killing 9623 states (over memory cap)
KLEE: WARNING: killing 9515 states (over memory cap)
KLEE: WARNING: killing 9316 states (over memory cap)
KLEE: WARNING: killing 17799 states (over memory cap)
KLEE: WARNING: killing 9368 states (over memory cap)
KLEE: WARNING: killing 17536 states (over memory cap)
KLEE: WARNING: killing 9515 states (over memory cap)
KLEE: WARNING: killing 17561 states (over memory cap)
KLEE: WARNING: killing 9382 states (over memory cap)
KLEE: WARNING: killing 9278 states (over memory cap)
KLEE: WARNING: killing 17642 states (over memory cap)
KLEE: WARNING: killing 9241 states (over memory cap)
KLEE: WARNING: killing 17672 states (over memory cap)
KLEE: WARNING: killing 9655 states (over memory cap)
KLEE: WARNING: killing 9193 states (over memory cap)
KLEE: WARNING: killing 9182 states (over memory cap)
KLEE: WARNING: killing 9445 states (over memory cap)
KLEE: WARNING: killing 9431 states (over memory cap)
KLEE: WARNING: killing 9332 states (over memory cap)
KLEE: WARNING: killing 9054 states (over memory cap)
KLEE: WARNING: killing 9131 states (over memory cap)
KLEE: WARNING: killing 9207 states (over memory cap)
KLEE: WARNING: killing 9374 states (over memory cap)
KLEE: WARNING: killing 9187 states (over memory cap)
KLEE: WARNING: killing 9264 states (over memory cap)
KLEE: WARNING: killing 8985 states (over memory cap)
KLEE: WARNING: killing 9246 states (over memory cap)
KLEE: WARNING: killing 8968 states (over memory cap)
KLEE: WARNING: killing 9313 states (over memory cap)
KLEE: WARNING: killing 9213 states (over memory cap)
KLEE: WARNING: killing 9115 states (over memory cap)
KLEE: WARNING: killing 8927 states (over memory cap)
KLEE: WARNING: killing 9358 states (over memory cap)
KLEE: WARNING: killing 9086 states (over memory cap)
KLEE: WARNING: killing 9251 states (over memory cap)
KLEE: WARNING: killing 9247 states (over memory cap)
KLEE: WARNING: killing 9501 states (over memory cap)
KLEE: WARNING: killing 8961 states (over memory cap)
KLEE: WARNING: killing 9126 states (over memory cap)
KLEE: WARNING: killing 8939 states (over memory cap)
KLEE: WARNING: killing 9631 states (over memory cap)
KLEE: WARNING: killing 9185 states (over memory cap)
KLEE: WARNING: killing 9086 states (over memory cap)
KLEE: WARNING: killing 8899 states (over memory cap)
KLEE: WARNING: killing 17566 states (over memory cap)
KLEE: WARNING: killing 9747 states (over memory cap)
KLEE: WARNING: killing 9559 states (over memory cap)
KLEE: WARNING: killing 9116 states (over memory cap)
KLEE: WARNING: killing 9018 states (over memory cap)
KLEE: WARNING: killing 9097 states (over memory cap)
KLEE: WARNING: killing 9261 states (over memory cap)
KLEE: WARNING: killing 9516 states (over memory cap)
KLEE: WARNING: killing 9156 states (over memory cap)
KLEE: WARNING: killing 9409 states (over memory cap)
KLEE: WARNING: killing 9050 states (over memory cap)
KLEE: WARNING: killing 8951 states (over memory cap)
KLEE: WARNING: killing 9204 states (over memory cap)
KLEE: WARNING: killing 9711 states (over memory cap)
KLEE: WARNING: killing 8927 states (over memory cap)
KLEE: WARNING: killing 8914 states (over memory cap)
KLEE: WARNING: killing 8992 states (over memory cap)
KLEE: WARNING: killing 9158 states (over memory cap)
KLEE: WARNING: killing 9150 states (over memory cap)
KLEE: WARNING: killing 9483 states (over memory cap)
KLEE: WARNING: killing 9390 states (over memory cap)
KLEE: WARNING: killing 8862 states (over memory cap)
KLEE: WARNING: killing 9025 states (over memory cap)
KLEE: WARNING: killing 9447 states (over memory cap)
KLEE: WARNING: killing 9180 states (over memory cap)
KLEE: WARNING: killing 9085 states (over memory cap)
KLEE: WARNING: killing 9074 states (over memory cap)
KLEE: WARNING: killing 9664 states (over memory cap)
KLEE: WARNING: killing 9485 states (over memory cap)
KLEE: WARNING: killing 8963 states (over memory cap)
KLEE: WARNING: killing 8871 states (over memory cap)
KLEE: WARNING: killing 8945 states (over memory cap)
KLEE: WARNING: killing 9270 states (over memory cap)
KLEE: WARNING: killing 9008 states (over memory cap)
KLEE: WARNING: killing 9084 states (over memory cap)
KLEE: WARNING: killing 9579 states (over memory cap)
KLEE: WARNING: killing 9407 states (over memory cap)
KLEE: WARNING: killing 9058 states (over memory cap)
KLEE: WARNING: killing 9389 states (over memory cap)
KLEE: WARNING: killing 9548 states (over memory cap)
KLEE: WARNING: killing 9120 states (over memory cap)
KLEE: WARNING: killing 9028 states (over memory cap)
KLEE: WARNING: killing 9017 states (over memory cap)
KLEE: WARNING: killing 9090 states (over memory cap)
KLEE: WARNING: killing 9337 states (over memory cap)
KLEE: WARNING: killing 9076 states (over memory cap)
KLEE: WARNING: killing 8983 states (over memory cap)
KLEE: WARNING: killing 9390 states (over memory cap)
KLEE: WARNING: killing 9052 states (over memory cap)
KLEE: WARNING: killing 8957 states (over memory cap)
KLEE: WARNING: killing 9117 states (over memory cap)
KLEE: WARNING: killing 9027 states (over memory cap)
KLEE: WARNING: killing 9189 states (over memory cap)
KLEE: WARNING: killing 9180 states (over memory cap)
KLEE: WARNING: killing 9503 states (over memory cap)
KLEE: WARNING: killing 9081 states (over memory cap)
KLEE: WARNING: killing 8818 states (over memory cap)
KLEE: WARNING: killing 8973 states (over memory cap)
KLEE: WARNING: killing 9297 states (over memory cap)
KLEE: WARNING: killing 9124 states (over memory cap)
KLEE: WARNING: killing 9116 states (over memory cap)
KLEE: WARNING: killing 9358 states (over memory cap)
KLEE: WARNING: killing 9513 states (over memory cap)
KLEE: WARNING: killing 9173 states (over memory cap)
KLEE: WARNING: killing 9170 states (over memory cap)
KLEE: WARNING: killing 9076 states (over memory cap)
KLEE: WARNING: killing 8904 states (over memory cap)
KLEE: WARNING: killing 9309 states (over memory cap)
KLEE: WARNING: killing 9217 states (over memory cap)
KLEE: WARNING: killing 8880 states (over memory cap)
KLEE: WARNING: killing 8955 states (over memory cap)
KLEE: WARNING: killing 9023 states (over memory cap)
KLEE: WARNING: killing 9018 states (over memory cap)
KLEE: WARNING: killing 9011 states (over memory cap)
KLEE: WARNING: killing 9248 states (over memory cap)
KLEE: WARNING: killing 8915 states (over memory cap)
KLEE: WARNING: killing 9231 states (over memory cap)
KLEE: WARNING: killing 9549 states (over memory cap)
KLEE: WARNING: killing 9375 states (over memory cap)
KLEE: WARNING: killing 8882 states (over memory cap)
KLEE: WARNING: killing 9442 states (over memory cap)
KLEE: WARNING: killing 9274 states (over memory cap)
KLEE: WARNING: killing 9592 states (over memory cap)
KLEE: WARNING: killing 9017 states (over memory cap)
KLEE: WARNING: killing 8930 states (over memory cap)
KLEE: WARNING: killing 8839 states (over memory cap)
KLEE: WARNING: killing 9152 states (over memory cap)
KLEE: WARNING: killing 9392 states (over memory cap)
KLEE: WARNING: killing 9138 states (over memory cap)
KLEE: WARNING: killing 9128 states (over memory cap)
KLEE: WARNING: killing 8961 states (over memory cap)
KLEE: WARNING: killing 8872 states (over memory cap)
KLEE: WARNING: killing 9424 states (over memory cap)
KLEE: WARNING: killing 9419 states (over memory cap)
KLEE: WARNING: killing 9091 states (over memory cap)
KLEE: WARNING: killing 9000 states (over memory cap)
KLEE: WARNING: killing 8910 states (over memory cap)
KLEE: WARNING: killing 9220 states (over memory cap)
KLEE: WARNING: killing 9293 states (over memory cap)
KLEE: WARNING: killing 9126 states (over memory cap)
KLEE: WARNING: killing 8879 states (over memory cap)
KLEE: WARNING: killing 9351 states (over memory cap)
KLEE: WARNING: killing 9101 states (over memory cap)
KLEE: WARNING: killing 8933 states (over memory cap)
KLEE: WARNING: killing 9481 states (over memory cap)
KLEE: WARNING: killing 9391 states (over memory cap)
KLEE: WARNING: killing 9065 states (over memory cap)
KLEE: WARNING: killing 9378 states (over memory cap)
KLEE: WARNING: killing 9367 states (over memory cap)
KLEE: WARNING: killing 9043 states (over memory cap)
KLEE: WARNING: killing 9351 states (over memory cap)
KLEE: WARNING: killing 9266 states (over memory cap)
KLEE: WARNING: killing 9499 states (over memory cap)
KLEE: WARNING: killing 9333 states (over memory cap)
KLEE: WARNING: killing 8849 states (over memory cap)
KLEE: WARNING: killing 9076 states (over memory cap)
KLEE: WARNING: killing 9149 states (over memory cap)
KLEE: WARNING: killing 9613 states (over memory cap)
KLEE: WARNING: killing 9290 states (over memory cap)
KLEE: WARNING: killing 8655 states (over memory cap)
KLEE: WARNING: killing 9114 states (over memory cap)
KLEE: WARNING: killing 8947 states (over memory cap)
KLEE: WARNING: killing 8863 states (over memory cap)
KLEE: WARNING: killing 9564 states (over memory cap)
KLEE: WARNING: killing 9320 states (over memory cap)
KLEE: WARNING: killing 8997 states (over memory cap)
KLEE: WARNING: killing 8988 states (over memory cap)
KLEE: WARNING: killing 8903 states (over memory cap)
KLEE: WARNING: killing 9049 states (over memory cap)
KLEE: WARNING: killing 8885 states (over memory cap)
KLEE: WARNING: killing 9110 states (over memory cap)
KLEE: WARNING: killing 9098 states (over memory cap)
KLEE: WARNING: killing 9323 states (over memory cap)
KLEE: WARNING: killing 9237 states (over memory cap)
KLEE: WARNING: killing 9309 states (over memory cap)
KLEE: WARNING: killing 9302 states (over memory cap)
KLEE: WARNING: killing 9137 states (over memory cap)
KLEE: WARNING: killing 8972 states (over memory cap)
KLEE: WARNING: killing 9275 states (over memory cap)
KLEE: WARNING: killing 9192 states (over memory cap)
KLEE: WARNING: killing 9263 states (over memory cap)
KLEE: WARNING: killing 9256 states (over memory cap)
KLEE: WARNING: killing 9250 states (over memory cap)
KLEE: WARNING: killing 9398 states (over memory cap)
KLEE: WARNING: killing 9159 states (over memory cap)
KLEE: WARNING: killing 9156 states (over memory cap)
KLEE: WARNING: killing 9300 states (over memory cap)
KLEE: WARNING: killing 9215 states (over memory cap)
KLEE: WARNING: killing 9055 states (over memory cap)
KLEE: WARNING: killing 9274 states (over memory cap)
KLEE: WARNING: killing 9115 states (over memory cap)
KLEE: WARNING: killing 9109 states (over memory cap)
KLEE: WARNING: killing 9023 states (over memory cap)
KLEE: WARNING: killing 8933 states (over memory cap)
KLEE: WARNING: killing 8697 states (over memory cap)
KLEE: WARNING: killing 9300 states (over memory cap)
KLEE: WARNING: killing 8683 states (over memory cap)
KLEE: WARNING: killing 9056 states (over memory cap)
KLEE: WARNING: killing 9046 states (over memory cap)
KLEE: WARNING: killing 9187 states (over memory cap)
KLEE: WARNING: killing 9105 states (over memory cap)
KLEE: WARNING: killing 9481 states (over memory cap)
KLEE: WARNING: killing 9322 states (over memory cap)
KLEE: WARNING: killing 9012 states (over memory cap)
KLEE: WARNING: killing 9304 states (over memory cap)
