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-43_2a-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.: 237 202 1910 14480
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.565759897232
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'warn_slowpath_null' (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 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)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function atomic_notifier_chain_unregister as symbolic
Defining function del_timer_sync as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strlen
  strncpy
  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.617264986038
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 346 158 1077 11303
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_518bb24f-d35f-4cc9-a168-e0b34c4c7875/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 20089 states (over memory cap)
KLEE: WARNING: killing 17334 states (over memory cap)
KLEE: WARNING: killing 17229 states (over memory cap)
KLEE: WARNING: killing 16403 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7058: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:6932: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7095: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16960 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7022: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7040: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:6950: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:6986: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:7076: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:6968: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16788 states (over memory cap)
KLEE: WARNING: killing 16499 states (over memory cap)
KLEE: WARNING: killing 15223 states (over memory cap)
KLEE: WARNING: killing 16817 states (over memory cap)
KLEE: WARNING: killing 16595 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:9497: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19486 states (over memory cap)
KLEE: WARNING: killing 18228 states (over memory cap)
KLEE: WARNING: killing 20274 states (over memory cap)
KLEE: WARNING: killing 20386 states (over memory cap)
KLEE: WARNING: killing 20171 states (over memory cap)
KLEE: WARNING: killing 19954 states (over memory cap)
KLEE: WARNING: killing 20961 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:3974: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21196 states (over memory cap)
KLEE: WARNING: killing 20271 states (over memory cap)
KLEE: WARNING: killing 20254 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-wTE7DV/linux-4.2-rc1.tar.xz-43_2a-drivers--char--ipmi--ipmi_msghandler.ko-entry_point_true-unreach-call.cil.out.c:3817: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 19326 states (over memory cap)
KLEE: WARNING: killing 19874 states (over memory cap)
KLEE: WARNING: killing 21062 states (over memory cap)
KLEE: WARNING: killing 20010 states (over memory cap)
KLEE: WARNING: killing 19921 states (over memory cap)
KLEE: WARNING: killing 19506 states (over memory cap)
KLEE: WARNING: killing 18782 states (over memory cap)
KLEE: WARNING: killing 20529 states (over memory cap)
KLEE: WARNING: killing 20564 states (over memory cap)
KLEE: WARNING: killing 19646 states (over memory cap)
KLEE: WARNING: killing 20579 states (over memory cap)
KLEE: WARNING: killing 20376 states (over memory cap)
KLEE: WARNING: killing 20285 states (over memory cap)
KLEE: WARNING: killing 20390 states (over memory cap)
KLEE: WARNING: killing 20298 states (over memory cap)
KLEE: WARNING: killing 20974 states (over memory cap)
KLEE: WARNING: killing 19939 states (over memory cap)
KLEE: WARNING: killing 21054 states (over memory cap)
KLEE: WARNING: killing 20019 states (over memory cap)
KLEE: WARNING: killing 19312 states (over memory cap)
KLEE: WARNING: killing 19475 states (over memory cap)
KLEE: WARNING: killing 20648 states (over memory cap)
KLEE: WARNING: killing 20248 states (over memory cap)
KLEE: WARNING: killing 19409 states (over memory cap)
KLEE: WARNING: killing 20321 states (over memory cap)
KLEE: WARNING: killing 20423 states (over memory cap)
KLEE: WARNING: killing 20146 states (over memory cap)
KLEE: WARNING: killing 20565 states (over memory cap)
KLEE: WARNING: killing 18797 states (over memory cap)
KLEE: WARNING: killing 20210 states (over memory cap)
KLEE: WARNING: killing 20631 states (over memory cap)
KLEE: WARNING: killing 20544 states (over memory cap)
KLEE: WARNING: killing 19720 states (over memory cap)
KLEE: WARNING: killing 20315 states (over memory cap)
KLEE: WARNING: killing 19987 states (over memory cap)
KLEE: WARNING: killing 20908 states (over memory cap)
KLEE: WARNING: killing 19639 states (over memory cap)
KLEE: WARNING: killing 19490 states (over memory cap)
KLEE: WARNING: killing 20153 states (over memory cap)
KLEE: WARNING: killing 20132 states (over memory cap)
KLEE: WARNING: killing 19988 states (over memory cap)
KLEE: WARNING: killing 20336 states (over memory cap)
KLEE: WARNING: killing 20189 states (over memory cap)
KLEE: WARNING: killing 19683 states (over memory cap)
KLEE: WARNING: killing 19848 states (over memory cap)
KLEE: WARNING: killing 19882 states (over memory cap)
KLEE: WARNING: killing 19376 states (over memory cap)
KLEE: WARNING: killing 21729 states (over memory cap)
KLEE: WARNING: killing 20867 states (over memory cap)
KLEE: WARNING: killing 19993 states (over memory cap)
KLEE: WARNING: killing 20463 states (over memory cap)
KLEE: WARNING: killing 19834 states (over memory cap)
KLEE: WARNING: killing 19563 states (over memory cap)
KLEE: WARNING: killing 20461 states (over memory cap)
KLEE: WARNING: killing 18795 states (over memory cap)
KLEE: WARNING: killing 20349 states (over memory cap)
KLEE: WARNING: killing 19848 states (over memory cap)
KLEE: WARNING: killing 20435 states (over memory cap)
KLEE: WARNING: killing 19995 states (over memory cap)
KLEE: WARNING: killing 20332 states (over memory cap)
KLEE: WARNING: killing 20258 states (over memory cap)
KLEE: WARNING: killing 20188 states (over memory cap)
KLEE: WARNING: killing 20710 states (over memory cap)
KLEE: WARNING: killing 19730 states (over memory cap)
KLEE: WARNING: killing 20254 states (over memory cap)
KLEE: WARNING: killing 20115 states (over memory cap)
KLEE: WARNING: killing 21483 states (over memory cap)
KLEE: WARNING: killing 20146 states (over memory cap)
KLEE: WARNING: killing 20477 states (over memory cap)
KLEE: WARNING: killing 19982 states (over memory cap)
KLEE: WARNING: killing 20566 states (over memory cap)
KLEE: WARNING: killing 19948 states (over memory cap)
KLEE: WARNING: killing 20641 states (over memory cap)
KLEE: WARNING: killing 20328 states (over memory cap)
KLEE: WARNING: killing 19115 states (over memory cap)
KLEE: WARNING: killing 20170 states (over memory cap)
KLEE: WARNING: killing 19854 states (over memory cap)
KLEE: WARNING: killing 20258 states (over memory cap)
KLEE: WARNING: killing 19947 states (over memory cap)
KLEE: WARNING: killing 19388 states (over memory cap)
KLEE: WARNING: killing 19790 states (over memory cap)
KLEE: WARNING: killing 20005 states (over memory cap)
KLEE: WARNING: killing 20529 states (over memory cap)
KLEE: WARNING: killing 20094 states (over memory cap)
KLEE: WARNING: killing 20374 states (over memory cap)
KLEE: WARNING: killing 21606 states (over memory cap)
KLEE: WARNING: killing 19995 states (over memory cap)
KLEE: WARNING: killing 20219 states (over memory cap)
KLEE: WARNING: killing 20254 states (over memory cap)
KLEE: WARNING: killing 20365 states (over memory cap)
KLEE: WARNING: killing 19812 states (over memory cap)
KLEE: WARNING: killing 19973 states (over memory cap)
KLEE: WARNING: killing 19483 states (over memory cap)
KLEE: WARNING: killing 21168 states (over memory cap)
KLEE: WARNING: killing 19679 states (over memory cap)
KLEE: WARNING: killing 19960 states (over memory cap)
KLEE: WARNING: killing 19874 states (over memory cap)
KLEE: WARNING: killing 20570 states (over memory cap)
KLEE: WARNING: killing 19905 states (over memory cap)
KLEE: WARNING: killing 21246 states (over memory cap)
KLEE: WARNING: killing 19766 states (over memory cap)
KLEE: WARNING: killing 19984 states (over memory cap)
KLEE: WARNING: killing 20017 states (over memory cap)
KLEE: WARNING: killing 20585 states (over memory cap)
KLEE: WARNING: killing 20218 states (over memory cap)
KLEE: WARNING: killing 20672 states (over memory cap)
KLEE: WARNING: killing 20198 states (over memory cap)
KLEE: WARNING: killing 19828 states (over memory cap)
KLEE: WARNING: killing 20856 states (over memory cap)
KLEE: WARNING: killing 19272 states (over memory cap)
KLEE: WARNING: killing 19540 states (over memory cap)
KLEE: WARNING: killing 20453 states (over memory cap)
KLEE: WARNING: killing 20839 states (over memory cap)
KLEE: WARNING: killing 20601 states (over memory cap)
KLEE: WARNING: killing 19424 states (over memory cap)
KLEE: WARNING: killing 19874 states (over memory cap)
KLEE: WARNING: killing 20318 states (over memory cap)
KLEE: WARNING: killing 19317 states (over memory cap)
KLEE: WARNING: killing 20631 states (over memory cap)
KLEE: WARNING: killing 20442 states (over memory cap)
KLEE: WARNING: killing 20834 states (over memory cap)
KLEE: WARNING: killing 19726 states (over memory cap)
KLEE: WARNING: killing 19817 states (over memory cap)
KLEE: WARNING: killing 20201 states (over memory cap)
KLEE: WARNING: killing 22086 states (over memory cap)
KLEE: WARNING: killing 19945 states (over memory cap)
KLEE: WARNING: killing 18843 states (over memory cap)
KLEE: WARNING: killing 19974 states (over memory cap)
KLEE: WARNING: killing 19949 states (over memory cap)
KLEE: WARNING: killing 19247 states (over memory cap)
