bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.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.: 32 78 530 4477
Removed infinite loop in pdc20621_qc_issue
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.238411903381
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'ata_sff_error_handler' (function is undefined)
Removed calls to 'ata_sff_tf_load' (function is undefined)
Removed calls to 'ata_sff_exec_command' (function is undefined)
Defining function ioread8 as symbolic
Defining function dmam_alloc_coherent as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function ata_sff_softreset as symbolic
Defining function ata_sff_qc_issue as symbolic
Defining function sg_next as symbolic
Defining function ata_scsi_ioctl as symbolic
Defining function ata_scsi_queuecmd as symbolic
Defining function ata_scsi_slave_config as symbolic
Defining function ata_std_bios_param as symbolic
Removed calls to 'ata_print_version' (function is undefined)
Removed calls to 'pcim_pin_device' (function is undefined)
Removed calls to 'ata_port_pbar_desc' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Defining function ata_host_alloc_pinfo as symbolic
Defining function pcim_enable_device as symbolic
Defining function pcim_iomap_regions as symbolic
Defining function pcim_iomap_table as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'ata_qc_complete' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function ata_host_activate as symbolic
Defining function printk as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ata_pci_remove_one' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'ata_scsi_slave_destroy' (function is undefined)
Removed calls to 'ata_scsi_unlock_native_capacity' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function __pci_register_driver as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  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.272633075714
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 82 72 296 2501
INFO: Starting verification
KLEE: WARNING ONCE: function "pdc20621_qc_prep" has inline asm
KLEE: WARNING ONCE: function "pdc20621_qc_issue" has inline asm
KLEE: WARNING ONCE: function "pdc_freeze" has inline asm
KLEE: WARNING ONCE: function "pdc_thaw" has inline asm
KLEE: WARNING ONCE: function "pdc_reset_port" has inline asm
KLEE: WARNING ONCE: function "pdc20621_push_hdma" has inline asm
KLEE: WARNING ONCE: function "pdc_sata_init_one" has inline asm
KLEE: WARNING ONCE: function "pdc20621_i2c_read" has inline asm
KLEE: WARNING ONCE: function "pdc20621_interrupt" has inline asm
KLEE: WARNING ONCE: function "pdc20621_pop_hdma" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING: undefined reference to function: ata_pci_remove_one
KLEE: WARNING: undefined reference to function: ata_scsi_slave_destroy
KLEE: WARNING: undefined reference to function: ata_scsi_unlock_native_capacity
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_7976106d-efbe-4756-ad0d-c75c00c76ddc/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:5408: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6030: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:5967: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:5794: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6055: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:5671: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:5982: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6121: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6040: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12528 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:5883: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13374 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6102: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13411 states (over memory cap)
KLEE: WARNING: killing 13543 states (over memory cap)
KLEE: WARNING: killing 13683 states (over memory cap)
KLEE: WARNING: killing 14126 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6534: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13984 states (over memory cap)
KLEE: WARNING: killing 9911 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6551: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14416 states (over memory cap)
KLEE: WARNING: killing 10854 states (over memory cap)
KLEE: WARNING: killing 10941 states (over memory cap)
KLEE: WARNING: killing 11213 states (over memory cap)
KLEE: WARNING: killing 10706 states (over memory cap)
KLEE: WARNING: killing 11272 states (over memory cap)
KLEE: WARNING: killing 11938 states (over memory cap)
KLEE: WARNING: killing 12219 states (over memory cap)
KLEE: WARNING: killing 11912 states (over memory cap)
KLEE: WARNING: killing 12089 states (over memory cap)
KLEE: WARNING: killing 11588 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6908: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11959 states (over memory cap)
KLEE: WARNING: killing 12039 states (over memory cap)
KLEE: WARNING: killing 11934 states (over memory cap)
KLEE: WARNING: killing 12405 states (over memory cap)
KLEE: WARNING: killing 12200 states (over memory cap)
KLEE: WARNING: killing 12671 states (over memory cap)
KLEE: WARNING: killing 12557 states (over memory cap)
KLEE: WARNING: killing 12636 states (over memory cap)
KLEE: WARNING: killing 12715 states (over memory cap)
KLEE: WARNING: killing 12217 states (over memory cap)
KLEE: WARNING: killing 12574 states (over memory cap)
KLEE: WARNING: killing 12932 states (over memory cap)
KLEE: WARNING: killing 12721 states (over memory cap)
KLEE: WARNING: killing 12796 states (over memory cap)
KLEE: WARNING: killing 13060 states (over memory cap)
KLEE: WARNING: killing 12849 states (over memory cap)
KLEE: WARNING: killing 13582 states (over memory cap)
KLEE: WARNING: killing 12992 states (over memory cap)
KLEE: WARNING: killing 13155 states (over memory cap)
KLEE: WARNING: killing 12570 states (over memory cap)
KLEE: WARNING: killing 13015 states (over memory cap)
KLEE: WARNING: killing 13176 states (over memory cap)
KLEE: WARNING: killing 13059 states (over memory cap)
KLEE: WARNING: killing 12934 states (over memory cap)
KLEE: WARNING: killing 13284 states (over memory cap)
KLEE: WARNING: killing 13262 states (over memory cap)
KLEE: WARNING: killing 13430 states (over memory cap)
KLEE: WARNING: killing 13307 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-bGTKEt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--ata--sata_sx4.ko-entry_point_true-unreach-call.cil.out.c:6569: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12913 states (over memory cap)
KLEE: WARNING: killing 13076 states (over memory cap)
KLEE: WARNING: killing 13331 states (over memory cap)
KLEE: WARNING: killing 13395 states (over memory cap)
KLEE: WARNING: killing 13467 states (over memory cap)
KLEE: WARNING: killing 13344 states (over memory cap)
KLEE: WARNING: killing 13508 states (over memory cap)
KLEE: WARNING: killing 13384 states (over memory cap)
KLEE: WARNING: killing 13633 states (over memory cap)
KLEE: WARNING: killing 13335 states (over memory cap)
KLEE: WARNING: killing 13670 states (over memory cap)
KLEE: WARNING: killing 13740 states (over memory cap)
KLEE: WARNING: killing 13536 states (over memory cap)
KLEE: WARNING: killing 13690 states (over memory cap)
KLEE: WARNING: killing 13484 states (over memory cap)
KLEE: WARNING: killing 13547 states (over memory cap)
KLEE: WARNING: killing 13429 states (over memory cap)
KLEE: WARNING: killing 13311 states (over memory cap)
KLEE: WARNING: killing 13638 states (over memory cap)
KLEE: WARNING: killing 13159 states (over memory cap)
KLEE: WARNING: killing 13679 states (over memory cap)
KLEE: WARNING: killing 13376 states (over memory cap)
KLEE: WARNING: killing 13269 states (over memory cap)
KLEE: WARNING: killing 13600 states (over memory cap)
KLEE: WARNING: killing 13663 states (over memory cap)
KLEE: WARNING: killing 13994 states (over memory cap)
KLEE: WARNING: killing 14243 states (over memory cap)
KLEE: WARNING: killing 13682 states (over memory cap)
KLEE: WARNING: killing 13741 states (over memory cap)
KLEE: WARNING: killing 12929 states (over memory cap)
KLEE: WARNING: killing 13610 states (over memory cap)
KLEE: WARNING: killing 13671 states (over memory cap)
KLEE: WARNING: killing 13648 states (over memory cap)
KLEE: WARNING: killing 13624 states (over memory cap)
