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--memstick--host--jmb38x_ms.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.: 80 104 886 5954
Removed infinite loop in sg_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 dma_map_sg_attrs
Removed infinite loop in dma_unmap_sg_attrs
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.289525985718
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'memstick_remove_host' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'memstick_free_host' (function is undefined)
Removed calls to 'memstick_suspend_host' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'memstick_resume_host' (function is undefined)
Removed calls to 'memstick_detect_change' (function is undefined)
Defining function pci_set_power_state as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Defining function __pci_enable_wake as symbolic
Removed calls to 'debug_dma_unmap_sg' (function is undefined)
Removed calls to 'debug_dma_map_sg' (function is undefined)
Defining function memstick_next_req as symbolic
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Defining function mod_timer as symbolic
Defining function sg_next as symbolic
Defining function del_timer as symbolic
Defining function pci_request_regions as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function dma_set_mask as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (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.329033851624
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 114 70 378 2537
INFO: Starting verification
KLEE: WARNING ONCE: function "jmb38x_ms_remove" has inline asm
KLEE: WARNING ONCE: function "jmb38x_ms_complete_cmd" has inline asm
KLEE: WARNING ONCE: function "sg_page" has inline asm
KLEE: WARNING ONCE: function "jmb38x_ms_transfer_data" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "jmb38x_ms_isr" 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_04db12f9-6446-4987-8136-14ee06ab2bad/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-c1eWtd/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--memstick--host--jmb38x_ms.ko-entry_point_true-unreach-call.cil.out.c:3031: 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 13335 states (over memory cap)
KLEE: WARNING: killing 17939 states (over memory cap)
KLEE: WARNING: killing 12585 states (over memory cap)
KLEE: WARNING: killing 17638 states (over memory cap)
KLEE: WARNING: killing 12342 states (over memory cap)
KLEE: WARNING: killing 12418 states (over memory cap)
KLEE: WARNING: killing 12132 states (over memory cap)
KLEE: WARNING: killing 12215 states (over memory cap)
KLEE: WARNING: killing 12172 states (over memory cap)
KLEE: WARNING: killing 12732 states (over memory cap)
KLEE: WARNING: killing 13051 states (over memory cap)
KLEE: WARNING: killing 13019 states (over memory cap)
KLEE: WARNING: killing 13218 states (over memory cap)
KLEE: WARNING: killing 13057 states (over memory cap)
KLEE: WARNING: killing 12557 states (over memory cap)
KLEE: WARNING: killing 13461 states (over memory cap)
KLEE: WARNING: killing 12956 states (over memory cap)
KLEE: WARNING: killing 13041 states (over memory cap)
KLEE: WARNING: killing 13361 states (over memory cap)
KLEE: WARNING: killing 13090 states (over memory cap)
KLEE: WARNING: killing 13295 states (over memory cap)
KLEE: WARNING: killing 12908 states (over memory cap)
KLEE: WARNING: killing 12880 states (over memory cap)
KLEE: WARNING: killing 13076 states (over memory cap)
KLEE: WARNING: killing 13153 states (over memory cap)
KLEE: WARNING: killing 13122 states (over memory cap)
KLEE: WARNING: killing 13089 states (over memory cap)
KLEE: WARNING: killing 13174 states (over memory cap)
KLEE: WARNING: killing 12682 states (over memory cap)
KLEE: WARNING: killing 13102 states (over memory cap)
KLEE: WARNING: killing 12955 states (over memory cap)
KLEE: WARNING: killing 12577 states (over memory cap)
KLEE: WARNING: killing 13230 states (over memory cap)
KLEE: WARNING: killing 12969 states (over memory cap)
KLEE: WARNING: killing 13274 states (over memory cap)
KLEE: WARNING: killing 13131 states (over memory cap)
KLEE: WARNING: killing 12986 states (over memory cap)
KLEE: WARNING: killing 13068 states (over memory cap)
KLEE: WARNING: killing 13038 states (over memory cap)
KLEE: WARNING: killing 13336 states (over memory cap)
KLEE: WARNING: killing 13315 states (over memory cap)
KLEE: WARNING: killing 13281 states (over memory cap)
KLEE: WARNING: killing 13257 states (over memory cap)
KLEE: WARNING: killing 13226 states (over memory cap)
KLEE: WARNING: killing 12977 states (over memory cap)
KLEE: WARNING: killing 13161 states (over memory cap)
KLEE: WARNING: killing 12692 states (over memory cap)
KLEE: WARNING: killing 12773 states (over memory cap)
KLEE: WARNING: killing 13286 states (over memory cap)
KLEE: WARNING: killing 13148 states (over memory cap)
KLEE: WARNING: killing 12901 states (over memory cap)
KLEE: WARNING: killing 12877 states (over memory cap)
KLEE: WARNING: killing 12957 states (over memory cap)
KLEE: WARNING: killing 13032 states (over memory cap)
KLEE: WARNING: killing 12790 states (over memory cap)
KLEE: WARNING: killing 13189 states (over memory cap)
KLEE: WARNING: killing 12523 states (over memory cap)
KLEE: WARNING: killing 13023 states (over memory cap)
KLEE: WARNING: killing 12676 states (over memory cap)
KLEE: WARNING: killing 13182 states (over memory cap)
KLEE: WARNING: killing 13155 states (over memory cap)
KLEE: WARNING: killing 13122 states (over memory cap)
KLEE: WARNING: killing 13101 states (over memory cap)
KLEE: WARNING: killing 13075 states (over memory cap)
KLEE: WARNING: killing 13040 states (over memory cap)
KLEE: WARNING: killing 12906 states (over memory cap)
KLEE: WARNING: killing 12982 states (over memory cap)
KLEE: WARNING: killing 13273 states (over memory cap)
KLEE: WARNING: killing 12826 states (over memory cap)
KLEE: WARNING: killing 12691 states (over memory cap)
KLEE: WARNING: killing 13077 states (over memory cap)
KLEE: WARNING: killing 13152 states (over memory cap)
KLEE: WARNING: killing 13026 states (over memory cap)
KLEE: WARNING: killing 13309 states (over memory cap)
KLEE: WARNING: killing 13181 states (over memory cap)
KLEE: WARNING: killing 12844 states (over memory cap)
KLEE: WARNING: killing 13226 states (over memory cap)
KLEE: WARNING: killing 12785 states (over memory cap)
KLEE: WARNING: killing 13074 states (over memory cap)
KLEE: WARNING: killing 13050 states (over memory cap)
KLEE: WARNING: killing 13122 states (over memory cap)
KLEE: WARNING: killing 13402 states (over memory cap)
KLEE: WARNING: killing 12766 states (over memory cap)
KLEE: WARNING: killing 13138 states (over memory cap)
KLEE: WARNING: killing 13016 states (over memory cap)
KLEE: WARNING: killing 12987 states (over memory cap)
KLEE: WARNING: killing 13065 states (over memory cap)
KLEE: WARNING: killing 12938 states (over memory cap)
KLEE: WARNING: killing 13113 states (over memory cap)
KLEE: WARNING: killing 12984 states (over memory cap)
KLEE: WARNING: killing 13061 states (over memory cap)
KLEE: WARNING: killing 12932 states (over memory cap)
KLEE: WARNING: killing 12910 states (over memory cap)
KLEE: WARNING: killing 12984 states (over memory cap)
KLEE: WARNING: killing 12762 states (over memory cap)
KLEE: WARNING: killing 12735 states (over memory cap)
KLEE: WARNING: killing 13109 states (over memory cap)
KLEE: WARNING: killing 13284 states (over memory cap)
KLEE: WARNING: killing 12663 states (over memory cap)
KLEE: WARNING: killing 12834 states (over memory cap)
KLEE: WARNING: killing 13211 states (over memory cap)
KLEE: WARNING: killing 13378 states (over memory cap)
KLEE: WARNING: killing 13064 states (over memory cap)
KLEE: WARNING: killing 13137 states (over memory cap)
KLEE: WARNING: killing 13007 states (over memory cap)
KLEE: WARNING: killing 12985 states (over memory cap)
KLEE: WARNING: killing 12962 states (over memory cap)
KLEE: WARNING: killing 12645 states (over memory cap)
KLEE: WARNING: killing 12620 states (over memory cap)
KLEE: WARNING: killing 12887 states (over memory cap)
KLEE: WARNING: killing 12959 states (over memory cap)
KLEE: WARNING: killing 12836 states (over memory cap)
KLEE: WARNING: killing 12909 states (over memory cap)
KLEE: WARNING: killing 12891 states (over memory cap)
KLEE: WARNING: killing 12962 states (over memory cap)
KLEE: WARNING: killing 13033 states (over memory cap)
KLEE: WARNING: killing 12913 states (over memory cap)
KLEE: WARNING: killing 13271 states (over memory cap)
