bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--char--ipmi--ipmi_msghandler.ko-main.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.: 147 271 2052 14750
INFO: Compilation, preparation and instrumentation time: 0.664960861206
Removed calls to 'warn_slowpath_null' (function is undefined)
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 'mutex_unlock' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function seq_putc as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave 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_cpu_idle as symbolic
Defining function printk as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Removed calls to 'module_put' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function try_module_get as symbolic
Defining function driver_register as symbolic
Defining function proc_mkdir as symbolic
Removed calls to '__tasklet_schedule' (function is undefined)
Defining function mod_timer as symbolic
Defining function atomic_notifier_chain_register as symbolic
Removed calls to '__list_del_entry' (function is undefined)
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 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'platform_device_put' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function autoremove_wake_function as symbolic
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function snprintf as symbolic
Defining function platform_device_alloc as symbolic
Defining function dev_set_drvdata as symbolic
Defining function platform_device_add as symbolic
Defining function _dev_info as symbolic
Defining function kstrdup as symbolic
Defining function sysfs_create_link as symbolic
Removed calls to 'sysfs_remove_link' (function is undefined)
Defining function device_create_file as symbolic
Defining function dev_get_drvdata as symbolic
Defining function driver_find_device as symbolic
Defining function sprintf as symbolic
Removed calls to 'driver_unregister' (function is undefined)
Defining function ldv_smi_ipmb_proc_ops_release as symbolic
Defining function ldv_smi_stats_proc_ops_release as symbolic
Defining function ldv_smi_version_proc_ops_release as symbolic
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
  strcpy
  strlen
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.682152032852
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 279 237 1464 12388
INFO: Starting verification
KLEE: WARNING ONCE: function "ipmi_smi_watcher_register" has inline asm
KLEE: WARNING ONCE: function "ipmi_free_recv_msg" 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 "i_ipmi_request" has inline asm
KLEE: WARNING ONCE: function "handle_new_recv_msgs" has inline asm
KLEE: WARNING ONCE: function "deliver_response" has inline asm
KLEE: WARNING ONCE: function "rcu_read_lock" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" 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 "ipmi_alloc_smi_msg" has inline asm
KLEE: WARNING ONCE: function "free_smi_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 "ipmi_destroy_user" has inline asm
KLEE: WARNING ONCE: function "ipmi_set_gets_events" 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_smi_watchdog_pretimeout" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: ERROR: /tmp/symbiotic-5AuV5h/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--char--ipmi--ipmi_msghandler.ko-main.cil.out.c:3885: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-5AuV5h/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--char--ipmi--ipmi_msghandler.ko-main.cil.out.c:3885: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-5AuV5h/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--char--ipmi--ipmi_msghandler.ko-main.cil.out.c:3885: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-5AuV5h/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--char--ipmi--ipmi_msghandler.ko-main.cil.out.c:3364: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-5AuV5h/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--char--ipmi--ipmi_msghandler.ko-main.cil.out.c:8615: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-5AuV5h/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--char--ipmi--ipmi_msghandler.ko-main.cil.out.c:8615: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 17761 states (over memory cap)
KLEE: WARNING: killing 10684 states (over memory cap)
KLEE: WARNING: killing 10360 states (over memory cap)
KLEE: WARNING: killing 10138 states (over memory cap)
KLEE: WARNING: killing 10304 states (over memory cap)
KLEE: WARNING: killing 9795 states (over memory cap)
KLEE: WARNING: killing 10248 states (over memory cap)
KLEE: WARNING: killing 10512 states (over memory cap)
KLEE: WARNING: killing 9910 states (over memory cap)
KLEE: WARNING: killing 9886 states (over memory cap)
KLEE: WARNING: killing 10529 states (over memory cap)
KLEE: WARNING: killing 10316 states (over memory cap)
KLEE: WARNING: killing 10481 states (over memory cap)
KLEE: WARNING: killing 10558 states (over memory cap)
KLEE: WARNING: killing 10535 states (over memory cap)
KLEE: WARNING: killing 10893 states (over memory cap)
KLEE: WARNING: killing 10962 states (over memory cap)
KLEE: WARNING: killing 10471 states (over memory cap)
KLEE: WARNING: killing 10642 states (over memory cap)
KLEE: WARNING: killing 10532 states (over memory cap)
KLEE: WARNING: killing 10790 states (over memory cap)
KLEE: WARNING: killing 10866 states (over memory cap)
KLEE: WARNING: killing 10941 states (over memory cap)
KLEE: WARNING: killing 10368 states (over memory cap)
KLEE: WARNING: killing 10437 states (over memory cap)
KLEE: WARNING: killing 10513 states (over memory cap)
KLEE: WARNING: killing 10775 states (over memory cap)
KLEE: WARNING: killing 10574 states (over memory cap)
KLEE: WARNING: killing 10458 states (over memory cap)
KLEE: WARNING: killing 10443 states (over memory cap)
KLEE: WARNING: killing 10236 states (over memory cap)
KLEE: WARNING: killing 10406 states (over memory cap)
KLEE: WARNING: killing 10293 states (over memory cap)
KLEE: WARNING: killing 10182 states (over memory cap)
KLEE: WARNING: killing 10808 states (over memory cap)
KLEE: WARNING: killing 10701 states (over memory cap)
KLEE: WARNING: killing 10410 states (over memory cap)
KLEE: WARNING: killing 10212 states (over memory cap)
KLEE: WARNING: killing 10468 states (over memory cap)
KLEE: WARNING: killing 10264 states (over memory cap)
KLEE: WARNING: killing 10160 states (over memory cap)
KLEE: WARNING: killing 10417 states (over memory cap)
KLEE: WARNING: killing 10399 states (over memory cap)
KLEE: WARNING: killing 10469 states (over memory cap)
KLEE: WARNING: killing 10188 states (over memory cap)
KLEE: WARNING: killing 10350 states (over memory cap)
KLEE: WARNING: killing 10245 states (over memory cap)
KLEE: WARNING: killing 10501 states (over memory cap)
KLEE: WARNING: killing 10572 states (over memory cap)
KLEE: WARNING: killing 10288 states (over memory cap)
KLEE: WARNING: killing 10274 states (over memory cap)
KLEE: WARNING: killing 10085 states (over memory cap)
KLEE: WARNING: killing 10159 states (over memory cap)
KLEE: WARNING: killing 10231 states (over memory cap)
KLEE: WARNING: killing 10392 states (over memory cap)
KLEE: WARNING: killing 10376 states (over memory cap)
KLEE: WARNING: killing 10625 states (over memory cap)
KLEE: WARNING: killing 10348 states (over memory cap)
KLEE: WARNING: killing 10332 states (over memory cap)
KLEE: WARNING: killing 10146 states (over memory cap)
KLEE: WARNING: killing 10218 states (over memory cap)
KLEE: WARNING: killing 10293 states (over memory cap)
KLEE: WARNING: killing 10275 states (over memory cap)
KLEE: WARNING: killing 10171 states (over memory cap)
KLEE: WARNING: killing 10159 states (over memory cap)
KLEE: WARNING: killing 10406 states (over memory cap)
KLEE: WARNING: killing 10389 states (over memory cap)
KLEE: WARNING: killing 10470 states (over memory cap)
KLEE: WARNING: killing 10018 states (over memory cap)
KLEE: WARNING: killing 10439 states (over memory cap)
KLEE: WARNING: killing 10775 states (over memory cap)
KLEE: WARNING: killing 10411 states (over memory cap)
KLEE: WARNING: killing 10135 states (over memory cap)
KLEE: WARNING: killing 10211 states (over memory cap)
KLEE: WARNING: killing 10109 states (over memory cap)
KLEE: WARNING: killing 10524 states (over memory cap)
KLEE: WARNING: killing 9997 states (over memory cap)
KLEE: WARNING: killing 10242 states (over memory cap)
KLEE: WARNING: killing 10226 states (over memory cap)
KLEE: WARNING: killing 10475 states (over memory cap)
KLEE: WARNING: killing 10379 states (over memory cap)
KLEE: WARNING: killing 10447 states (over memory cap)
KLEE: WARNING: killing 10349 states (over memory cap)
KLEE: WARNING: killing 10253 states (over memory cap)
KLEE: WARNING: killing 10154 states (over memory cap)
KLEE: WARNING: killing 10397 states (over memory cap)
KLEE: WARNING: killing 10299 states (over memory cap)
KLEE: WARNING: killing 10283 states (over memory cap)
KLEE: WARNING: killing 10102 states (over memory cap)
KLEE: WARNING: killing 10086 states (over memory cap)
KLEE: WARNING: killing 10069 states (over memory cap)
KLEE: WARNING: killing 10142 states (over memory cap)
KLEE: WARNING: killing 10465 states (over memory cap)
KLEE: WARNING: killing 10283 states (over memory cap)
KLEE: WARNING: killing 10437 states (over memory cap)
KLEE: WARNING: killing 10597 states (over memory cap)
KLEE: WARNING: killing 10334 states (over memory cap)
KLEE: WARNING: killing 10575 states (over memory cap)
KLEE: WARNING: killing 10219 states (over memory cap)
KLEE: WARNING: killing 10213 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10266 states (over memory cap)
KLEE: WARNING: killing 10088 states (over memory cap)
KLEE: WARNING: killing 9826 states (over memory cap)
KLEE: WARNING: killing 10142 states (over memory cap)
KLEE: WARNING: killing 10297 states (over memory cap)
KLEE: WARNING: killing 10286 states (over memory cap)
KLEE: WARNING: killing 10105 states (over memory cap)
KLEE: WARNING: killing 10341 states (over memory cap)
KLEE: WARNING: killing 10248 states (over memory cap)
KLEE: WARNING: killing 10486 states (over memory cap)
KLEE: WARNING: killing 10472 states (over memory cap)
KLEE: WARNING: killing 10209 states (over memory cap)
KLEE: WARNING: killing 9952 states (over memory cap)
KLEE: WARNING: killing 10103 states (over memory cap)
KLEE: WARNING: killing 10174 states (over memory cap)
KLEE: WARNING: killing 10321 states (over memory cap)
KLEE: WARNING: killing 10308 states (over memory cap)
KLEE: WARNING: killing 10540 states (over memory cap)
KLEE: WARNING: killing 10449 states (over memory cap)
KLEE: WARNING: killing 10524 states (over memory cap)
KLEE: WARNING: killing 10263 states (over memory cap)
KLEE: WARNING: killing 10338 states (over memory cap)
KLEE: WARNING: killing 9996 states (over memory cap)
KLEE: WARNING: killing 9981 states (over memory cap)
KLEE: WARNING: killing 10536 states (over memory cap)
KLEE: WARNING: killing 10120 states (over memory cap)
KLEE: WARNING: killing 10185 states (over memory cap)
KLEE: WARNING: killing 10173 states (over memory cap)
KLEE: WARNING: killing 10244 states (over memory cap)
KLEE: WARNING: killing 10393 states (over memory cap)
KLEE: WARNING: killing 10218 states (over memory cap)
KLEE: WARNING: killing 10447 states (over memory cap)
KLEE: WARNING: killing 10438 states (over memory cap)
KLEE: WARNING: killing 10346 states (over memory cap)
KLEE: WARNING: killing 10251 states (over memory cap)
KLEE: WARNING: killing 10161 states (over memory cap)
KLEE: WARNING: killing 10388 states (over memory cap)
KLEE: WARNING: killing 10372 states (over memory cap)
KLEE: WARNING: killing 10362 states (over memory cap)
KLEE: WARNING: killing 10274 states (over memory cap)
KLEE: WARNING: killing 10100 states (over memory cap)
KLEE: WARNING: killing 10409 states (over memory cap)
KLEE: WARNING: killing 10237 states (over memory cap)
KLEE: WARNING: killing 10465 states (over memory cap)
KLEE: WARNING: killing 10217 states (over memory cap)
KLEE: WARNING: killing 10441 states (over memory cap)
KLEE: WARNING: killing 10028 states (over memory cap)
KLEE: WARNING: killing 10018 states (over memory cap)
KLEE: WARNING: killing 10164 states (over memory cap)
KLEE: WARNING: killing 10153 states (over memory cap)
KLEE: WARNING: killing 10217 states (over memory cap)
KLEE: WARNING: killing 10758 states (over memory cap)
KLEE: WARNING: killing 10118 states (over memory cap)
KLEE: WARNING: killing 10102 states (over memory cap)
KLEE: WARNING: killing 10254 states (over memory cap)
KLEE: WARNING: killing 10238 states (over memory cap)
KLEE: WARNING: killing 10148 states (over memory cap)
KLEE: WARNING: killing 10611 states (over memory cap)
KLEE: WARNING: killing 10286 states (over memory cap)
KLEE: WARNING: killing 10350 states (over memory cap)
KLEE: WARNING: killing 9949 states (over memory cap)
KLEE: WARNING: killing 10168 states (over memory cap)
KLEE: WARNING: killing 10318 states (over memory cap)
KLEE: WARNING: killing 10382 states (over memory cap)
KLEE: WARNING: killing 10213 states (over memory cap)
KLEE: WARNING: killing 10358 states (over memory cap)
KLEE: WARNING: killing 10344 states (over memory cap)
KLEE: WARNING: killing 9868 states (over memory cap)
KLEE: WARNING: killing 10321 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 10219 states (over memory cap)
KLEE: WARNING: killing 10205 states (over memory cap)
KLEE: WARNING: killing 10352 states (over memory cap)
KLEE: WARNING: killing 10491 states (over memory cap)
KLEE: WARNING: killing 10171 states (over memory cap)
KLEE: WARNING: killing 10162 states (over memory cap)
KLEE: WARNING: killing 10533 states (over memory cap)
KLEE: WARNING: killing 10065 states (over memory cap)
KLEE: WARNING: killing 10132 states (over memory cap)
KLEE: WARNING: killing 10196 states (over memory cap)
KLEE: WARNING: killing 10264 states (over memory cap)
KLEE: WARNING: killing 10100 states (over memory cap)
KLEE: WARNING: killing 10470 states (over memory cap)
KLEE: WARNING: killing 10387 states (over memory cap)
KLEE: WARNING: killing 10148 states (over memory cap)
KLEE: WARNING: killing 10360 states (over memory cap)
KLEE: WARNING: killing 10042 states (over memory cap)
KLEE: WARNING: killing 10186 states (over memory cap)
KLEE: WARNING: killing 10180 states (over memory cap)
KLEE: WARNING: killing 10319 states (over memory cap)
KLEE: WARNING: killing 10153 states (over memory cap)
KLEE: WARNING: killing 10065 states (over memory cap)
