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-32_7a-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.: 382 688 5210 43523
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
INFO: Compilation, preparation and instrumentation time: 1.59457993507
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 'list_del' (function is undefined)
Removed calls to 'mutex_lock' (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
Defining function mutex_trylock 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.83366394043
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 526 542 3083 25549
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_2bccd9c3-1591-41ab-9f24-d9e476a902dc/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8109 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15614 states (over memory cap)
KLEE: WARNING: killing 15570 states (over memory cap)
KLEE: WARNING: killing 15820 states (over memory cap)
KLEE: WARNING: killing 15493 states (over memory cap)
KLEE: WARNING: killing 14821 states (over memory cap)
KLEE: WARNING: killing 15481 states (over memory cap)
KLEE: WARNING: killing 14637 states (over memory cap)
KLEE: WARNING: killing 15124 states (over memory cap)
KLEE: WARNING: killing 16364 states (over memory cap)
KLEE: WARNING: killing 16569 states (over memory cap)
KLEE: WARNING: killing 16602 states (over memory cap)
KLEE: WARNING: killing 16811 states (over memory cap)
KLEE: WARNING: killing 17188 states (over memory cap)
KLEE: WARNING: killing 17226 states (over memory cap)
KLEE: WARNING: killing 16745 states (over memory cap)
KLEE: WARNING: killing 16381 states (over memory cap)
KLEE: WARNING: killing 15840 states (over memory cap)
KLEE: WARNING: killing 16275 states (over memory cap)
KLEE: WARNING: killing 16422 states (over memory cap)
KLEE: WARNING: killing 16348 states (over memory cap)
KLEE: WARNING: killing 16437 states (over memory cap)
KLEE: WARNING: killing 16816 states (over memory cap)
KLEE: WARNING: killing 16735 states (over memory cap)
KLEE: WARNING: killing 16097 states (over memory cap)
KLEE: WARNING: killing 17486 states (over memory cap)
KLEE: WARNING: killing 15945 states (over memory cap)
KLEE: WARNING: killing 16884 states (over memory cap)
KLEE: WARNING: killing 15792 states (over memory cap)
KLEE: WARNING: killing 15603 states (over memory cap)
KLEE: WARNING: killing 16873 states (over memory cap)
KLEE: WARNING: killing 16353 states (over memory cap)
KLEE: WARNING: killing 15825 states (over memory cap)
KLEE: WARNING: killing 16077 states (over memory cap)
KLEE: WARNING: killing 15947 states (over memory cap)
KLEE: WARNING: killing 16100 states (over memory cap)
KLEE: WARNING: killing 17134 states (over memory cap)
KLEE: WARNING: killing 16114 states (over memory cap)
KLEE: WARNING: killing 17044 states (over memory cap)
KLEE: WARNING: killing 16633 states (over memory cap)
KLEE: WARNING: killing 15615 states (over memory cap)
KLEE: WARNING: killing 16432 states (over memory cap)
KLEE: WARNING: killing 17357 states (over memory cap)
KLEE: WARNING: killing 15902 states (over memory cap)
KLEE: WARNING: killing 16596 states (over memory cap)
KLEE: WARNING: killing 16585 states (over memory cap)
KLEE: WARNING: killing 16673 states (over memory cap)
KLEE: WARNING: killing 15827 states (over memory cap)
KLEE: WARNING: killing 16303 states (over memory cap)
KLEE: WARNING: killing 16724 states (over memory cap)
KLEE: WARNING: killing 15941 states (over memory cap)
KLEE: WARNING: killing 16688 states (over memory cap)
KLEE: WARNING: killing 16840 states (over memory cap)
KLEE: WARNING: killing 15944 states (over memory cap)
KLEE: WARNING: killing 16033 states (over memory cap)
KLEE: WARNING: killing 16125 states (over memory cap)
KLEE: WARNING: killing 15891 states (over memory cap)
KLEE: WARNING: killing 16311 states (over memory cap)
KLEE: WARNING: killing 16077 states (over memory cap)
KLEE: WARNING: killing 16607 states (over memory cap)
KLEE: WARNING: killing 17296 states (over memory cap)
KLEE: WARNING: killing 16359 states (over memory cap)
KLEE: WARNING: killing 16721 states (over memory cap)
KLEE: WARNING: killing 16326 states (over memory cap)
KLEE: WARNING: killing 15825 states (over memory cap)
KLEE: WARNING: killing 16077 states (over memory cap)
KLEE: WARNING: killing 16813 states (over memory cap)
KLEE: WARNING: killing 16204 states (over memory cap)
KLEE: WARNING: killing 16078 states (over memory cap)
KLEE: WARNING: killing 16441 states (over memory cap)
KLEE: WARNING: killing 16755 states (over memory cap)
KLEE: WARNING: killing 15986 states (over memory cap)
KLEE: WARNING: killing 16237 states (over memory cap)
KLEE: WARNING: killing 15892 states (over memory cap)
KLEE: WARNING: killing 16475 states (over memory cap)
KLEE: WARNING: killing 17099 states (over memory cap)
KLEE: WARNING: killing 16977 states (over memory cap)
KLEE: WARNING: killing 16591 states (over memory cap)
KLEE: WARNING: killing 16790 states (over memory cap)
KLEE: WARNING: killing 16458 states (over memory cap)
KLEE: WARNING: killing 16498 states (over memory cap)
KLEE: WARNING: killing 15841 states (over memory cap)
KLEE: WARNING: killing 16198 states (over memory cap)
KLEE: WARNING: killing 16610 states (over memory cap)
KLEE: WARNING: killing 15846 states (over memory cap)
KLEE: WARNING: killing 16101 states (over memory cap)
KLEE: WARNING: killing 16618 states (over memory cap)
KLEE: WARNING: killing 16228 states (over memory cap)
KLEE: WARNING: killing 16429 states (over memory cap)
KLEE: WARNING: killing 16041 states (over memory cap)
KLEE: WARNING: killing 16714 states (over memory cap)
KLEE: WARNING: killing 16172 states (over memory cap)
KLEE: WARNING: killing 15945 states (over memory cap)
KLEE: WARNING: killing 16934 states (over memory cap)
KLEE: WARNING: killing 16659 states (over memory cap)
KLEE: WARNING: killing 16799 states (over memory cap)
KLEE: WARNING: killing 16417 states (over memory cap)
KLEE: WARNING: killing 16403 states (over memory cap)
KLEE: WARNING: killing 16494 states (over memory cap)
KLEE: WARNING: killing 16634 states (over memory cap)
KLEE: WARNING: killing 16419 states (over memory cap)
KLEE: WARNING: killing 15928 states (over memory cap)
KLEE: WARNING: killing 16440 states (over memory cap)
KLEE: WARNING: killing 16059 states (over memory cap)
KLEE: WARNING: killing 16518 states (over memory cap)
KLEE: WARNING: killing 17183 states (over memory cap)
KLEE: WARNING: killing 16126 states (over memory cap)
KLEE: WARNING: killing 16269 states (over memory cap)
KLEE: WARNING: killing 16098 states (over memory cap)
KLEE: WARNING: killing 16135 states (over memory cap)
KLEE: WARNING: killing 16280 states (over memory cap)
KLEE: WARNING: killing 16683 states (over memory cap)
KLEE: WARNING: killing 16832 states (over memory cap)
KLEE: WARNING: killing 16401 states (over memory cap)
KLEE: WARNING: killing 16919 states (over memory cap)
KLEE: WARNING: killing 15499 states (over memory cap)
KLEE: WARNING: killing 16257 states (over memory cap)
KLEE: WARNING: killing 16608 states (over memory cap)
KLEE: WARNING: killing 16023 states (over memory cap)
KLEE: WARNING: killing 16893 states (over memory cap)
KLEE: WARNING: killing 15739 states (over memory cap)
KLEE: WARNING: killing 16398 states (over memory cap)
KLEE: WARNING: killing 16437 states (over memory cap)
KLEE: WARNING: killing 16476 states (over memory cap)
KLEE: WARNING: killing 16927 states (over memory cap)
KLEE: WARNING: killing 16088 states (over memory cap)
KLEE: WARNING: killing 17002 states (over memory cap)
KLEE: WARNING: killing 16790 states (over memory cap)
KLEE: WARNING: killing 15692 states (over memory cap)
KLEE: WARNING: killing 16396 states (over memory cap)
KLEE: WARNING: killing 15871 states (over memory cap)
KLEE: WARNING: killing 15859 states (over memory cap)
KLEE: WARNING: killing 16555 states (over memory cap)
KLEE: WARNING: killing 16540 states (over memory cap)
KLEE: WARNING: killing 16427 states (over memory cap)
KLEE: WARNING: killing 15688 states (over memory cap)
KLEE: WARNING: killing 16445 states (over memory cap)
KLEE: WARNING: killing 17664 states (over memory cap)
KLEE: WARNING: killing 16323 states (over memory cap)
KLEE: WARNING: killing 16771 states (over memory cap)
KLEE: WARNING: killing 16651 states (over memory cap)
KLEE: WARNING: killing 16430 states (over memory cap)
KLEE: WARNING: killing 16220 states (over memory cap)
KLEE: WARNING: killing 15638 states (over memory cap)
KLEE: WARNING: killing 16441 states (over memory cap)
KLEE: WARNING: killing 16070 states (over memory cap)
KLEE: WARNING: killing 15292 states (over memory cap)
KLEE: WARNING: killing 16595 states (over memory cap)
KLEE: WARNING: killing 15978 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
