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--infiniband--hw--mlx5--mlx5_ib.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.: 372 496 4573 40889
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_sync_single_for_cpu
Removed infinite loop in dma_sync_single_for_device
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in mlx5_ib_process_mad
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.2099878788
Defining function sprintf as symbolic
Defining function ioread32be as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'ib_unregister_device' (function is undefined)
Removed calls to 'cleanup_srcu_struct' (function is undefined)
Removed calls to 'ib_dealloc_device' (function is undefined)
Removed calls to 'ib_dispatch_event' (function is undefined)
Defining function printk as symbolic
Removed calls to 'ib_umem_release' (function is undefined)
Removed calls to 'mlx5_buf_free' (function is undefined)
Removed calls to 'mlx5_db_free' (function is undefined)
Defining function mlx5_core_dealloc_pd as symbolic
Defining function mlx5_core_destroy_mkey as symbolic
Defining function mlx5_core_destroy_cq as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mlx5_core_xrcd_dealloc as symbolic
Defining function mlx5_core_destroy_srq as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'synchronize_srcu' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to '_raw_spin_lock_nested' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function ib_destroy_cq as symbolic
Defining function ib_dereg_mr as symbolic
Defining function ib_dealloc_pd as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function mlx5_core_qp_modify as symbolic
Defining function mlx5_core_destroy_qp as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'free_pages' (function is undefined)
Defining function mlx5_core_page_fault_resume as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Removed calls to '__srcu_read_unlock' (function is undefined)
Defining function ib_umem_odp_map_dma_pages as symbolic
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Removed calls to 'down' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'up' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Defining function wait_for_completion_timeout as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function get_zeroed_page as symbolic
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function sg_next as symbolic
Defining function __phys_addr as symbolic
Defining function radix_tree_lookup as symbolic
Defining function __srcu_read_lock as symbolic
Defining function __get_free_pages as symbolic
Defining function ib_umem_copy_from as symbolic
Defining function del_timer_sync as symbolic
Defining function cancel_delayed_work as symbolic
Defining function ib_alloc_device as symbolic
Defining function strlcpy as symbolic
Removed calls to 'mlx5_query_port_max_mtu' (function is undefined)
Removed calls to 'mlx5_query_port_oper_mtu' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'kvfree' (function is undefined)
Removed calls to 'mlx5_fill_page_array' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function ib_register_device as symbolic
Defining function device_create_file as symbolic
Defining function ib_alloc_pd as symbolic
Defining function ib_get_dma_mr as symbolic
Defining function ib_create_cq as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function debugfs_create_u32 as symbolic
Defining function queue_work_on as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_write_unlock_irqrestore' (function is undefined)
Defining function mlx5_core_create_mkey as symbolic
Defining function _raw_write_lock_irqsave as symbolic
Defining function radix_tree_insert as symbolic
Defining function mod_timer as symbolic
Defining function __init_srcu_struct as symbolic
Defining function mlx5_query_hca_vport_node_guid as symbolic
Defining function mlx5_core_mad_ifc as symbolic
Defining function mlx5_core_access_reg as symbolic
Defining function mlx5_core_xrcd_alloc as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function mlx5_core_create_psv as symbolic
Defining function mlx5_core_destroy_psv as symbolic
Defining function mlx5_core_detach_mcg as symbolic
Defining function mlx5_core_attach_mcg as symbolic
Removed calls to 'ib_umem_odp_unmap_dma_pages' (function is undefined)
Defining function ib_umem_get as symbolic
Defining function vzalloc as symbolic
Defining function ib_umem_page_count as symbolic
Defining function find_first_bit as symbolic
Defining function mlx5_core_get_srq as symbolic
Defining function mlx5_core_modify_cq as symbolic
Defining function mlx5_buf_alloc as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function mlx5_vector2eqn as symbolic
Defining function mlx5_core_create_cq as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function mlx5_db_alloc as symbolic
Defining function mlx5_core_qp_query as symbolic
Defining function ib_modify_qp_is_ok as symbolic
Defining function mlx5_core_create_qp as symbolic
Defining function mlx5_core_query_srq as symbolic
Defining function mlx5_core_arm_srq as symbolic
Defining function mlx5_core_create_srq as symbolic
Defining function mlx5_core_alloc_pd as symbolic
Defining function pgprot_writecombine as symbolic
Defining function remap_pfn_range as symbolic
Defining function mlx5_cmd_free_uar as symbolic
Defining function mlx5_cmd_alloc_uar as symbolic
Defining function mlx5_set_port_caps as symbolic
Defining function mlx5_query_hca_vport_pkey as symbolic
Defining function mlx5_query_hca_vport_gid as symbolic
Defining function mlx5_query_hca_vport_context as symbolic
Defining function mlx5_query_port_link_width_oper as symbolic
Defining function mlx5_query_port_proto_oper as symbolic
Defining function mlx5_query_port_vl_hw_cap as symbolic
Defining function mlx5_core_query_vendor_id as symbolic
Defining function mlx5_query_hca_vport_system_image_guid as symbolic
Removed calls to 'usleep_range' (function is undefined)
Defining function simple_open as symbolic
Defining function sscanf as symbolic
Defining function snprintf as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'mlx5_unregister_interface' (function is undefined)
Defining function ldv_release_5 as symbolic
Defining function mlx5_register_interface as symbolic
Defining function ldv_release_6 as symbolic
Linked our definitions to these undefined functions:
  __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.357172966
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 516 349 2408 23651
INFO: Starting verification
KLEE: WARNING ONCE: function "mlx5_ib_add" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_event" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_dealloc_xrcd" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_dealloc_pd" has inline asm
KLEE: WARNING ONCE: function "mlx5_mr_cache_cleanup" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_destroy_qp" has inline asm
KLEE: WARNING ONCE: function "__mlx5_ib_cq_clean" has inline asm
KLEE: WARNING ONCE: function "free_uuar" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_mr_pfault_handler" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_update_mtt" has inline asm
KLEE: WARNING ONCE: function "__mlx5_ib_populate_pas" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_alloc_ucontext" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_dealloc_ucontext" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_alloc_pd" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_create_srq" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_post_srq_recv" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_create_qp" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_modify_qp" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_post_send" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_post_recv" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_create_cq" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_modify_cq" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_resize_cq" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_poll_cq" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_arm_cq" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_reg_user_mr" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_dereg_mr" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_destroy_mr" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_mcg_attach" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_mcg_detach" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_process_mad" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_create_mr" has inline asm
KLEE: WARNING ONCE: function "mlx5_mr_cache_init" has inline asm
KLEE: WARNING ONCE: function "__cache_work_func" has inline asm
KLEE: WARNING ONCE: function "add_keys" has inline asm
KLEE: WARNING ONCE: function "remove_keys" has inline asm
KLEE: WARNING ONCE: function "reg_mr_callback" has inline asm
KLEE: WARNING ONCE: function "clean_mr" has inline asm
KLEE: WARNING ONCE: function "free_cached_mr" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_cont_pages" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_cq_event" has inline asm
KLEE: WARNING ONCE: function "alloc_uuar" has inline asm
KLEE: WARNING ONCE: function "mlx5_query_mad_ifc_port" has inline asm
KLEE: WARNING ONCE: function "mlx5_ib_get_buf_offset" 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_0fb760a9-2010-4dac-9410-000524e3b456/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8746 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15482 states (over memory cap)
KLEE: WARNING: killing 15616 states (over memory cap)
KLEE: WARNING: killing 15106 states (over memory cap)
KLEE: WARNING: killing 14663 states (over memory cap)
KLEE: WARNING: killing 14855 states (over memory cap)
KLEE: WARNING: killing 15859 states (over memory cap)
KLEE: WARNING: killing 15830 states (over memory cap)
KLEE: WARNING: killing 15342 states (over memory cap)
KLEE: WARNING: killing 15428 states (over memory cap)
KLEE: WARNING: killing 16782 states (over memory cap)
KLEE: WARNING: killing 17271 states (over memory cap)
KLEE: WARNING: killing 17314 states (over memory cap)
KLEE: WARNING: killing 17058 states (over memory cap)
KLEE: WARNING: killing 17036 states (over memory cap)
KLEE: WARNING: killing 16273 states (over memory cap)
KLEE: WARNING: killing 16535 states (over memory cap)
KLEE: WARNING: killing 16568 states (over memory cap)
KLEE: WARNING: killing 16037 states (over memory cap)
KLEE: WARNING: killing 16012 states (over memory cap)
KLEE: WARNING: killing 16841 states (over memory cap)
KLEE: WARNING: killing 16422 states (over memory cap)
KLEE: WARNING: killing 16686 states (over memory cap)
KLEE: WARNING: killing 15923 states (over memory cap)
KLEE: WARNING: killing 15681 states (over memory cap)
KLEE: WARNING: killing 16615 states (over memory cap)
KLEE: WARNING: killing 16254 states (over memory cap)
KLEE: WARNING: killing 16347 states (over memory cap)
KLEE: WARNING: killing 16045 states (over memory cap)
KLEE: WARNING: killing 16591 states (over memory cap)
KLEE: WARNING: killing 16456 states (over memory cap)
KLEE: WARNING: killing 16157 states (over memory cap)
KLEE: WARNING: killing 16080 states (over memory cap)
KLEE: WARNING: killing 17238 states (over memory cap)
KLEE: WARNING: killing 16328 states (over memory cap)
KLEE: WARNING: killing 16641 states (over memory cap)
KLEE: WARNING: killing 15400 states (over memory cap)
KLEE: WARNING: killing 16661 states (over memory cap)
KLEE: WARNING: killing 16250 states (over memory cap)
KLEE: WARNING: killing 17014 states (over memory cap)
KLEE: WARNING: killing 15882 states (over memory cap)
KLEE: WARNING: killing 16578 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 16431 states (over memory cap)
KLEE: WARNING: killing 17077 states (over memory cap)
KLEE: WARNING: killing 16016 states (over memory cap)
KLEE: WARNING: killing 15662 states (over memory cap)
KLEE: WARNING: killing 16692 states (over memory cap)
KLEE: WARNING: killing 16613 states (over memory cap)
KLEE: WARNING: killing 16601 states (over memory cap)
KLEE: WARNING: killing 16035 states (over memory cap)
KLEE: WARNING: killing 16289 states (over memory cap)
KLEE: WARNING: killing 16709 states (over memory cap)
KLEE: WARNING: killing 16641 states (over memory cap)
KLEE: WARNING: killing 16514 states (over memory cap)
KLEE: WARNING: killing 16445 states (over memory cap)
KLEE: WARNING: killing 16696 states (over memory cap)
KLEE: WARNING: killing 16352 states (over memory cap)
KLEE: WARNING: killing 16175 states (over memory cap)
KLEE: WARNING: killing 16533 states (over memory cap)
KLEE: WARNING: killing 15921 states (over memory cap)
KLEE: WARNING: killing 16446 states (over memory cap)
KLEE: WARNING: killing 16319 states (over memory cap)
KLEE: WARNING: killing 17012 states (over memory cap)
KLEE: WARNING: killing 16401 states (over memory cap)
KLEE: WARNING: killing 16114 states (over memory cap)
KLEE: WARNING: killing 16419 states (over memory cap)
KLEE: WARNING: killing 16891 states (over memory cap)
KLEE: WARNING: killing 16233 states (over memory cap)
KLEE: WARNING: killing 16157 states (over memory cap)
KLEE: WARNING: killing 16305 states (over memory cap)
KLEE: WARNING: killing 17042 states (over memory cap)
KLEE: WARNING: killing 16382 states (over memory cap)
KLEE: WARNING: killing 16313 states (over memory cap)
KLEE: WARNING: killing 16564 states (over memory cap)
KLEE: WARNING: killing 15264 states (over memory cap)
KLEE: WARNING: killing 17390 states (over memory cap)
KLEE: WARNING: killing 16198 states (over memory cap)
KLEE: WARNING: killing 16666 states (over memory cap)
KLEE: WARNING: killing 16277 states (over memory cap)
KLEE: WARNING: killing 16317 states (over memory cap)
KLEE: WARNING: killing 16347 states (over memory cap)
KLEE: WARNING: killing 16280 states (over memory cap)
KLEE: WARNING: killing 16002 states (over memory cap)
KLEE: WARNING: killing 15877 states (over memory cap)
KLEE: WARNING: killing 17297 states (over memory cap)
KLEE: WARNING: killing 15748 states (over memory cap)
KLEE: WARNING: killing 16735 states (over memory cap)
KLEE: WARNING: killing 16140 states (over memory cap)
KLEE: WARNING: killing 16820 states (over memory cap)
KLEE: WARNING: killing 16166 states (over memory cap)
KLEE: WARNING: killing 16472 states (over memory cap)
KLEE: WARNING: killing 16618 states (over memory cap)
KLEE: WARNING: killing 16280 states (over memory cap)
KLEE: WARNING: killing 16008 states (over memory cap)
KLEE: WARNING: killing 16303 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 15861 states (over memory cap)
KLEE: WARNING: killing 16472 states (over memory cap)
KLEE: WARNING: killing 16298 states (over memory cap)
KLEE: WARNING: killing 16550 states (over memory cap)
KLEE: WARNING: killing 17066 states (over memory cap)
KLEE: WARNING: killing 16948 states (over memory cap)
KLEE: WARNING: killing 15675 states (over memory cap)
KLEE: WARNING: killing 16709 states (over memory cap)
KLEE: WARNING: killing 16647 states (over memory cap)
KLEE: WARNING: killing 16004 states (over memory cap)
KLEE: WARNING: killing 16620 states (over memory cap)
KLEE: WARNING: killing 16342 states (over memory cap)
KLEE: WARNING: killing 15914 states (over memory cap)
KLEE: WARNING: killing 16681 states (over memory cap)
KLEE: WARNING: killing 16826 states (over memory cap)
KLEE: WARNING: killing 15767 states (over memory cap)
KLEE: WARNING: killing 16266 states (over memory cap)
KLEE: WARNING: killing 16731 states (over memory cap)
KLEE: WARNING: killing 16982 states (over memory cap)
KLEE: WARNING: killing 16399 states (over memory cap)
KLEE: WARNING: killing 15963 states (over memory cap)
KLEE: WARNING: killing 16054 states (over memory cap)
KLEE: WARNING: killing 15988 states (over memory cap)
KLEE: WARNING: killing 17005 states (over memory cap)
KLEE: WARNING: killing 16738 states (over memory cap)
KLEE: WARNING: killing 16834 states (over memory cap)
KLEE: WARNING: killing 16247 states (over memory cap)
KLEE: WARNING: killing 16542 states (over memory cap)
KLEE: WARNING: killing 16017 states (over memory cap)
KLEE: WARNING: killing 16311 states (over memory cap)
KLEE: WARNING: killing 16090 states (over memory cap)
KLEE: WARNING: killing 16646 states (over memory cap)
KLEE: WARNING: killing 16630 states (over memory cap)
KLEE: WARNING: killing 16771 states (over memory cap)
KLEE: WARNING: killing 16815 states (over memory cap)
KLEE: WARNING: killing 16595 states (over memory cap)
KLEE: WARNING: killing 15809 states (over memory cap)
KLEE: WARNING: killing 16258 states (over memory cap)
KLEE: WARNING: killing 16246 states (over memory cap)
KLEE: WARNING: killing 16586 states (over memory cap)
KLEE: WARNING: killing 16216 states (over memory cap)
KLEE: WARNING: killing 16296 states (over memory cap)
KLEE: WARNING: killing 15880 states (over memory cap)
KLEE: WARNING: killing 15859 states (over memory cap)
KLEE: WARNING: killing 17012 states (over memory cap)
KLEE: WARNING: killing 16854 states (over memory cap)
KLEE: WARNING: killing 16481 states (over memory cap)
KLEE: WARNING: killing 16263 states (over memory cap)
KLEE: WARNING: killing 16961 states (over memory cap)
KLEE: WARNING: killing 16741 states (over memory cap)
KLEE: WARNING: killing 16376 states (over memory cap)
KLEE: WARNING: killing 16664 states (over memory cap)
KLEE: WARNING: killing 15786 states (over memory cap)
KLEE: WARNING: killing 16531 states (over memory cap)
KLEE: WARNING: killing 16108 states (over memory cap)
KLEE: WARNING: killing 16291 states (over memory cap)
KLEE: WARNING: killing 16230 states (over memory cap)
KLEE: WARNING: killing 16014 states (over memory cap)
KLEE: WARNING: killing 16301 states (over memory cap)
KLEE: WARNING: killing 15782 states (over memory cap)
KLEE: WARNING: killing 16728 states (over memory cap)
KLEE: WARNING: killing 17061 states (over memory cap)
KLEE: WARNING: killing 17055 states (over memory cap)
KLEE: WARNING: killing 15734 states (over memory cap)
KLEE: WARNING: killing 15970 states (over memory cap)
