bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 101 68 744 2855
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.257615089417
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'complete' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'ipmi_free_recv_msg' (function is undefined)
Removed calls to 'panic' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'kill_fasync' (function is undefined)
Removed calls to 'ipmi_get_version' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Defining function ipmi_smi_watcher_unregister as symbolic
Defining function unregister_die_notifier as symbolic
Defining function atomic_notifier_chain_unregister as symbolic
Defining function unregister_reboot_notifier as symbolic
Defining function misc_deregister as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Defining function ipmi_destroy_user as symbolic
Defining function printk as symbolic
Defining function ipmi_create_user as symbolic
Defining function misc_register as symbolic
Removed calls to 'wait_for_completion' (function is undefined)
Defining function ipmi_request_supply_msgs as symbolic
Removed calls to 'ipmi_poll_interface' (function is undefined)
Defining function fasync_helper as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Defining function default_wake_function as symbolic
Defining function register_die_notifier as symbolic
Defining function strim as symbolic
Defining function param_set_int as symbolic
Defining function simple_strtoul as symbolic
Defining function register_reboot_notifier as symbolic
Defining function atomic_notifier_chain_register as symbolic
Defining function ipmi_smi_watcher_register as symbolic
Defining function no_llseek as symbolic
Defining function ldv_undefined_int as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  strlen
  strncpy
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.188554048538
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 146 70 383 1710
INFO: Starting verification
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "set_timeout_free_smi" has inline asm
KLEE: WARNING ONCE: function "set_timeout_free_recv" has inline asm
KLEE: WARNING ONCE: function "heartbeat_free_smi" has inline asm
KLEE: WARNING ONCE: function "heartbeat_free_recv" has inline asm
KLEE: WARNING ONCE: function "ipmi_read" has inline asm
KLEE: WARNING ONCE: function "ipmi_close" has inline asm
KLEE: WARNING ONCE: function "ipmi_wdog_pretimeout_handler" has inline asm
KLEE: WARNING ONCE: function "ipmi_nmi" has inline asm
KLEE: WARNING ONCE: function "panic_halt_ipmi_set_timeout" has inline asm
KLEE: WARNING ONCE: function "ipmi_open" has inline asm
KLEE: WARNING ONCE: function "panic_smi_free" has inline asm
KLEE: WARNING ONCE: function "panic_recv_free" has inline asm
KLEE: WARNING ONCE: flushing 9608 bytes on read, may be slow and/or crash: MO14[9608] allocated at global:
KLEE: ERROR: /tmp/symbiotic-CFuukF/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i:3368: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-CFuukF/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i:3369: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
