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-32_7a-drivers--staging--silicom--bpctl_mod.ko-ldv_main0_sequence_infinite_withcheck_stateful.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.: 399 337 4323 23662
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.935225009918
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 'ldv_handler_precall' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'iounmap' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Defining function unregister_netdevice_notifier as symbolic
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
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.969556093216
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 470 330 2507 14271
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
