bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-validator-v0.6/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point_false-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.: 299 235 2242 13633
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.513897180557
Defining function printk as symbolic
Removed calls to 'dev_set_drvdata' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function schedule_timeout_uninterruptible as symbolic
Defining function ipmi_unregister_smi as symbolic
Defining function mod_timer as symbolic
Defining function ipmi_alloc_smi_msg as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Defining function atomic_notifier_call_chain as symbolic
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'ipmi_smi_msg_received' (function is undefined)
Removed calls to 'ipmi_smi_watchdog_pretimeout' (function is undefined)
Defining function dev_warn as symbolic
Defining function kthread_stop as symbolic
Defining function del_timer_sync as symbolic
Defining function dev_get_drvdata as symbolic
Defining function _dev_info as symbolic
Defining function pci_enable_device as symbolic
Defining function dev_err as symbolic
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to '__release_region' (function is undefined)
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 'free_irq' (function is undefined)
Defining function request_threaded_irq as symbolic
Removed calls to 'iounmap' (function is undefined)
Defining function __request_region as symbolic
Defining function ioremap_nocache as symbolic
Defining function acpi_evaluate_integer as symbolic
Defining function pnp_get_resource as symbolic
Defining function acpi_install_gpe_handler as symbolic
Defining function acpi_remove_gpe_handler as symbolic
Defining function wake_up_process as symbolic
Removed calls to 'set_user_nice' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function kthread_create as symbolic
Defining function dev_notice as symbolic
Defining function schedule_timeout_interruptible as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'pnp_unregister_driver' (function is undefined)
Removed calls to 'driver_unregister' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function kstrdup as symbolic
Defining function simple_strtoul as symbolic
Removed calls to 'synchronize_sched' (function is undefined)
Defining function platform_device_alloc as symbolic
Defining function platform_device_add as symbolic
Defining function ipmi_register_smi as symbolic
Defining function ipmi_smi_add_proc_entry as symbolic
Defining function sprintf as symbolic
Defining function atomic_notifier_chain_register as symbolic
Defining function driver_register as symbolic
Defining function __pci_register_driver as symbolic
Defining function pnp_register_driver as symbolic
Defining function acpi_get_table as symbolic
Defining function dmi_find_device as symbolic
Defining function del_timer as symbolic
Linked our definitions to these undefined functions:
  strchr
  strcmp
  strcpy
  strlen
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.510763883591
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 343 195 1355 7729
INFO: Starting verification
KLEE: WARNING ONCE: function "cleanup_one_si" has inline asm
KLEE: WARNING ONCE: function "smi_event_handler" has inline asm
KLEE: WARNING ONCE: function "handle_flags" has inline asm
KLEE: WARNING ONCE: function "si_irq_handler" has inline asm
KLEE: WARNING ONCE: function "intf_mem_inb" has inline asm
KLEE: WARNING ONCE: function "intf_mem_outb" has inline asm
KLEE: WARNING ONCE: function "intf_mem_inw" has inline asm
KLEE: WARNING ONCE: function "intf_mem_outw" has inline asm
KLEE: WARNING ONCE: function "intf_mem_inl" has inline asm
KLEE: WARNING ONCE: function "intf_mem_outl" has inline asm
KLEE: WARNING ONCE: function "mem_inq" has inline asm
KLEE: WARNING ONCE: function "mem_outq" has inline asm
KLEE: WARNING ONCE: function "port_inb" has inline asm
KLEE: WARNING ONCE: function "port_outb" has inline asm
KLEE: WARNING ONCE: function "port_inw" has inline asm
KLEE: WARNING ONCE: function "port_outw" has inline asm
KLEE: WARNING ONCE: function "port_inl" has inline asm
KLEE: WARNING ONCE: function "port_outl" has inline asm
KLEE: WARNING ONCE: function "ipmi_acpi_gpe" has inline asm
KLEE: WARNING ONCE: function "smi_timeout" has inline asm
KLEE: WARNING ONCE: function "ipmi_thread" has inline asm
KLEE: WARNING ONCE: function "try_smi_init" 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_343dd8e9-648e-4f6e-af0e-68b3ed3c2307/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 13011 states (over memory cap)
KLEE: WARNING: killing 8583 states (over memory cap)
KLEE: WARNING: killing 9122 states (over memory cap)
KLEE: WARNING: killing 9330 states (over memory cap)
KLEE: WARNING: killing 9710 states (over memory cap)
KLEE: WARNING: killing 10572 states (over memory cap)
KLEE: WARNING: killing 10894 states (over memory cap)
KLEE: WARNING: killing 11161 states (over memory cap)
KLEE: WARNING: killing 12402 states (over memory cap)
KLEE: WARNING: killing 12178 states (over memory cap)
KLEE: WARNING: killing 12875 states (over memory cap)
KLEE: WARNING: killing 13189 states (over memory cap)
KLEE: WARNING: killing 13997 states (over memory cap)
KLEE: WARNING: killing 14426 states (over memory cap)
KLEE: WARNING: killing 13486 states (over memory cap)
KLEE: WARNING: killing 13687 states (over memory cap)
KLEE: WARNING: killing 13234 states (over memory cap)
KLEE: WARNING: killing 13270 states (over memory cap)
KLEE: WARNING: killing 14281 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-5DUyaU/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point_false-unreach-call.cil.out.c:7246: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14260 states (over memory cap)
KLEE: WARNING: killing 14731 states (over memory cap)
KLEE: WARNING: killing 14716 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-5DUyaU/linux-stable-90a4845-1-110_1a-drivers--char--ipmi--ipmi_si.ko-entry_point_false-unreach-call.cil.out.c:6197: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14961 states (over memory cap)
KLEE: WARNING: killing 14834 states (over memory cap)
KLEE: WARNING: killing 15467 states (over memory cap)
KLEE: WARNING: killing 14805 states (over memory cap)
KLEE: WARNING: killing 15216 states (over memory cap)
KLEE: WARNING: killing 14928 states (over memory cap)
KLEE: WARNING: killing 14850 states (over memory cap)
KLEE: WARNING: killing 15314 states (over memory cap)
KLEE: WARNING: killing 15236 states (over memory cap)
KLEE: WARNING: killing 14892 states (over memory cap)
KLEE: WARNING: killing 15243 states (over memory cap)
KLEE: WARNING: killing 15063 states (over memory cap)
KLEE: WARNING: killing 15414 states (over memory cap)
