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--staging--silicom--bpctl_mod.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.: 411 340 4361 23778
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
INFO: Compilation, preparation and instrumentation time: 0.901561975479
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to 'up' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Defining function printk as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function sprintf as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function mod_timer as symbolic
Defining function del_timer_sync as symbolic
Defining function _copy_from_user as symbolic
Defining function kstrtoint_from_user as symbolic
Defining function create_proc_entry as symbolic
Defining function proc_mkdir as symbolic
Defining function down_interruptible as symbolic
Defining function _raw_spin_trylock as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function pci_get_subsys as symbolic
Defining function register_netdevice_notifier as symbolic
Defining function ioremap_nocache as symbolic
Defining function __register_chrdev as symbolic
Defining function unregister_netdevice_notifier as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.891242027283
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 478 331 2512 14314
INFO: Starting verification
KLEE: WARNING ONCE: function "device_ioctl" has inline asm
KLEE: WARNING ONCE: function "bypass_status" has inline asm
KLEE: WARNING ONCE: function "disc_off_status" has inline asm
KLEE: WARNING ONCE: function "read_reg" has inline asm
KLEE: WARNING ONCE: function "write_pulse" has inline asm
KLEE: WARNING ONCE: function "bypass_from_last_read" has inline asm
KLEE: WARNING ONCE: function "send_bypass_clear_pulse" has inline asm
KLEE: WARNING ONCE: function "set_tx" has inline asm
KLEE: WARNING ONCE: function "tpl_hw_off" has inline asm
KLEE: WARNING ONCE: function "tpl_hw_on" has inline asm
KLEE: WARNING ONCE: function "write_reg" has inline asm
KLEE: WARNING ONCE: function "data_pulse" has inline asm
KLEE: WARNING ONCE: function "write_data_port_int" has inline asm
KLEE: WARNING ONCE: function "bp75_acquire_phy" has inline asm
KLEE: WARNING ONCE: function "bp75_write_phy_reg_mdic" has inline asm
KLEE: WARNING ONCE: function "bp75_release_phy" has inline asm
KLEE: WARNING ONCE: function "bp75_get_hw_semaphore_generic" has inline asm
KLEE: WARNING ONCE: function "bp75_read_phy_reg_mdic" has inline asm
KLEE: WARNING ONCE: function "tap_status" has inline asm
KLEE: WARNING ONCE: function "wdt_timer_reload" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "set_bp_force_link_fn" has inline asm
KLEE: WARNING ONCE: function "get_bp_force_link_fn" has inline asm
KLEE: WARNING ONCE: function "tx_status" has inline asm
KLEE: WARNING ONCE: function "bp75_put_hw_semaphore_generic" has inline asm
KLEE: WARNING ONCE: function "tpl_hw_status" has inline asm
KLEE: WARNING ONCE: function "bypass_caps_init" has inline asm
KLEE: WARNING ONCE: function "bp_tpl_timer_fn" has inline asm
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 10600 states (over memory cap)
KLEE: WARNING: killing 11059 states (over memory cap)
KLEE: WARNING: killing 10930 states (over memory cap)
KLEE: WARNING: killing 10883 states (over memory cap)
KLEE: WARNING: killing 11176 states (over memory cap)
KLEE: WARNING: killing 11464 states (over memory cap)
KLEE: WARNING: killing 11346 states (over memory cap)
KLEE: WARNING: killing 11636 states (over memory cap)
KLEE: WARNING: killing 11603 states (over memory cap)
KLEE: WARNING: killing 11975 states (over memory cap)
KLEE: WARNING: killing 12594 states (over memory cap)
KLEE: WARNING: killing 12472 states (over memory cap)
KLEE: WARNING: killing 13087 states (over memory cap)
KLEE: WARNING: killing 12812 states (over memory cap)
KLEE: WARNING: killing 12773 states (over memory cap)
KLEE: WARNING: killing 13222 states (over memory cap)
KLEE: WARNING: killing 13180 states (over memory cap)
KLEE: WARNING: killing 13217 states (over memory cap)
KLEE: WARNING: killing 13101 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 13260 states (over memory cap)
KLEE: WARNING: killing 13373 states (over memory cap)
KLEE: WARNING: killing 13415 states (over memory cap)
KLEE: WARNING: killing 13688 states (over memory cap)
KLEE: WARNING: killing 13573 states (over memory cap)
KLEE: WARNING: killing 13766 states (over memory cap)
KLEE: WARNING: killing 13652 states (over memory cap)
KLEE: WARNING: killing 13612 states (over memory cap)
KLEE: WARNING: killing 14124 states (over memory cap)
KLEE: WARNING: killing 13929 states (over memory cap)
KLEE: WARNING: killing 13968 states (over memory cap)
KLEE: WARNING: killing 14005 states (over memory cap)
KLEE: WARNING: killing 13966 states (over memory cap)
KLEE: WARNING: killing 7745 states (over memory cap)
KLEE: WARNING: killing 13527 states (over memory cap)
KLEE: WARNING: killing 13948 states (over memory cap)
KLEE: WARNING: killing 13759 states (over memory cap)
KLEE: WARNING: killing 14177 states (over memory cap)
KLEE: WARNING: killing 7732 states (over memory cap)
KLEE: WARNING: killing 13595 states (over memory cap)
KLEE: WARNING: killing 7624 states (over memory cap)
KLEE: WARNING: killing 13772 states (over memory cap)
KLEE: WARNING: killing 7517 states (over memory cap)
KLEE: WARNING: killing 13492 states (over memory cap)
KLEE: WARNING: killing 7714 states (over memory cap)
KLEE: WARNING: killing 13590 states (over memory cap)
KLEE: WARNING: killing 7534 states (over memory cap)
KLEE: WARNING: killing 13537 states (over memory cap)
KLEE: WARNING: killing 7948 states (over memory cap)
KLEE: WARNING: killing 13634 states (over memory cap)
KLEE: WARNING: killing 7699 states (over memory cap)
KLEE: WARNING: killing 13289 states (over memory cap)
KLEE: WARNING: killing 7667 states (over memory cap)
KLEE: WARNING: killing 13684 states (over memory cap)
KLEE: WARNING: killing 7860 states (over memory cap)
KLEE: WARNING: killing 13936 states (over memory cap)
KLEE: WARNING: killing 7691 states (over memory cap)
KLEE: WARNING: killing 7316 states (over memory cap)
KLEE: WARNING: killing 13354 states (over memory cap)
KLEE: WARNING: killing 7578 states (over memory cap)
KLEE: WARNING: killing 13380 states (over memory cap)
KLEE: WARNING: killing 7695 states (over memory cap)
KLEE: WARNING: killing 13553 states (over memory cap)
KLEE: WARNING: killing 7667 states (over memory cap)
KLEE: WARNING: killing 7298 states (over memory cap)
KLEE: WARNING: killing 7360 states (over memory cap)
KLEE: WARNING: killing 13400 states (over memory cap)
KLEE: WARNING: killing 7696 states (over memory cap)
KLEE: WARNING: killing 7258 states (over memory cap)
KLEE: WARNING: killing 13417 states (over memory cap)
KLEE: WARNING: killing 7802 states (over memory cap)
KLEE: WARNING: killing 7223 states (over memory cap)
KLEE: WARNING: killing 13364 states (over memory cap)
KLEE: WARNING: killing 7842 states (over memory cap)
KLEE: WARNING: killing 7266 states (over memory cap)
KLEE: WARNING: killing 7258 states (over memory cap)
KLEE: WARNING: killing 13433 states (over memory cap)
KLEE: WARNING: killing 7732 states (over memory cap)
KLEE: WARNING: killing 7368 states (over memory cap)
KLEE: WARNING: killing 7074 states (over memory cap)
KLEE: WARNING: killing 7066 states (over memory cap)
KLEE: WARNING: killing 7059 states (over memory cap)
KLEE: WARNING: killing 7048 states (over memory cap)
KLEE: WARNING: killing 7042 states (over memory cap)
KLEE: WARNING: killing 13161 states (over memory cap)
KLEE: WARNING: killing 7651 states (over memory cap)
KLEE: WARNING: killing 7221 states (over memory cap)
KLEE: WARNING: killing 7356 states (over memory cap)
KLEE: WARNING: killing 7209 states (over memory cap)
KLEE: WARNING: killing 7132 states (over memory cap)
KLEE: WARNING: killing 6983 states (over memory cap)
KLEE: WARNING: killing 7257 states (over memory cap)
KLEE: WARNING: killing 7387 states (over memory cap)
KLEE: WARNING: killing 7172 states (over memory cap)
KLEE: WARNING: killing 7025 states (over memory cap)
KLEE: WARNING: killing 7156 states (over memory cap)
KLEE: WARNING: killing 7081 states (over memory cap)
KLEE: WARNING: killing 7007 states (over memory cap)
KLEE: WARNING: killing 7205 states (over memory cap)
KLEE: WARNING: killing 6991 states (over memory cap)
KLEE: WARNING: killing 7261 states (over memory cap)
KLEE: WARNING: killing 7045 states (over memory cap)
KLEE: WARNING: killing 7036 states (over memory cap)
KLEE: WARNING: killing 7170 states (over memory cap)
KLEE: WARNING: killing 7021 states (over memory cap)
KLEE: WARNING: killing 6946 states (over memory cap)
KLEE: WARNING: killing 7215 states (over memory cap)
KLEE: WARNING: killing 6929 states (over memory cap)
KLEE: WARNING: killing 7059 states (over memory cap)
KLEE: WARNING: killing 7257 states (over memory cap)
KLEE: WARNING: killing 7182 states (over memory cap)
KLEE: WARNING: killing 7106 states (over memory cap)
KLEE: WARNING: killing 7170 states (over memory cap)
KLEE: WARNING: killing 7161 states (over memory cap)
KLEE: WARNING: killing 7018 states (over memory cap)
KLEE: WARNING: killing 7012 states (over memory cap)
KLEE: WARNING: killing 7208 states (over memory cap)
KLEE: WARNING: killing 7203 states (over memory cap)
KLEE: WARNING: killing 7056 states (over memory cap)
KLEE: WARNING: killing 7119 states (over memory cap)
KLEE: WARNING: killing 7042 states (over memory cap)
KLEE: WARNING: killing 7033 states (over memory cap)
KLEE: WARNING: killing 7029 states (over memory cap)
KLEE: WARNING: killing 7019 states (over memory cap)
KLEE: WARNING: killing 6808 states (over memory cap)
KLEE: WARNING: killing 6935 states (over memory cap)
KLEE: WARNING: killing 7198 states (over memory cap)
KLEE: WARNING: killing 7127 states (over memory cap)
KLEE: WARNING: killing 7321 states (over memory cap)
KLEE: WARNING: killing 7179 states (over memory cap)
KLEE: WARNING: killing 7108 states (over memory cap)
KLEE: WARNING: killing 6899 states (over memory cap)
KLEE: WARNING: killing 6957 states (over memory cap)
KLEE: WARNING: killing 7014 states (over memory cap)
KLEE: WARNING: killing 6943 states (over memory cap)
KLEE: WARNING: killing 7269 states (over memory cap)
KLEE: WARNING: killing 7063 states (over memory cap)
KLEE: WARNING: killing 7056 states (over memory cap)
KLEE: WARNING: killing 7050 states (over memory cap)
KLEE: WARNING: killing 6976 states (over memory cap)
KLEE: WARNING: killing 7033 states (over memory cap)
KLEE: WARNING: killing 6959 states (over memory cap)
KLEE: WARNING: killing 7087 states (over memory cap)
KLEE: WARNING: killing 7013 states (over memory cap)
KLEE: WARNING: killing 7205 states (over memory cap)
KLEE: WARNING: killing 7268 states (over memory cap)
KLEE: WARNING: killing 6994 states (over memory cap)
