bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--irda--via-ircc.ko-entry_point_true-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.: 121 151 1050 8519
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.332587957382
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'free_dma' (function is undefined)
Removed calls to 'irlap_close' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'irda_device_set_media_busy' (function is undefined)
Defining function printk as symbolic
Defining function capable as symbolic
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Removed calls to 'irda_setup_dma' (function is undefined)
Defining function net_ratelimit as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function request_dma as symbolic
Defining function sprintf as symbolic
Defining function irlap_open as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Defining function skb_put as symbolic
Defining function netif_rx as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_read_lock_held as symbolic
Removed calls to 'lock_release' (function is undefined)
Defining function rcu_is_watching as symbolic
Defining function async_wrap_skb as symbolic
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Defining function pci_enable_device as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'irda_init_max_qos_capabilies' (function is undefined)
Removed calls to 'irda_qos_bits_to_value' (function is undefined)
Defining function alloc_irdadev as symbolic
Defining function __request_region as symbolic
Defining function register_netdev as symbolic
Defining function pci_bus_write_config_byte as symbolic
Defining function pci_bus_read_config_byte as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_shutdown_4 as symbolic
Defining function ldv_ndo_init_3 as symbolic
Defining function ldv_ndo_uninit_3 as symbolic
Defining function ldv_ndo_init_2 as symbolic
Defining function ldv_ndo_uninit_2 as symbolic
Defining function __pci_register_driver as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.473429918289
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 129 104 671 7715
INFO: Starting verification
KLEE: WARNING ONCE: function "via_ircc_net_open" has inline asm
KLEE: WARNING ONCE: function "via_ircc_net_close" has inline asm
KLEE: WARNING ONCE: function "via_ircc_hard_xmit_fir" has inline asm
KLEE: WARNING ONCE: function "via_ircc_change_speed" has inline asm
KLEE: WARNING ONCE: function "CkRxRecv" has inline asm
KLEE: WARNING ONCE: function "via_ircc_change_dongle_speed" has inline asm
KLEE: WARNING ONCE: function "via_ircc_dma_receive" has inline asm
KLEE: WARNING ONCE: function "ClkTx" has inline asm
KLEE: WARNING ONCE: function "Wr_Indx" has inline asm
KLEE: WARNING ONCE: function "Wr_Byte" has inline asm
KLEE: WARNING ONCE: function "via_ircc_dma_xmit" has inline asm
KLEE: WARNING ONCE: function "via_ircc_interrupt" has inline asm
KLEE: WARNING ONCE: function "hwreset" has inline asm
KLEE: WARNING ONCE: function "irda_device_txqueue_empty" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "CommonInit" has inline asm
KLEE: WARNING ONCE: function "SetBaudRate" has inline asm
KLEE: WARNING ONCE: function "via_ircc_hard_xmit_sir" has inline asm
KLEE: WARNING ONCE: function "via_init_one" has inline asm
KLEE: WARNING ONCE: function "via_remove_one" has inline asm
KLEE: WARNING ONCE: function "via_ircc_open" 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_eb57facb-3f8d-49ab-b142-fd7b291e8310/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PqdEoB/linux-4.2-rc1.tar.xz-43_2a-drivers--net--irda--via-ircc.ko-entry_point_true-unreach-call.cil.out.c:6505: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16406 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 13946 states (over memory cap)
KLEE: WARNING: killing 13685 states (over memory cap)
KLEE: WARNING: killing 13938 states (over memory cap)
KLEE: WARNING: killing 13584 states (over memory cap)
KLEE: WARNING: killing 13431 states (over memory cap)
KLEE: WARNING: killing 14267 states (over memory cap)
KLEE: WARNING: killing 14125 states (over memory cap)
KLEE: WARNING: killing 14184 states (over memory cap)
KLEE: WARNING: killing 14231 states (over memory cap)
KLEE: WARNING: killing 14586 states (over memory cap)
KLEE: WARNING: killing 15027 states (over memory cap)
KLEE: WARNING: killing 15085 states (over memory cap)
KLEE: WARNING: killing 15141 states (over memory cap)
KLEE: WARNING: killing 14239 states (over memory cap)
KLEE: WARNING: killing 14772 states (over memory cap)
KLEE: WARNING: killing 14542 states (over memory cap)
KLEE: WARNING: killing 14691 states (over memory cap)
KLEE: WARNING: killing 14841 states (over memory cap)
KLEE: WARNING: killing 14323 states (over memory cap)
KLEE: WARNING: killing 14671 states (over memory cap)
KLEE: WARNING: killing 14531 states (over memory cap)
KLEE: WARNING: killing 14681 states (over memory cap)
KLEE: WARNING: killing 14363 states (over memory cap)
KLEE: WARNING: killing 14794 states (over memory cap)
KLEE: WARNING: killing 14661 states (over memory cap)
KLEE: WARNING: killing 14162 states (over memory cap)
KLEE: WARNING: killing 15334 states (over memory cap)
KLEE: WARNING: killing 14548 states (over memory cap)
KLEE: WARNING: killing 14325 states (over memory cap)
KLEE: WARNING: killing 14289 states (over memory cap)
KLEE: WARNING: killing 14806 states (over memory cap)
KLEE: WARNING: killing 15048 states (over memory cap)
KLEE: WARNING: killing 14550 states (over memory cap)
KLEE: WARNING: killing 14329 states (over memory cap)
KLEE: WARNING: killing 14753 states (over memory cap)
KLEE: WARNING: killing 14536 states (over memory cap)
KLEE: WARNING: killing 14967 states (over memory cap)
KLEE: WARNING: killing 14834 states (over memory cap)
KLEE: WARNING: killing 14988 states (over memory cap)
KLEE: WARNING: killing 14687 states (over memory cap)
KLEE: WARNING: killing 14473 states (over memory cap)
KLEE: WARNING: killing 14440 states (over memory cap)
KLEE: WARNING: killing 14497 states (over memory cap)
KLEE: WARNING: killing 14821 states (over memory cap)
KLEE: WARNING: killing 14351 states (over memory cap)
KLEE: WARNING: killing 14939 states (over memory cap)
KLEE: WARNING: killing 14376 states (over memory cap)
KLEE: WARNING: killing 14166 states (over memory cap)
KLEE: WARNING: killing 14575 states (over memory cap)
KLEE: WARNING: killing 14547 states (over memory cap)
KLEE: WARNING: killing 14778 states (over memory cap)
KLEE: WARNING: killing 14843 states (over memory cap)
KLEE: WARNING: killing 14547 states (over memory cap)
KLEE: WARNING: killing 14336 states (over memory cap)
KLEE: WARNING: killing 14388 states (over memory cap)
KLEE: WARNING: killing 14269 states (over memory cap)
KLEE: WARNING: killing 14855 states (over memory cap)
KLEE: WARNING: killing 14564 states (over memory cap)
KLEE: WARNING: killing 14708 states (over memory cap)
KLEE: WARNING: killing 14683 states (over memory cap)
KLEE: WARNING: killing 14570 states (over memory cap)
KLEE: WARNING: killing 14454 states (over memory cap)
KLEE: WARNING: killing 14513 states (over memory cap)
KLEE: WARNING: killing 14318 states (over memory cap)
KLEE: WARNING: killing 14458 states (over memory cap)
KLEE: WARNING: killing 14516 states (over memory cap)
KLEE: WARNING: killing 14583 states (over memory cap)
KLEE: WARNING: killing 14292 states (over memory cap)
KLEE: WARNING: killing 14439 states (over memory cap)
KLEE: WARNING: killing 14417 states (over memory cap)
KLEE: WARNING: killing 14220 states (over memory cap)
KLEE: WARNING: killing 14442 states (over memory cap)
KLEE: WARNING: killing 14835 states (over memory cap)
KLEE: WARNING: killing 14645 states (over memory cap)
KLEE: WARNING: killing 14359 states (over memory cap)
KLEE: WARNING: killing 14679 states (over memory cap)
KLEE: WARNING: killing 14568 states (over memory cap)
KLEE: WARNING: killing 14540 states (over memory cap)
KLEE: WARNING: killing 14599 states (over memory cap)
KLEE: WARNING: killing 14660 states (over memory cap)
KLEE: WARNING: killing 14377 states (over memory cap)
KLEE: WARNING: killing 14772 states (over memory cap)
KLEE: WARNING: killing 14168 states (over memory cap)
KLEE: WARNING: killing 14638 states (over memory cap)
KLEE: WARNING: killing 14532 states (over memory cap)
KLEE: WARNING: killing 14256 states (over memory cap)
KLEE: WARNING: killing 14474 states (over memory cap)
KLEE: WARNING: killing 8301 states (over memory cap)
KLEE: WARNING: killing 13535 states (over memory cap)
KLEE: WARNING: killing 14667 states (over memory cap)
KLEE: WARNING: killing 14303 states (over memory cap)
KLEE: WARNING: killing 14615 states (over memory cap)
KLEE: WARNING: killing 14419 states (over memory cap)
KLEE: WARNING: killing 8136 states (over memory cap)
KLEE: WARNING: killing 13891 states (over memory cap)
KLEE: WARNING: killing 14598 states (over memory cap)
KLEE: WARNING: killing 8104 states (over memory cap)
KLEE: WARNING: killing 14239 states (over memory cap)
KLEE: WARNING: killing 14377 states (over memory cap)
KLEE: WARNING: killing 14435 states (over memory cap)
KLEE: WARNING: killing 14326 states (over memory cap)
KLEE: WARNING: killing 14052 states (over memory cap)
KLEE: WARNING: killing 14680 states (over memory cap)
KLEE: WARNING: killing 14654 states (over memory cap)
KLEE: WARNING: killing 8078 states (over memory cap)
KLEE: WARNING: killing 13981 states (over memory cap)
KLEE: WARNING: killing 8137 states (over memory cap)
KLEE: WARNING: killing 13943 states (over memory cap)
KLEE: WARNING: killing 14396 states (over memory cap)
KLEE: WARNING: killing 7944 states (over memory cap)
KLEE: WARNING: killing 13961 states (over memory cap)
KLEE: WARNING: killing 14330 states (over memory cap)
KLEE: WARNING: killing 7985 states (over memory cap)
KLEE: WARNING: killing 13657 states (over memory cap)
KLEE: WARNING: killing 7962 states (over memory cap)
KLEE: WARNING: killing 14174 states (over memory cap)
KLEE: WARNING: killing 14469 states (over memory cap)
KLEE: WARNING: killing 14040 states (over memory cap)
KLEE: WARNING: killing 8221 states (over memory cap)
KLEE: WARNING: killing 13850 states (over memory cap)
KLEE: WARNING: killing 7972 states (over memory cap)
KLEE: WARNING: killing 14058 states (over memory cap)
KLEE: WARNING: killing 8106 states (over memory cap)
KLEE: WARNING: killing 13863 states (over memory cap)
KLEE: WARNING: killing 8087 states (over memory cap)
KLEE: WARNING: killing 13827 states (over memory cap)
KLEE: WARNING: killing 8067 states (over memory cap)
KLEE: WARNING: killing 14259 states (over memory cap)
KLEE: WARNING: killing 7973 states (over memory cap)
KLEE: WARNING: killing 13765 states (over memory cap)
KLEE: WARNING: killing 8261 states (over memory cap)
KLEE: WARNING: killing 14208 states (over memory cap)
KLEE: WARNING: killing 14024 states (over memory cap)
KLEE: WARNING: killing 7846 states (over memory cap)
KLEE: WARNING: killing 13601 states (over memory cap)
KLEE: WARNING: killing 7747 states (over memory cap)
KLEE: WARNING: killing 13871 states (over memory cap)
KLEE: WARNING: killing 7725 states (over memory cap)
KLEE: WARNING: killing 13754 states (over memory cap)
KLEE: WARNING: killing 8243 states (over memory cap)
KLEE: WARNING: killing 14116 states (over memory cap)
KLEE: WARNING: killing 7920 states (over memory cap)
KLEE: WARNING: killing 13856 states (over memory cap)
KLEE: WARNING: killing 8130 states (over memory cap)
KLEE: WARNING: killing 7669 states (over memory cap)
KLEE: WARNING: killing 13506 states (over memory cap)
KLEE: WARNING: killing 7722 states (over memory cap)
KLEE: WARNING: killing 13388 states (over memory cap)
KLEE: WARNING: killing 7852 states (over memory cap)
KLEE: WARNING: killing 13816 states (over memory cap)
KLEE: WARNING: killing 7913 states (over memory cap)
KLEE: WARNING: killing 13783 states (over memory cap)
KLEE: WARNING: killing 7889 states (over memory cap)
KLEE: WARNING: killing 13747 states (over memory cap)
