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--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.: 121 294 2038 16195
Removed infinite loop in ib_send_cm_req
Removed infinite loop in cm_process_work
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.712121963501
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
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.757741928101
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 221 140 1085 9704
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_c704aa6b-ae91-4be6-b673-340d187d8dd6/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10985 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 11911 states (over memory cap)
KLEE: WARNING: killing 11101 states (over memory cap)
KLEE: WARNING: killing 11512 states (over memory cap)
KLEE: WARNING: killing 10615 states (over memory cap)
KLEE: WARNING: killing 10594 states (over memory cap)
KLEE: WARNING: killing 10742 states (over memory cap)
KLEE: WARNING: killing 10546 states (over memory cap)
KLEE: WARNING: killing 11380 states (over memory cap)
KLEE: WARNING: killing 11532 states (over memory cap)
KLEE: WARNING: killing 11936 states (over memory cap)
KLEE: WARNING: killing 11740 states (over memory cap)
KLEE: WARNING: killing 11381 states (over memory cap)
KLEE: WARNING: killing 12128 states (over memory cap)
KLEE: WARNING: killing 12023 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_jKf0y/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--core--ib_cm.ko-entry_point_true-unreach-call.cil.out.c:12959: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12514 states (over memory cap)
KLEE: WARNING: killing 11984 states (over memory cap)
KLEE: WARNING: killing 12048 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_jKf0y/linux-4.2-rc1.tar.xz-08_1a-drivers--infiniband--core--ib_cm.ko-entry_point_true-unreach-call.cil.out.c:13361: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12794 states (over memory cap)
KLEE: WARNING: killing 12270 states (over memory cap)
KLEE: WARNING: killing 12503 states (over memory cap)
KLEE: WARNING: killing 12997 states (over memory cap)
KLEE: WARNING: killing 13148 states (over memory cap)
KLEE: WARNING: killing 12121 states (over memory cap)
KLEE: WARNING: killing 12358 states (over memory cap)
KLEE: WARNING: killing 12345 states (over memory cap)
KLEE: WARNING: killing 11828 states (over memory cap)
KLEE: WARNING: killing 12475 states (over memory cap)
KLEE: WARNING: killing 12041 states (over memory cap)
KLEE: WARNING: killing 12444 states (over memory cap)
KLEE: WARNING: killing 11841 states (over memory cap)
KLEE: WARNING: killing 11662 states (over memory cap)
KLEE: WARNING: killing 11556 states (over memory cap)
KLEE: WARNING: killing 11290 states (over memory cap)
KLEE: WARNING: killing 12269 states (over memory cap)
KLEE: WARNING: killing 12257 states (over memory cap)
KLEE: WARNING: killing 12156 states (over memory cap)
KLEE: WARNING: killing 11645 states (over memory cap)
KLEE: WARNING: killing 11958 states (over memory cap)
KLEE: WARNING: killing 11940 states (over memory cap)
KLEE: WARNING: killing 11675 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_c704aa6b-ae91-4be6-b673-340d187d8dd6/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11658 states (over memory cap)
KLEE: WARNING: killing 12303 states (over memory cap)
KLEE: WARNING: killing 12286 states (over memory cap)
KLEE: WARNING: killing 12029 states (over memory cap)
KLEE: WARNING: killing 11688 states (over memory cap)
KLEE: WARNING: killing 11922 states (over memory cap)
KLEE: WARNING: killing 12151 states (over memory cap)
KLEE: WARNING: killing 11894 states (over memory cap)
KLEE: WARNING: killing 12124 states (over memory cap)
KLEE: WARNING: killing 11861 states (over memory cap)
KLEE: WARNING: killing 12902 states (over memory cap)
KLEE: WARNING: killing 12079 states (over memory cap)
KLEE: WARNING: killing 11986 states (over memory cap)
KLEE: WARNING: killing 11401 states (over memory cap)
KLEE: WARNING: killing 11792 states (over memory cap)
KLEE: WARNING: killing 11782 states (over memory cap)
KLEE: WARNING: killing 12090 states (over memory cap)
KLEE: WARNING: killing 12072 states (over memory cap)
KLEE: WARNING: killing 12060 states (over memory cap)
KLEE: WARNING: killing 11888 states (over memory cap)
KLEE: WARNING: killing 11951 states (over memory cap)
KLEE: WARNING: killing 11781 states (over memory cap)
KLEE: WARNING: killing 12245 states (over memory cap)
KLEE: WARNING: killing 12151 states (over memory cap)
KLEE: WARNING: killing 11742 states (over memory cap)
KLEE: WARNING: killing 11724 states (over memory cap)
KLEE: WARNING: killing 12036 states (over memory cap)
KLEE: WARNING: killing 12023 states (over memory cap)
KLEE: WARNING: killing 12091 states (over memory cap)
KLEE: WARNING: killing 12076 states (over memory cap)
KLEE: WARNING: killing 11587 states (over memory cap)
KLEE: WARNING: killing 11970 states (over memory cap)
KLEE: WARNING: killing 11882 states (over memory cap)
KLEE: WARNING: killing 11864 states (over memory cap)
KLEE: WARNING: killing 11375 states (over memory cap)
KLEE: WARNING: killing 12074 states (over memory cap)
KLEE: WARNING: killing 12227 states (over memory cap)
KLEE: WARNING: killing 12136 states (over memory cap)
KLEE: WARNING: killing 12517 states (over memory cap)
KLEE: WARNING: killing 11404 states (over memory cap)
KLEE: WARNING: killing 12020 states (over memory cap)
KLEE: WARNING: killing 11774 states (over memory cap)
KLEE: WARNING: killing 12231 states (over memory cap)
KLEE: WARNING: killing 11747 states (over memory cap)
KLEE: WARNING: killing 12051 states (over memory cap)
KLEE: WARNING: killing 11959 states (over memory cap)
KLEE: WARNING: killing 12339 states (over memory cap)
KLEE: WARNING: killing 12015 states (over memory cap)
KLEE: WARNING: killing 11612 states (over memory cap)
KLEE: WARNING: killing 11988 states (over memory cap)
KLEE: WARNING: killing 11901 states (over memory cap)
KLEE: WARNING: killing 11891 states (over memory cap)
KLEE: WARNING: killing 11954 states (over memory cap)
KLEE: WARNING: killing 11709 states (over memory cap)
KLEE: WARNING: killing 11780 states (over memory cap)
KLEE: WARNING: killing 11531 states (over memory cap)
KLEE: WARNING: killing 12293 states (over memory cap)
KLEE: WARNING: killing 11898 states (over memory cap)
KLEE: WARNING: killing 11967 states (over memory cap)
KLEE: WARNING: killing 12108 states (over memory cap)
KLEE: WARNING: killing 12174 states (over memory cap)
KLEE: WARNING: killing 11936 states (over memory cap)
KLEE: WARNING: killing 11692 states (over memory cap)
KLEE: WARNING: killing 11911 states (over memory cap)
KLEE: WARNING: killing 12130 states (over memory cap)
KLEE: WARNING: killing 11890 states (over memory cap)
KLEE: WARNING: killing 11649 states (over memory cap)
KLEE: WARNING: killing 12477 states (over memory cap)
KLEE: WARNING: killing 11551 states (over memory cap)
KLEE: WARNING: killing 11463 states (over memory cap)
KLEE: WARNING: killing 11828 states (over memory cap)
KLEE: WARNING: killing 12202 states (over memory cap)
KLEE: WARNING: killing 11886 states (over memory cap)
KLEE: WARNING: killing 11720 states (over memory cap)
KLEE: WARNING: killing 11786 states (over memory cap)
KLEE: WARNING: killing 11851 states (over memory cap)
KLEE: WARNING: killing 11837 states (over memory cap)
KLEE: WARNING: killing 11978 states (over memory cap)
KLEE: WARNING: killing 11893 states (over memory cap)
KLEE: WARNING: killing 11882 states (over memory cap)
KLEE: WARNING: killing 12399 states (over memory cap)
KLEE: WARNING: killing 11865 states (over memory cap)
KLEE: WARNING: killing 11850 states (over memory cap)
KLEE: WARNING: killing 11692 states (over memory cap)
KLEE: WARNING: killing 11907 states (over memory cap)
KLEE: WARNING: killing 11900 states (over memory cap)
KLEE: WARNING: killing 12268 states (over memory cap)
KLEE: WARNING: killing 11581 states (over memory cap)
KLEE: WARNING: killing 11791 states (over memory cap)
KLEE: WARNING: killing 12083 states (over memory cap)
KLEE: WARNING: killing 12148 states (over memory cap)
KLEE: WARNING: killing 11837 states (over memory cap)
KLEE: WARNING: killing 12123 states (over memory cap)
KLEE: WARNING: killing 11439 states (over memory cap)
KLEE: WARNING: killing 11952 states (over memory cap)
KLEE: WARNING: killing 11716 states (over memory cap)
KLEE: WARNING: killing 11481 states (over memory cap)
KLEE: WARNING: killing 11916 states (over memory cap)
KLEE: WARNING: killing 11759 states (over memory cap)
KLEE: WARNING: killing 11819 states (over memory cap)
KLEE: WARNING: killing 11588 states (over memory cap)
KLEE: WARNING: killing 12621 states (over memory cap)
KLEE: WARNING: killing 12093 states (over memory cap)
KLEE: WARNING: killing 11706 states (over memory cap)
KLEE: WARNING: killing 11625 states (over memory cap)
KLEE: WARNING: killing 12207 states (over memory cap)
KLEE: WARNING: killing 11979 states (over memory cap)
KLEE: WARNING: killing 11893 states (over memory cap)
KLEE: WARNING: killing 12253 states (over memory cap)
KLEE: WARNING: killing 12023 states (over memory cap)
KLEE: WARNING: killing 12315 states (over memory cap)
KLEE: WARNING: killing 11632 states (over memory cap)
KLEE: WARNING: killing 12068 states (over memory cap)
KLEE: WARNING: killing 11911 states (over memory cap)
KLEE: WARNING: killing 11974 states (over memory cap)
KLEE: WARNING: killing 11528 states (over memory cap)
KLEE: WARNING: killing 11659 states (over memory cap)
KLEE: WARNING: killing 11945 states (over memory cap)
KLEE: WARNING: killing 11564 states (over memory cap)
KLEE: WARNING: killing 12219 states (over memory cap)
KLEE: WARNING: killing 11915 states (over memory cap)
KLEE: WARNING: killing 12122 states (over memory cap)
KLEE: WARNING: killing 11821 states (over memory cap)
KLEE: WARNING: killing 11806 states (over memory cap)
KLEE: WARNING: killing 11943 states (over memory cap)
KLEE: WARNING: killing 12078 states (over memory cap)
KLEE: WARNING: killing 12216 states (over memory cap)
KLEE: WARNING: killing 11841 states (over memory cap)
KLEE: WARNING: killing 11684 states (over memory cap)
KLEE: WARNING: killing 11817 states (over memory cap)
KLEE: WARNING: killing 11662 states (over memory cap)
KLEE: WARNING: killing 12308 states (over memory cap)
KLEE: WARNING: killing 12009 states (over memory cap)
KLEE: WARNING: killing 11485 states (over memory cap)
KLEE: WARNING: killing 11839 states (over memory cap)
KLEE: WARNING: killing 11613 states (over memory cap)
KLEE: WARNING: killing 12037 states (over memory cap)
KLEE: WARNING: killing 11666 states (over memory cap)
KLEE: WARNING: killing 11943 states (over memory cap)
KLEE: WARNING: killing 11863 states (over memory cap)
KLEE: WARNING: killing 12066 states (over memory cap)
KLEE: WARNING: killing 11770 states (over memory cap)
KLEE: WARNING: killing 11685 states (over memory cap)
KLEE: WARNING: killing 12180 states (over memory cap)
KLEE: WARNING: killing 12026 states (over memory cap)
KLEE: WARNING: killing 11940 states (over memory cap)
KLEE: WARNING: killing 11855 states (over memory cap)
KLEE: WARNING: killing 12208 states (over memory cap)
KLEE: WARNING: killing 11694 states (over memory cap)
KLEE: WARNING: killing 12042 states (over memory cap)
KLEE: WARNING: killing 11817 states (over memory cap)
KLEE: WARNING: killing 12023 states (over memory cap)
KLEE: WARNING: killing 11438 states (over memory cap)
KLEE: WARNING: killing 12000 states (over memory cap)
KLEE: WARNING: killing 11992 states (over memory cap)
KLEE: WARNING: killing 11764 states (over memory cap)
KLEE: WARNING: killing 12039 states (over memory cap)
KLEE: WARNING: killing 12241 states (over memory cap)
KLEE: WARNING: killing 11947 states (over memory cap)
KLEE: WARNING: killing 12149 states (over memory cap)
KLEE: WARNING: killing 12071 states (over memory cap)
KLEE: WARNING: killing 11845 states (over memory cap)
KLEE: WARNING: killing 11973 states (over memory cap)
KLEE: WARNING: killing 11752 states (over memory cap)
KLEE: WARNING: killing 11744 states (over memory cap)
KLEE: WARNING: killing 11942 states (over memory cap)
KLEE: WARNING: killing 12283 states (over memory cap)
KLEE: WARNING: killing 11851 states (over memory cap)
KLEE: WARNING: killing 11701 states (over memory cap)
KLEE: WARNING: killing 11899 states (over memory cap)
KLEE: WARNING: killing 12314 states (over memory cap)
KLEE: WARNING: killing 11882 states (over memory cap)
KLEE: WARNING: killing 11447 states (over memory cap)
KLEE: WARNING: killing 11786 states (over memory cap)
KLEE: WARNING: killing 12197 states (over memory cap)
KLEE: WARNING: killing 12400 states (over memory cap)
KLEE: WARNING: killing 11408 states (over memory cap)
KLEE: WARNING: killing 12097 states (over memory cap)
KLEE: WARNING: killing 11943 states (over memory cap)
KLEE: WARNING: killing 11863 states (over memory cap)
