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--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 429 4495 32180
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.02691912651
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)
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)
Removed calls to 'ldv_check_final_state' (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
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  strlen
  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.02604603767
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 513 394 2659 18996
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_b8546f13-13e7-4e6c-88dd-6638e68bb93a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8056 states (over memory cap)
KLEE: WARNING: killing 15314 states (over memory cap)
KLEE: WARNING: killing 14550 states (over memory cap)
KLEE: WARNING: killing 14872 states (over memory cap)
KLEE: WARNING: killing 14479 states (over memory cap)
KLEE: WARNING: killing 15174 states (over memory cap)
KLEE: WARNING: killing 14627 states (over memory cap)
KLEE: WARNING: killing 14750 states (over memory cap)
KLEE: WARNING: killing 15755 states (over memory cap)
KLEE: WARNING: killing 15421 states (over memory cap)
KLEE: WARNING: killing 16012 states (over memory cap)
KLEE: WARNING: killing 16245 states (over memory cap)
KLEE: WARNING: killing 16021 states (over memory cap)
KLEE: WARNING: killing 16919 states (over memory cap)
KLEE: WARNING: killing 16952 states (over memory cap)
KLEE: WARNING: killing 16271 states (over memory cap)
KLEE: WARNING: killing 15992 states (over memory cap)
KLEE: WARNING: killing 16436 states (over memory cap)
KLEE: WARNING: killing 15601 states (over memory cap)
KLEE: WARNING: killing 16141 states (over memory cap)
KLEE: WARNING: killing 16017 states (over memory cap)
KLEE: WARNING: killing 15852 states (over memory cap)
KLEE: WARNING: killing 16640 states (over memory cap)
KLEE: WARNING: killing 15715 states (over memory cap)
KLEE: WARNING: killing 14932 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15472 states (over memory cap)
KLEE: WARNING: killing 15347 states (over memory cap)
KLEE: WARNING: killing 16786 states (over memory cap)
KLEE: WARNING: killing 16521 states (over memory cap)
KLEE: WARNING: killing 16254 states (over memory cap)
KLEE: WARNING: killing 16591 states (over memory cap)
KLEE: WARNING: killing 15520 states (over memory cap)
KLEE: WARNING: killing 16246 states (over memory cap)
KLEE: WARNING: killing 15978 states (over memory cap)
KLEE: WARNING: killing 16214 states (over memory cap)
KLEE: WARNING: killing 16102 states (over memory cap)
KLEE: WARNING: killing 16236 states (over memory cap)
KLEE: WARNING: killing 15914 states (over memory cap)
KLEE: WARNING: killing 15999 states (over memory cap)
KLEE: WARNING: killing 16580 states (over memory cap)
KLEE: WARNING: killing 16068 states (over memory cap)
KLEE: WARNING: killing 15007 states (over memory cap)
KLEE: WARNING: killing 16281 states (over memory cap)
KLEE: WARNING: killing 15916 states (over memory cap)
KLEE: WARNING: killing 15749 states (over memory cap)
KLEE: WARNING: killing 16331 states (over memory cap)
KLEE: WARNING: killing 16017 states (over memory cap)
KLEE: WARNING: killing 15606 states (over memory cap)
KLEE: WARNING: killing 16719 states (over memory cap)
KLEE: WARNING: killing 16906 states (over memory cap)
KLEE: WARNING: killing 16790 states (over memory cap)
KLEE: WARNING: killing 16179 states (over memory cap)
KLEE: WARNING: killing 15529 states (over memory cap)
KLEE: WARNING: killing 15405 states (over memory cap)
KLEE: WARNING: killing 16812 states (over memory cap)
KLEE: WARNING: killing 15527 states (over memory cap)
KLEE: WARNING: killing 16041 states (over memory cap)
KLEE: WARNING: killing 16861 states (over memory cap)
KLEE: WARNING: killing 16362 states (over memory cap)
KLEE: WARNING: killing 15912 states (over memory cap)
KLEE: WARNING: killing 16044 states (over memory cap)
KLEE: WARNING: killing 16716 states (over memory cap)
KLEE: WARNING: killing 16309 states (over memory cap)
KLEE: WARNING: killing 15656 states (over memory cap)
KLEE: WARNING: killing 16228 states (over memory cap)
KLEE: WARNING: killing 16846 states (over memory cap)
KLEE: WARNING: killing 15614 states (over memory cap)
KLEE: WARNING: killing 16086 states (over memory cap)
KLEE: WARNING: killing 16069 states (over memory cap)
KLEE: WARNING: killing 16350 states (over memory cap)
KLEE: WARNING: killing 16040 states (over memory cap)
KLEE: WARNING: killing 15981 states (over memory cap)
KLEE: WARNING: killing 16599 states (over memory cap)
KLEE: WARNING: killing 16334 states (over memory cap)
KLEE: WARNING: killing 15842 states (over memory cap)
KLEE: WARNING: killing 15880 states (over memory cap)
KLEE: WARNING: killing 16346 states (over memory cap)
KLEE: WARNING: killing 15704 states (over memory cap)
KLEE: WARNING: killing 16171 states (over memory cap)
KLEE: WARNING: killing 15727 states (over memory cap)
KLEE: WARNING: killing 15859 states (over memory cap)
KLEE: WARNING: killing 16132 states (over memory cap)
KLEE: WARNING: killing 16939 states (over memory cap)
KLEE: WARNING: killing 16018 states (over memory cap)
KLEE: WARNING: killing 16724 states (over memory cap)
KLEE: WARNING: killing 16132 states (over memory cap)
KLEE: WARNING: killing 16316 states (over memory cap)
KLEE: WARNING: killing 16012 states (over memory cap)
KLEE: WARNING: killing 16378 states (over memory cap)
KLEE: WARNING: killing 15796 states (over memory cap)
KLEE: WARNING: killing 16017 states (over memory cap)
KLEE: WARNING: killing 16243 states (over memory cap)
KLEE: WARNING: killing 16706 states (over memory cap)
KLEE: WARNING: killing 15985 states (over memory cap)
KLEE: WARNING: killing 15355 states (over memory cap)
KLEE: WARNING: killing 15908 states (over memory cap)
KLEE: WARNING: killing 16371 states (over memory cap)
KLEE: WARNING: killing 16454 states (over memory cap)
KLEE: WARNING: killing 16485 states (over memory cap)
KLEE: WARNING: killing 16001 states (over memory cap)
KLEE: WARNING: killing 15514 states (over memory cap)
KLEE: WARNING: killing 15824 states (over memory cap)
KLEE: WARNING: killing 16712 states (over memory cap)
KLEE: WARNING: killing 15616 states (over memory cap)
KLEE: WARNING: killing 17064 states (over memory cap)
KLEE: WARNING: killing 16164 states (over memory cap)
KLEE: WARNING: killing 15961 states (over memory cap)
KLEE: WARNING: killing 16418 states (over memory cap)
KLEE: WARNING: killing 16685 states (over memory cap)
KLEE: WARNING: killing 15740 states (over memory cap)
KLEE: WARNING: killing 15203 states (over memory cap)
KLEE: WARNING: killing 16502 states (over memory cap)
KLEE: WARNING: killing 16865 states (over memory cap)
KLEE: WARNING: killing 16146 states (over memory cap)
KLEE: WARNING: killing 16842 states (over memory cap)
KLEE: WARNING: killing 16454 states (over memory cap)
KLEE: WARNING: killing 15927 states (over memory cap)
KLEE: WARNING: killing 16335 states (over memory cap)
KLEE: WARNING: killing 16180 states (over memory cap)
KLEE: WARNING: killing 15792 states (over memory cap)
KLEE: WARNING: killing 16198 states (over memory cap)
KLEE: WARNING: killing 15395 states (over memory cap)
KLEE: WARNING: killing 16545 states (over memory cap)
KLEE: WARNING: killing 16673 states (over memory cap)
KLEE: WARNING: killing 15586 states (over memory cap)
KLEE: WARNING: killing 16313 states (over memory cap)
KLEE: WARNING: killing 16165 states (over memory cap)
KLEE: WARNING: killing 16381 states (over memory cap)
KLEE: WARNING: killing 16832 states (over memory cap)
KLEE: WARNING: killing 16357 states (over memory cap)
KLEE: WARNING: killing 16159 states (over memory cap)
KLEE: WARNING: killing 16329 states (over memory cap)
KLEE: WARNING: killing 15759 states (over memory cap)
KLEE: WARNING: killing 16621 states (over memory cap)
KLEE: WARNING: killing 15965 states (over memory cap)
KLEE: WARNING: killing 15815 states (over memory cap)
KLEE: WARNING: killing 15938 states (over memory cap)
KLEE: WARNING: killing 16479 states (over memory cap)
KLEE: WARNING: killing 15915 states (over memory cap)
KLEE: WARNING: killing 15897 states (over memory cap)
KLEE: WARNING: killing 16021 states (over memory cap)
KLEE: WARNING: killing 16741 states (over memory cap)
KLEE: WARNING: killing 15670 states (over memory cap)
KLEE: WARNING: killing 15837 states (over memory cap)
KLEE: WARNING: killing 16425 states (over memory cap)
KLEE: WARNING: killing 16038 states (over memory cap)
KLEE: WARNING: killing 15979 states (over memory cap)
KLEE: WARNING: killing 16326 states (over memory cap)
KLEE: WARNING: killing 16542 states (over memory cap)
KLEE: WARNING: killing 16391 states (over memory cap)
KLEE: WARNING: killing 16288 states (over memory cap)
KLEE: WARNING: killing 15638 states (over memory cap)
KLEE: WARNING: killing 16259 states (over memory cap)
KLEE: WARNING: killing 16520 states (over memory cap)
KLEE: WARNING: killing 16236 states (over memory cap)
KLEE: WARNING: killing 16315 states (over memory cap)
KLEE: WARNING: killing 15705 states (over memory cap)
KLEE: WARNING: killing 16014 states (over memory cap)
KLEE: WARNING: killing 16179 states (over memory cap)
KLEE: WARNING: killing 16390 states (over memory cap)
KLEE: WARNING: killing 16832 states (over memory cap)
KLEE: WARNING: killing 15968 states (over memory cap)
KLEE: WARNING: killing 16127 states (over memory cap)
KLEE: WARNING: killing 16025 states (over memory cap)
KLEE: WARNING: killing 16464 states (over memory cap)
KLEE: WARNING: killing 16362 states (over memory cap)
KLEE: WARNING: killing 15941 states (over memory cap)
KLEE: WARNING: killing 16738 states (over memory cap)
KLEE: WARNING: killing 16194 states (over memory cap)
KLEE: WARNING: killing 15061 states (over memory cap)
