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--core--ib_cm.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.: 123 330 2183 16746
Removed infinite loop in ib_send_cm_req
Removed infinite loop in cm_process_work
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.620233058929
Removed calls to 'idr_preload' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function idr_alloc_cyclic as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'rb_erase' (function is undefined)
Removed calls to 'ib_cancel_mad' (function is undefined)
Removed calls to 'idr_remove' (function is undefined)
Removed calls to 'wait_for_completion' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to 'ib_free_recv_mad' (function is undefined)
Defining function ib_post_send_mad as symbolic
Removed calls to 'ib_free_send_mad' (function is undefined)
Defining function ib_destroy_ah as symbolic
Defining function ib_create_ah as symbolic
Defining function ib_create_send_mad as symbolic
Defining function kmemdup as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'rb_insert_color' (function is undefined)
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 '_raw_read_unlock_irqrestore' (function is undefined)
Defining function _raw_read_lock_irqsave as symbolic
Defining function ib_find_cached_gid as symbolic
Defining function ib_find_cached_pkey as symbolic
Defining function ib_init_ah_from_path as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function idr_find_slowpath as symbolic
Defining function ib_init_ah_from_wc as symbolic
Defining function ib_create_ah_from_wc as symbolic
Defining function ib_modify_mad as symbolic
Defining function ib_get_cached_gid as symbolic
Defining function kasprintf as symbolic
Defining function sprintf as symbolic
Removed calls to 'kobject_put' (function is undefined)
Removed calls to 'ib_set_client_data' (function is undefined)
Removed calls to '_raw_write_unlock_irqrestore' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Defining function ib_get_client_data as symbolic
Defining function _raw_write_lock_irqsave as symbolic
Defining function ib_modify_port as symbolic
Defining function ib_unregister_mad_agent as symbolic
Defining function device_create as symbolic
Defining function ib_register_mad_agent as symbolic
Defining function kobject_init_and_add as symbolic
Defining function ib_query_device as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ib_unregister_client' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'class_unregister' (function is undefined)
Removed calls to 'idr_destroy' (function is undefined)
Removed calls to '__rwlock_init' (function is undefined)
Removed calls to 'idr_init' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Defining function ldv_probe_6 as symbolic
Defining function __class_register as symbolic
Defining function __alloc_workqueue_key as symbolic
Defining function ib_register_client as symbolic
Defining function cancel_delayed_work as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __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: 0.670577049255
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 223 177 1222 10081
INFO: Starting verification
KLEE: WARNING ONCE: function "ib_create_cm_id" has inline asm
KLEE: WARNING ONCE: function "cm_deref_id" has inline asm
KLEE: WARNING ONCE: function "cm_alloc_msg" has inline asm
KLEE: WARNING ONCE: function "ib_send_cm_req" has inline asm
KLEE: WARNING ONCE: function "cm_work_handler" has inline asm
KLEE: WARNING ONCE: function "cm_get_id" has inline asm
KLEE: WARNING ONCE: function "cm_process_work" has inline asm
KLEE: WARNING ONCE: function "cm_add_one" has inline asm
KLEE: WARNING ONCE: function "cm_send_handler" has inline asm
KLEE: WARNING ONCE: function "cm_recv_handler" 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_9688f0ec-7386-465b-bcd5-bbfa0eafbd50/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10926 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 11688 states (over memory cap)
KLEE: WARNING: killing 11310 states (over memory cap)
KLEE: WARNING: killing 11286 states (over memory cap)
KLEE: WARNING: killing 11172 states (over memory cap)
KLEE: WARNING: killing 11061 states (over memory cap)
KLEE: WARNING: killing 11033 states (over memory cap)
KLEE: WARNING: killing 10836 states (over memory cap)
KLEE: WARNING: killing 10900 states (over memory cap)
KLEE: WARNING: killing 11225 states (over memory cap)
KLEE: WARNING: killing 11113 states (over memory cap)
KLEE: WARNING: killing 11440 states (over memory cap)
KLEE: WARNING: killing 11328 states (over memory cap)
KLEE: WARNING: killing 11735 states (over memory cap)
KLEE: WARNING: killing 11800 states (over memory cap)
KLEE: WARNING: killing 12039 states (over memory cap)
KLEE: WARNING: killing 12018 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-rVgaPG/linux-4.2-rc1.tar.xz-32_7a-drivers--infiniband--core--ib_cm.ko-entry_point_true-unreach-call.cil.out.c:13371: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13021 states (over memory cap)
KLEE: WARNING: killing 11983 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-rVgaPG/linux-4.2-rc1.tar.xz-32_7a-drivers--infiniband--core--ib_cm.ko-entry_point_true-unreach-call.cil.out.c:6838: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-rVgaPG/linux-4.2-rc1.tar.xz-32_7a-drivers--infiniband--core--ib_cm.ko-entry_point_true-unreach-call.cil.out.c:12969: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12983 states (over memory cap)
KLEE: WARNING: killing 11696 states (over memory cap)
KLEE: WARNING: killing 12437 states (over memory cap)
KLEE: WARNING: killing 12673 states (over memory cap)
KLEE: WARNING: killing 11817 states (over memory cap)
KLEE: WARNING: killing 12979 states (over memory cap)
KLEE: WARNING: killing 12455 states (over memory cap)
KLEE: WARNING: killing 12443 states (over memory cap)
KLEE: WARNING: killing 12172 states (over memory cap)
KLEE: WARNING: killing 11907 states (over memory cap)
KLEE: WARNING: killing 12061 states (over memory cap)
KLEE: WARNING: killing 11960 states (over memory cap)
KLEE: WARNING: killing 11605 states (over memory cap)
KLEE: WARNING: killing 12093 states (over memory cap)
KLEE: WARNING: killing 11491 states (over memory cap)
KLEE: WARNING: killing 12220 states (over memory cap)
KLEE: WARNING: killing 11544 states (over memory cap)
KLEE: WARNING: killing 11692 states (over memory cap)
KLEE: WARNING: killing 11671 states (over memory cap)
KLEE: WARNING: killing 11496 states (over memory cap)
KLEE: WARNING: killing 11969 states (over memory cap)
KLEE: WARNING: killing 11458 states (over memory cap)
KLEE: WARNING: killing 12273 states (over memory cap)
KLEE: WARNING: killing 12088 states (over memory cap)
KLEE: WARNING: killing 12322 states (over memory cap)
KLEE: WARNING: killing 11898 states (over memory cap)
KLEE: WARNING: killing 11962 states (over memory cap)
KLEE: WARNING: killing 11949 states (over memory cap)
KLEE: WARNING: killing 11613 states (over memory cap)
KLEE: WARNING: killing 11759 states (over memory cap)
KLEE: WARNING: killing 12233 states (over memory cap)
KLEE: WARNING: killing 11976 states (over memory cap)
KLEE: WARNING: killing 11640 states (over memory cap)
KLEE: WARNING: killing 11788 states (over memory cap)
KLEE: WARNING: killing 12011 states (over memory cap)
KLEE: WARNING: killing 12408 states (over memory cap)
KLEE: WARNING: killing 12234 states (over memory cap)
KLEE: WARNING: killing 11900 states (over memory cap)
KLEE: WARNING: killing 11888 states (over memory cap)
KLEE: WARNING: killing 11870 states (over memory cap)
KLEE: WARNING: killing 12261 states (over memory cap)
KLEE: WARNING: killing 12091 states (over memory cap)
KLEE: WARNING: killing 12157 states (over memory cap)
KLEE: WARNING: killing 11825 states (over memory cap)
KLEE: WARNING: killing 12049 states (over memory cap)
KLEE: WARNING: killing 11960 states (over memory cap)
KLEE: WARNING: killing 11865 states (over memory cap)
KLEE: WARNING: killing 11852 states (over memory cap)
KLEE: WARNING: killing 11596 states (over memory cap)
KLEE: WARNING: killing 11902 states (over memory cap)
KLEE: WARNING: killing 11650 states (over memory cap)
KLEE: WARNING: killing 12191 states (over memory cap)
KLEE: WARNING: killing 11624 states (over memory cap)
KLEE: WARNING: killing 11850 states (over memory cap)
KLEE: WARNING: killing 12234 states (over memory cap)
KLEE: WARNING: killing 11580 states (over memory cap)
KLEE: WARNING: killing 11892 states (over memory cap)
KLEE: WARNING: killing 11637 states (over memory cap)
KLEE: WARNING: killing 11941 states (over memory cap)
KLEE: WARNING: killing 12083 states (over memory cap)
KLEE: WARNING: killing 11756 states (over memory cap)
KLEE: WARNING: killing 11507 states (over memory cap)
KLEE: WARNING: killing 12128 states (over memory cap)
KLEE: WARNING: killing 12352 states (over memory cap)
KLEE: WARNING: killing 12735 states (over memory cap)
KLEE: WARNING: killing 12177 states (over memory cap)
KLEE: WARNING: killing 11695 states (over memory cap)
KLEE: WARNING: killing 12465 states (over memory cap)
KLEE: WARNING: killing 12224 states (over memory cap)
KLEE: WARNING: killing 11822 states (over memory cap)
KLEE: WARNING: killing 11729 states (over memory cap)
KLEE: WARNING: killing 12108 states (over memory cap)
KLEE: WARNING: killing 11394 states (over memory cap)
KLEE: WARNING: killing 11302 states (over memory cap)
KLEE: WARNING: killing 12227 states (over memory cap)
KLEE: WARNING: killing 11821 states (over memory cap)
KLEE: WARNING: killing 12121 states (over memory cap)
KLEE: WARNING: killing 11719 states (over memory cap)
KLEE: WARNING: killing 11632 states (over memory cap)
KLEE: WARNING: killing 11700 states (over memory cap)
KLEE: WARNING: killing 11689 states (over memory cap)
KLEE: WARNING: killing 11985 states (over memory cap)
KLEE: WARNING: killing 11588 states (over memory cap)
KLEE: WARNING: killing 12122 states (over memory cap)
KLEE: WARNING: killing 12263 states (over memory cap)
KLEE: WARNING: killing 11251 states (over memory cap)
KLEE: WARNING: killing 12627 states (over memory cap)
KLEE: WARNING: killing 11765 states (over memory cap)
KLEE: WARNING: killing 11751 states (over memory cap)
KLEE: WARNING: killing 11659 states (over memory cap)
KLEE: WARNING: killing 12267 states (over memory cap)
KLEE: WARNING: killing 11789 states (over memory cap)
KLEE: WARNING: killing 12091 states (over memory cap)
KLEE: WARNING: killing 12310 states (over memory cap)
KLEE: WARNING: killing 12298 states (over memory cap)
KLEE: WARNING: killing 11984 states (over memory cap)
KLEE: WARNING: killing 11902 states (over memory cap)
KLEE: WARNING: killing 11202 states (over memory cap)
KLEE: WARNING: killing 11644 states (over memory cap)
KLEE: WARNING: killing 11249 states (over memory cap)
KLEE: WARNING: killing 11923 states (over memory cap)
KLEE: WARNING: killing 11988 states (over memory cap)
KLEE: WARNING: killing 11829 states (over memory cap)
KLEE: WARNING: killing 11513 states (over memory cap)
KLEE: WARNING: killing 11957 states (over memory cap)
KLEE: WARNING: killing 12098 states (over memory cap)
KLEE: WARNING: killing 11560 states (over memory cap)
KLEE: WARNING: killing 11701 states (over memory cap)
KLEE: WARNING: killing 11844 states (over memory cap)
KLEE: WARNING: killing 11916 states (over memory cap)
KLEE: WARNING: killing 11599 states (over memory cap)
KLEE: WARNING: killing 12269 states (over memory cap)
KLEE: WARNING: killing 12029 states (over memory cap)
KLEE: WARNING: killing 11719 states (over memory cap)
KLEE: WARNING: killing 11786 states (over memory cap)
KLEE: WARNING: killing 11770 states (over memory cap)
KLEE: WARNING: killing 12365 states (over memory cap)
KLEE: WARNING: killing 11606 states (over memory cap)
KLEE: WARNING: killing 12416 states (over memory cap)
KLEE: WARNING: killing 11580 states (over memory cap)
KLEE: WARNING: killing 11492 states (over memory cap)
KLEE: WARNING: killing 11856 states (over memory cap)
KLEE: WARNING: killing 12521 states (over memory cap)
KLEE: WARNING: killing 11469 states (over memory cap)
KLEE: WARNING: killing 12281 states (over memory cap)
KLEE: WARNING: killing 12122 states (over memory cap)
KLEE: WARNING: killing 11669 states (over memory cap)
KLEE: WARNING: killing 11959 states (over memory cap)
KLEE: WARNING: killing 11723 states (over memory cap)
KLEE: WARNING: killing 11781 states (over memory cap)
KLEE: WARNING: killing 11844 states (over memory cap)
KLEE: WARNING: killing 11835 states (over memory cap)
KLEE: WARNING: killing 11524 states (over memory cap)
KLEE: WARNING: killing 11663 states (over memory cap)
KLEE: WARNING: killing 11582 states (over memory cap)
KLEE: WARNING: killing 12161 states (over memory cap)
KLEE: WARNING: killing 11785 states (over memory cap)
KLEE: WARNING: killing 11701 states (over memory cap)
KLEE: WARNING: killing 11915 states (over memory cap)
KLEE: WARNING: killing 12047 states (over memory cap)
KLEE: WARNING: killing 11816 states (over memory cap)
KLEE: WARNING: killing 12102 states (over memory cap)
KLEE: WARNING: killing 11943 states (over memory cap)
KLEE: WARNING: killing 12305 states (over memory cap)
KLEE: WARNING: killing 11635 states (over memory cap)
KLEE: WARNING: killing 11545 states (over memory cap)
KLEE: WARNING: killing 11977 states (over memory cap)
KLEE: WARNING: killing 12041 states (over memory cap)
KLEE: WARNING: killing 12256 states (over memory cap)
KLEE: WARNING: killing 11952 states (over memory cap)
KLEE: WARNING: killing 12239 states (over memory cap)
KLEE: WARNING: killing 12011 states (over memory cap)
KLEE: WARNING: killing 11777 states (over memory cap)
KLEE: WARNING: killing 11546 states (over memory cap)
KLEE: WARNING: killing 11900 states (over memory cap)
KLEE: WARNING: killing 11527 states (over memory cap)
KLEE: WARNING: killing 11228 states (over memory cap)
KLEE: WARNING: killing 12084 states (over memory cap)
KLEE: WARNING: killing 11640 states (over memory cap)
KLEE: WARNING: killing 11630 states (over memory cap)
KLEE: WARNING: killing 11912 states (over memory cap)
KLEE: WARNING: killing 12119 states (over memory cap)
KLEE: WARNING: killing 12179 states (over memory cap)
KLEE: WARNING: killing 11806 states (over memory cap)
KLEE: WARNING: killing 11866 states (over memory cap)
KLEE: WARNING: killing 11715 states (over memory cap)
KLEE: WARNING: killing 12206 states (over memory cap)
KLEE: WARNING: killing 11622 states (over memory cap)
KLEE: WARNING: killing 11900 states (over memory cap)
KLEE: WARNING: killing 11954 states (over memory cap)
KLEE: WARNING: killing 11807 states (over memory cap)
KLEE: WARNING: killing 11072 states (over memory cap)
KLEE: WARNING: killing 11420 states (over memory cap)
KLEE: WARNING: killing 11337 states (over memory cap)
KLEE: WARNING: killing 12041 states (over memory cap)
KLEE: WARNING: killing 12389 states (over memory cap)
KLEE: WARNING: killing 11952 states (over memory cap)
KLEE: WARNING: killing 12011 states (over memory cap)
KLEE: WARNING: killing 12501 states (over memory cap)
KLEE: WARNING: killing 12136 states (over memory cap)
KLEE: WARNING: killing 12341 states (over memory cap)
KLEE: WARNING: killing 12042 states (over memory cap)
KLEE: WARNING: killing 11965 states (over memory cap)
KLEE: WARNING: killing 11671 states (over memory cap)
KLEE: WARNING: killing 12232 states (over memory cap)
KLEE: WARNING: killing 11868 states (over memory cap)
KLEE: WARNING: killing 11715 states (over memory cap)
KLEE: WARNING: killing 11556 states (over memory cap)
KLEE: WARNING: killing 11757 states (over memory cap)
KLEE: WARNING: killing 11957 states (over memory cap)
KLEE: WARNING: killing 11662 states (over memory cap)
KLEE: WARNING: killing 12293 states (over memory cap)
KLEE: WARNING: killing 12066 states (over memory cap)
KLEE: WARNING: killing 12126 states (over memory cap)
KLEE: WARNING: killing 11766 states (over memory cap)
KLEE: WARNING: killing 12036 states (over memory cap)
KLEE: WARNING: killing 11464 states (over memory cap)
KLEE: WARNING: killing 11735 states (over memory cap)
KLEE: WARNING: killing 12145 states (over memory cap)
KLEE: WARNING: killing 11853 states (over memory cap)
KLEE: WARNING: killing 11354 states (over memory cap)
KLEE: WARNING: killing 11760 states (over memory cap)
KLEE: WARNING: killing 12101 states (over memory cap)
