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--char--ipmi--ipmi_msghandler.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.: 244 337 2370 16474
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.714996099472
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'driver_unregister' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function try_module_get as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function mod_timer as symbolic
Defining function driver_register as symbolic
Defining function printk as symbolic
Defining function proc_mkdir as symbolic
Defining function atomic_notifier_chain_register as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_watching as symbolic
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function kstrdup as symbolic
Defining function proc_create_data as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function snprintf as symbolic
Defining function platform_device_register as symbolic
Defining function sysfs_create_link as symbolic
Defining function kasprintf as symbolic
Removed calls to 'sysfs_remove_link' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Defining function driver_find_device as symbolic
Defining function sprintf as symbolic
Defining function schedule_timeout as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function PDE_DATA as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_putc as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'proc_remove' (function is undefined)
Defining function atomic_notifier_chain_unregister as symbolic
Defining function del_timer_sync as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strlen
  strncpy
  __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.804121017456
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 351 294 1571 12690
INFO: Starting verification
KLEE: WARNING ONCE: function "ipmi_smi_watcher_register" has inline asm
KLEE: WARNING ONCE: function "kref_get" has inline asm
KLEE: WARNING ONCE: function "ipmi_free_recv_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_create_user" has inline asm
KLEE: WARNING ONCE: function "ipmi_timeout" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "ipmi_alloc_smi_msg" has inline asm
KLEE: WARNING ONCE: function "deliver_response" has inline asm
KLEE: WARNING ONCE: function "tasklet_schedule" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "free_smi_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_destroy_user" has inline asm
KLEE: WARNING ONCE: function "ipmi_set_gets_events" has inline asm
KLEE: WARNING ONCE: function "ipmi_register_for_cmd" has inline asm
KLEE: WARNING ONCE: function "ipmi_unregister_for_cmd" has inline asm
KLEE: WARNING ONCE: function "i_ipmi_request" has inline asm
KLEE: WARNING ONCE: function "ipmi_alloc_recv_msg" has inline asm
KLEE: WARNING ONCE: function "free_recv_msg" has inline asm
KLEE: WARNING ONCE: function "handle_new_recv_msgs" has inline asm
KLEE: WARNING ONCE: function "handle_one_recv_msg" has inline asm
KLEE: WARNING ONCE: function "ipmi_register_smi" has inline asm
KLEE: WARNING ONCE: function "ipmi_bmc_unregister" has inline asm
KLEE: WARNING ONCE: function "ipmi_unregister_smi" has inline asm
KLEE: WARNING ONCE: function "ipmi_smi_msg_received" has inline asm
KLEE: WARNING ONCE: function "ipmi_panic_request_and_wait" has inline asm
KLEE: WARNING ONCE: function "dummy_smi_done_handler" has inline asm
KLEE: WARNING ONCE: function "dummy_recv_done_handler" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
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_fdab8904-b11d-46c2-8d4e-9ee72cfabb0d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7088: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7142: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7178: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7070: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7052: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7197: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7034: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7124: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7160: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:9617: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14127 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 16337 states (over memory cap)
KLEE: WARNING: killing 16683 states (over memory cap)
KLEE: WARNING: killing 16115 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:3701: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hP3DID/linux-4.2-rc1.tar.xz-32_7a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:4042: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16868 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 17185 states (over memory cap)
KLEE: WARNING: killing 15907 states (over memory cap)
KLEE: WARNING: killing 17047 states (over memory cap)
KLEE: WARNING: killing 18318 states (over memory cap)
KLEE: WARNING: killing 18419 states (over memory cap)
KLEE: WARNING: killing 18447 states (over memory cap)
KLEE: WARNING: killing 20111 states (over memory cap)
KLEE: WARNING: killing 19763 states (over memory cap)
KLEE: WARNING: killing 20445 states (over memory cap)
KLEE: WARNING: killing 19648 states (over memory cap)
KLEE: WARNING: killing 21695 states (over memory cap)
KLEE: WARNING: killing 20648 states (over memory cap)
KLEE: WARNING: killing 19463 states (over memory cap)
KLEE: WARNING: killing 20535 states (over memory cap)
KLEE: WARNING: killing 19862 states (over memory cap)
KLEE: WARNING: killing 19257 states (over memory cap)
KLEE: WARNING: killing 20768 states (over memory cap)
KLEE: WARNING: killing 19657 states (over memory cap)
KLEE: WARNING: killing 20078 states (over memory cap)
KLEE: WARNING: killing 19357 states (over memory cap)
KLEE: WARNING: killing 18367 states (over memory cap)
KLEE: WARNING: killing 19934 states (over memory cap)
KLEE: WARNING: killing 19276 states (over memory cap)
KLEE: WARNING: killing 20078 states (over memory cap)
KLEE: WARNING: killing 19357 states (over memory cap)
KLEE: WARNING: killing 20031 states (over memory cap)
KLEE: WARNING: killing 20705 states (over memory cap)
KLEE: WARNING: killing 20045 states (over memory cap)
KLEE: WARNING: killing 20212 states (over memory cap)
KLEE: WARNING: killing 20445 states (over memory cap)
KLEE: WARNING: killing 21045 states (over memory cap)
KLEE: WARNING: killing 20586 states (over memory cap)
KLEE: WARNING: killing 20243 states (over memory cap)
KLEE: WARNING: killing 19908 states (over memory cap)
KLEE: WARNING: killing 19191 states (over memory cap)
KLEE: WARNING: killing 20492 states (over memory cap)
KLEE: WARNING: killing 20723 states (over memory cap)
KLEE: WARNING: killing 20451 states (over memory cap)
KLEE: WARNING: killing 20363 states (over memory cap)
KLEE: WARNING: killing 19589 states (over memory cap)
KLEE: WARNING: killing 19315 states (over memory cap)
KLEE: WARNING: killing 19663 states (over memory cap)
KLEE: WARNING: killing 20577 states (over memory cap)
KLEE: WARNING: killing 19374 states (over memory cap)
KLEE: WARNING: killing 20409 states (over memory cap)
KLEE: WARNING: killing 20268 states (over memory cap)
KLEE: WARNING: killing 19193 states (over memory cap)
KLEE: WARNING: killing 18928 states (over memory cap)
KLEE: WARNING: killing 19583 states (over memory cap)
KLEE: WARNING: killing 19564 states (over memory cap)
KLEE: WARNING: killing 20532 states (over memory cap)
KLEE: WARNING: killing 20339 states (over memory cap)
KLEE: WARNING: killing 20320 states (over memory cap)
KLEE: WARNING: killing 20608 states (over memory cap)
KLEE: WARNING: killing 20225 states (over memory cap)
KLEE: WARNING: killing 20137 states (over memory cap)
KLEE: WARNING: killing 19869 states (over memory cap)
KLEE: WARNING: killing 20465 states (over memory cap)
KLEE: WARNING: killing 19710 states (over memory cap)
KLEE: WARNING: killing 20174 states (over memory cap)
KLEE: WARNING: killing 20331 states (over memory cap)
KLEE: WARNING: killing 20254 states (over memory cap)
KLEE: WARNING: killing 19802 states (over memory cap)
KLEE: WARNING: killing 20392 states (over memory cap)
KLEE: WARNING: killing 19393 states (over memory cap)
KLEE: WARNING: killing 19622 states (over memory cap)
KLEE: WARNING: killing 20637 states (over memory cap)
KLEE: WARNING: killing 19710 states (over memory cap)
KLEE: WARNING: killing 20303 states (over memory cap)
KLEE: WARNING: killing 19188 states (over memory cap)
KLEE: WARNING: killing 20266 states (over memory cap)
KLEE: WARNING: killing 20133 states (over memory cap)
KLEE: WARNING: killing 21137 states (over memory cap)
KLEE: WARNING: killing 19970 states (over memory cap)
KLEE: WARNING: killing 19465 states (over memory cap)
KLEE: WARNING: killing 20289 states (over memory cap)
KLEE: WARNING: killing 20141 states (over memory cap)
KLEE: WARNING: killing 19703 states (over memory cap)
KLEE: WARNING: killing 20595 states (over memory cap)
KLEE: WARNING: killing 19728 states (over memory cap)
KLEE: WARNING: killing 20132 states (over memory cap)
KLEE: WARNING: killing 19450 states (over memory cap)
KLEE: WARNING: killing 19550 states (over memory cap)
KLEE: WARNING: killing 19417 states (over memory cap)
KLEE: WARNING: killing 20725 states (over memory cap)
KLEE: WARNING: killing 19627 states (over memory cap)
KLEE: WARNING: killing 20087 states (over memory cap)
KLEE: WARNING: killing 20066 states (over memory cap)
KLEE: WARNING: killing 19686 states (over memory cap)
KLEE: WARNING: killing 20751 states (over memory cap)
KLEE: WARNING: killing 20974 states (over memory cap)
KLEE: WARNING: killing 19349 states (over memory cap)
KLEE: WARNING: killing 20829 states (over memory cap)
KLEE: WARNING: killing 19321 states (over memory cap)
KLEE: WARNING: killing 19961 states (over memory cap)
KLEE: WARNING: killing 19824 states (over memory cap)
KLEE: WARNING: killing 20405 states (over memory cap)
KLEE: WARNING: killing 20215 states (over memory cap)
KLEE: WARNING: killing 18885 states (over memory cap)
KLEE: WARNING: killing 20045 states (over memory cap)
KLEE: WARNING: killing 19556 states (over memory cap)
KLEE: WARNING: killing 20601 states (over memory cap)
KLEE: WARNING: killing 20483 states (over memory cap)
KLEE: WARNING: killing 19396 states (over memory cap)
KLEE: WARNING: killing 18562 states (over memory cap)
KLEE: WARNING: killing 20963 states (over memory cap)
KLEE: WARNING: killing 20061 states (over memory cap)
KLEE: WARNING: killing 19806 states (over memory cap)
KLEE: WARNING: killing 19676 states (over memory cap)
KLEE: WARNING: killing 19657 states (over memory cap)
KLEE: WARNING: killing 20885 states (over memory cap)
KLEE: WARNING: killing 21107 states (over memory cap)
KLEE: WARNING: killing 20149 states (over memory cap)
KLEE: WARNING: killing 19601 states (over memory cap)
KLEE: WARNING: killing 19744 states (over memory cap)
KLEE: WARNING: killing 19442 states (over memory cap)
KLEE: WARNING: killing 20130 states (over memory cap)
KLEE: WARNING: killing 19524 states (over memory cap)
KLEE: WARNING: killing 20094 states (over memory cap)
KLEE: WARNING: killing 20137 states (over memory cap)
KLEE: WARNING: killing 19942 states (over memory cap)
KLEE: WARNING: killing 20803 states (over memory cap)
KLEE: WARNING: killing 20736 states (over memory cap)
KLEE: WARNING: killing 21014 states (over memory cap)
KLEE: WARNING: killing 19485 states (over memory cap)
KLEE: WARNING: killing 19128 states (over memory cap)
KLEE: WARNING: killing 20266 states (over memory cap)
KLEE: WARNING: killing 19600 states (over memory cap)
KLEE: WARNING: killing 19464 states (over memory cap)
KLEE: WARNING: killing 19563 states (over memory cap)
KLEE: WARNING: killing 20706 states (over memory cap)
KLEE: WARNING: killing 19540 states (over memory cap)
KLEE: WARNING: killing 20739 states (over memory cap)
KLEE: WARNING: killing 20263 states (over memory cap)
KLEE: WARNING: killing 19665 states (over memory cap)
KLEE: WARNING: killing 19996 states (over memory cap)
KLEE: WARNING: killing 20209 states (over memory cap)
KLEE: WARNING: killing 20252 states (over memory cap)
KLEE: WARNING: killing 19829 states (over memory cap)
KLEE: WARNING: killing 19983 states (over memory cap)
KLEE: WARNING: killing 19978 states (over memory cap)
KLEE: WARNING: killing 19668 states (over memory cap)
KLEE: WARNING: killing 19476 states (over memory cap)
