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-08_1a-drivers--scsi--esas2r--esas2r.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.: 335 413 4473 32169
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.24158811569
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'up' (function is undefined)
Defining function down_interruptible as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function dma_alloc_attrs as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Removed calls to '__list_add' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function snprintf as symbolic
Defining function vsnprintf as symbolic
Defining function printk as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'print_hex_dump' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'scsi_remove_device' (function is undefined)
Removed calls to 'scsi_device_put' (function is undefined)
Defining function scsi_device_lookup as symbolic
Defining function scsi_add_device as symbolic
Defining function scsi_device_set_state as symbolic
Defining function sprintf as symbolic
Removed calls to 'scsi_dma_unmap' (function is undefined)
Defining function pci_find_capability as symbolic
Removed calls to '__tasklet_hi_schedule' (function is undefined)
Defining function pci_bus_read_config_dword as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function jiffies_to_msecs as symbolic
Removed calls to '__might_fault' (function is undefined)
Defining function copy_user_generic_unrolled as symbolic
Defining function copy_user_generic_string as symbolic
Defining function copy_user_enhanced_fast_string as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'scsi_unregister' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function scsi_change_queue_depth as symbolic
Defining function seq_printf as symbolic
Defining function seq_puts as symbolic
Defining function seq_putc as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function scsi_dma_map as symbolic
Defining function sg_next as symbolic
Defining function proc_create_data as symbolic
Defining function __register_chrdev as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'scsi_remove_host' (function is undefined)
Removed calls to 'scsi_host_put' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'sysfs_remove_bin_file' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'pci_release_region' (function is undefined)
Defining function schedule_timeout_interruptible as symbolic
Defining function del_timer_sync as symbolic
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'scsi_scan_host' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Defining function pci_set_power_state as symbolic
Defining function pci_enable_device as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to 'scsi_report_bus_reset' (function is undefined)
Removed calls to 'do_gettimeofday' (function is undefined)
Defining function pci_bus_write_config_word as symbolic
Defining function pci_enable_msi_range as symbolic
Defining function pci_request_region as symbolic
Defining function ioremap_nocache as symbolic
Defining function __pci_enable_wake as symbolic
Defining function pci_choose_state as symbolic
Defining function pci_save_state as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Defining function sysfs_create_bin_file as symbolic
Defining function scsi_add_host_with_dma as symbolic
Defining function dma_get_required_mask as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Defining function scsi_host_alloc as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ldv_release_6 as symbolic
Defining function ldv_probe_6 as symbolic
Defining function ldv_release_11 as symbolic
Defining function ldv_probe_11 as symbolic
Defining function ldv_open_3 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_release_7 as symbolic
Defining function ldv_probe_7 as symbolic
Defining function ldv_release_9 as symbolic
Defining function ldv_probe_9 as symbolic
Defining function ldv_release_8 as symbolic
Defining function ldv_probe_8 as symbolic
Defining function ldv_suspend_late_4 as symbolic
Defining function ldv_resume_early_4 as symbolic
Defining function ldv_shutdown_4 as symbolic
Defining function ldv_release_10 as symbolic
Defining function ldv_probe_10 as symbolic
Defining function ldv_probe_5 as symbolic
Defining function __pci_register_driver as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  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: 1.25630497932
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 511 385 2629 18791
INFO: Starting verification
KLEE: WARNING ONCE: function "esas2r_fm_api" has inline asm
KLEE: WARNING ONCE: function "esas2r_enable_heartbeat" has inline asm
KLEE: WARNING ONCE: function "complete_fmapi_req" has inline asm
KLEE: WARNING ONCE: function "fw_download_proc" has inline asm
KLEE: WARNING ONCE: function "esas2r_complete_request" has inline asm
KLEE: WARNING ONCE: function "esas2r_local_start_request" has inline asm
KLEE: WARNING ONCE: function "esas2r_start_vda_request" has inline asm
KLEE: WARNING ONCE: function "esas2r_queue_fw_event" has inline asm
KLEE: WARNING ONCE: function "esas2r_process_fs_ioctl" has inline asm
KLEE: WARNING ONCE: function "hba_ioctl_callback" has inline asm
KLEE: WARNING ONCE: function "esas2r_reset_adapter" has inline asm
KLEE: WARNING ONCE: function "esas2r_schedule_tasklet" has inline asm
KLEE: WARNING ONCE: function "esas2r_nvram_write" has inline asm
KLEE: WARNING ONCE: function "esas2r_nvram_callback" has inline asm
KLEE: WARNING ONCE: function "esas2r_nvram_validate" has inline asm
KLEE: WARNING ONCE: function "esas2r_nvram_set_defaults" has inline asm
KLEE: WARNING ONCE: function "esas2r_ioctl_handler" has inline asm
KLEE: WARNING ONCE: function "esas2r_reset_bus" has inline asm
KLEE: WARNING ONCE: function "esas2r_do_deferred_processes" has inline asm
KLEE: WARNING ONCE: function "esas2r_kill_adapter" has inline asm
KLEE: WARNING ONCE: function "esas2r_adapter_power_down" has inline asm
KLEE: WARNING ONCE: function "esas2r_power_down" has inline asm
KLEE: WARNING ONCE: function "esas2r_process_adapter_reset" has inline asm
KLEE: WARNING ONCE: function "esas2r_process_bus_reset" has inline asm
KLEE: WARNING ONCE: function "esas2r_resume" has inline asm
KLEE: WARNING ONCE: function "esas2r_setup_interrupts" has inline asm
KLEE: WARNING ONCE: function "esas2r_power_up" has inline asm
KLEE: WARNING ONCE: function "esas2r_claim_interrupts" has inline asm
KLEE: WARNING ONCE: function "esas2r_timer_callback" has inline asm
KLEE: WARNING ONCE: function "esas2r_interrupt" has inline asm
KLEE: WARNING ONCE: function "esas2r_msi_interrupt" has inline asm
KLEE: WARNING ONCE: function "esas2r_get_outbound_responses" has inline asm
KLEE: WARNING ONCE: function "esas2r_doorbell_interrupt" has inline asm
KLEE: WARNING ONCE: function "esas2r_do_tasklet_tasks" has inline asm
KLEE: WARNING ONCE: function "esas2r_reset_chip" has inline asm
KLEE: WARNING ONCE: function "esas2r_check_adapter" has inline asm
KLEE: WARNING ONCE: function "esas2r_init_adapter_hw" has inline asm
KLEE: WARNING ONCE: function "esas2r_disc_initialize" has inline asm
KLEE: WARNING ONCE: function "esas2r_disc_check_for_work" has inline asm
KLEE: WARNING ONCE: function "esas2r_timer_tick" has inline asm
KLEE: WARNING ONCE: function "esas2r_disc_start_port" has inline asm
KLEE: WARNING ONCE: function "esas2r_disc_continue" has inline asm
KLEE: WARNING ONCE: function "esas2r_disc_check_complete" has inline asm
KLEE: WARNING ONCE: function "esas2r_polled_interrupt" has inline asm
KLEE: WARNING ONCE: function "esas2r_wait_request" has inline asm
KLEE: WARNING ONCE: function "esas2r_read_flash_block" has inline asm
KLEE: WARNING ONCE: function "esas2r_flash_access" has inline asm
KLEE: WARNING ONCE: function "esas2r_read_mem_block" has inline asm
KLEE: WARNING ONCE: function "esas2r_init_adapter" has inline asm
KLEE: WARNING ONCE: function "esas2r_set_degraded_mode" has inline asm
KLEE: WARNING ONCE: function "esas2r_force_interrupt" has inline asm
KLEE: WARNING ONCE: function "esas2r_map_data_window" has inline asm
KLEE: WARNING ONCE: function "esas2r_is_adapter_present" has inline asm
KLEE: WARNING ONCE: function "esas2r_adapter_tasklet" has inline asm
KLEE: WARNING ONCE: function "esas2r_adapter_interrupt" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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_eeab17aa-df71-4587-9c13-967776ce2e1b/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 20493 states (over memory cap)
KLEE: WARNING: killing 14851 states (over memory cap)
KLEE: WARNING: killing 14917 states (over memory cap)
KLEE: WARNING: killing 14471 states (over memory cap)
KLEE: WARNING: killing 14387 states (over memory cap)
KLEE: WARNING: killing 14563 states (over memory cap)
KLEE: WARNING: killing 14539 states (over memory cap)
KLEE: WARNING: killing 14503 states (over memory cap)
KLEE: WARNING: killing 15410 states (over memory cap)
KLEE: WARNING: killing 15700 states (over memory cap)
KLEE: WARNING: killing 16501 states (over memory cap)
KLEE: WARNING: killing 16172 states (over memory cap)
KLEE: WARNING: killing 16616 states (over memory cap)
KLEE: WARNING: killing 15872 states (over memory cap)
KLEE: WARNING: killing 16469 states (over memory cap)
KLEE: WARNING: killing 15636 states (over memory cap)
KLEE: WARNING: killing 16534 states (over memory cap)
KLEE: WARNING: killing 16621 states (over memory cap)
KLEE: WARNING: killing 15120 states (over memory cap)
KLEE: WARNING: killing 15455 states (over memory cap)
KLEE: WARNING: killing 15844 states (over memory cap)
KLEE: WARNING: killing 15621 states (over memory cap)
KLEE: WARNING: killing 16108 states (over memory cap)
KLEE: WARNING: killing 15789 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15665 states (over memory cap)
KLEE: WARNING: killing 15749 states (over memory cap)
KLEE: WARNING: killing 16139 states (over memory cap)
KLEE: WARNING: killing 16271 states (over memory cap)
KLEE: WARNING: killing 15695 states (over memory cap)
KLEE: WARNING: killing 16789 states (over memory cap)
KLEE: WARNING: killing 15666 states (over memory cap)
KLEE: WARNING: killing 16204 states (over memory cap)
KLEE: WARNING: killing 15732 states (over memory cap)
KLEE: WARNING: killing 15812 states (over memory cap)
KLEE: WARNING: killing 15747 states (over memory cap)
KLEE: WARNING: killing 15477 states (over memory cap)
KLEE: WARNING: killing 16062 states (over memory cap)
KLEE: WARNING: killing 16793 states (over memory cap)
KLEE: WARNING: killing 16181 states (over memory cap)
KLEE: WARNING: killing 16966 states (over memory cap)
KLEE: WARNING: killing 16547 states (over memory cap)
KLEE: WARNING: killing 16234 states (over memory cap)
KLEE: WARNING: killing 15613 states (over memory cap)
KLEE: WARNING: killing 16148 states (over memory cap)
KLEE: WARNING: killing 16280 states (over memory cap)
KLEE: WARNING: killing 15962 states (over memory cap)
KLEE: WARNING: killing 16147 states (over memory cap)
KLEE: WARNING: killing 16528 states (over memory cap)
KLEE: WARNING: killing 15967 states (over memory cap)
KLEE: WARNING: killing 16446 states (over memory cap)
KLEE: WARNING: killing 15935 states (over memory cap)
KLEE: WARNING: killing 16359 states (over memory cap)
KLEE: WARNING: killing 15651 states (over memory cap)
KLEE: WARNING: killing 16279 states (over memory cap)
KLEE: WARNING: killing 15473 states (over memory cap)
KLEE: WARNING: killing 16640 states (over memory cap)
KLEE: WARNING: killing 16526 states (over memory cap)
KLEE: WARNING: killing 16268 states (over memory cap)
KLEE: WARNING: killing 15809 states (over memory cap)
KLEE: WARNING: killing 16233 states (over memory cap)
KLEE: WARNING: killing 16421 states (over memory cap)
KLEE: WARNING: killing 16108 states (over memory cap)
KLEE: WARNING: killing 15900 states (over memory cap)
KLEE: WARNING: killing 16077 states (over memory cap)
KLEE: WARNING: killing 16406 states (over memory cap)
KLEE: WARNING: killing 16144 states (over memory cap)
KLEE: WARNING: killing 15448 states (over memory cap)
KLEE: WARNING: killing 16458 states (over memory cap)
KLEE: WARNING: killing 16544 states (over memory cap)
KLEE: WARNING: killing 16624 states (over memory cap)
KLEE: WARNING: killing 15591 states (over memory cap)
KLEE: WARNING: killing 16648 states (over memory cap)
KLEE: WARNING: killing 16144 states (over memory cap)
KLEE: WARNING: killing 16037 states (over memory cap)
KLEE: WARNING: killing 17036 states (over memory cap)
KLEE: WARNING: killing 15861 states (over memory cap)
KLEE: WARNING: killing 15894 states (over memory cap)
KLEE: WARNING: killing 16318 states (over memory cap)
KLEE: WARNING: killing 16642 states (over memory cap)
KLEE: WARNING: killing 16291 states (over memory cap)
KLEE: WARNING: killing 15793 states (over memory cap)
KLEE: WARNING: killing 16603 states (over memory cap)
KLEE: WARNING: killing 16395 states (over memory cap)
KLEE: WARNING: killing 16286 states (over memory cap)
KLEE: WARNING: killing 16225 states (over memory cap)
KLEE: WARNING: killing 16017 states (over memory cap)
KLEE: WARNING: killing 15714 states (over memory cap)
KLEE: WARNING: killing 15173 states (over memory cap)
KLEE: WARNING: killing 17080 states (over memory cap)
KLEE: WARNING: killing 16303 states (over memory cap)
KLEE: WARNING: killing 16191 states (over memory cap)
KLEE: WARNING: killing 15843 states (over memory cap)
KLEE: WARNING: killing 16400 states (over memory cap)
KLEE: WARNING: killing 15677 states (over memory cap)
KLEE: WARNING: killing 16375 states (over memory cap)
KLEE: WARNING: killing 16074 states (over memory cap)
KLEE: WARNING: killing 16256 states (over memory cap)
KLEE: WARNING: killing 16051 states (over memory cap)
KLEE: WARNING: killing 15947 states (over memory cap)
KLEE: WARNING: killing 16458 states (over memory cap)
KLEE: WARNING: killing 16159 states (over memory cap)
KLEE: WARNING: killing 15767 states (over memory cap)
KLEE: WARNING: killing 16516 states (over memory cap)
KLEE: WARNING: killing 15320 states (over memory cap)
KLEE: WARNING: killing 16437 states (over memory cap)
KLEE: WARNING: killing 16048 states (over memory cap)
KLEE: WARNING: killing 16084 states (over memory cap)
KLEE: WARNING: killing 16166 states (over memory cap)
KLEE: WARNING: killing 16482 states (over memory cap)
KLEE: WARNING: killing 16136 states (over memory cap)
KLEE: WARNING: killing 16080 states (over memory cap)
KLEE: WARNING: killing 16679 states (over memory cap)
KLEE: WARNING: killing 15967 states (over memory cap)
KLEE: WARNING: killing 16043 states (over memory cap)
KLEE: WARNING: killing 15419 states (over memory cap)
KLEE: WARNING: killing 15877 states (over memory cap)
KLEE: WARNING: killing 16136 states (over memory cap)
KLEE: WARNING: killing 16501 states (over memory cap)
KLEE: WARNING: killing 16393 states (over memory cap)
KLEE: WARNING: killing 16476 states (over memory cap)
KLEE: WARNING: killing 16374 states (over memory cap)
KLEE: WARNING: killing 15893 states (over memory cap)
KLEE: WARNING: killing 15689 states (over memory cap)
KLEE: WARNING: killing 15352 states (over memory cap)
KLEE: WARNING: killing 16128 states (over memory cap)
KLEE: WARNING: killing 17148 states (over memory cap)
KLEE: WARNING: killing 16159 states (over memory cap)
KLEE: WARNING: killing 15730 states (over memory cap)
KLEE: WARNING: killing 15662 states (over memory cap)
KLEE: WARNING: killing 16622 states (over memory cap)
KLEE: WARNING: killing 16005 states (over memory cap)
KLEE: WARNING: killing 16643 states (over memory cap)
KLEE: WARNING: killing 15934 states (over memory cap)
KLEE: WARNING: killing 16517 states (over memory cap)
KLEE: WARNING: killing 15815 states (over memory cap)
KLEE: WARNING: killing 16678 states (over memory cap)
KLEE: WARNING: killing 15835 states (over memory cap)
KLEE: WARNING: killing 15959 states (over memory cap)
KLEE: WARNING: killing 15534 states (over memory cap)
KLEE: WARNING: killing 16111 states (over memory cap)
KLEE: WARNING: killing 15823 states (over memory cap)
KLEE: WARNING: killing 16640 states (over memory cap)
KLEE: WARNING: killing 16760 states (over memory cap)
KLEE: WARNING: killing 15965 states (over memory cap)
KLEE: WARNING: killing 16455 states (over memory cap)
KLEE: WARNING: killing 16495 states (over memory cap)
KLEE: WARNING: killing 16203 states (over memory cap)
KLEE: WARNING: killing 15822 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 15567 states (over memory cap)
KLEE: WARNING: killing 15828 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 17029 states (over memory cap)
KLEE: WARNING: killing 16291 states (over memory cap)
KLEE: WARNING: killing 15870 states (over memory cap)
KLEE: WARNING: killing 16627 states (over memory cap)
KLEE: WARNING: killing 16112 states (over memory cap)
KLEE: WARNING: killing 16008 states (over memory cap)
KLEE: WARNING: killing 16907 states (over memory cap)
KLEE: WARNING: killing 16397 states (over memory cap)
KLEE: WARNING: killing 15704 states (over memory cap)
KLEE: WARNING: killing 16000 states (over memory cap)
