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--ali-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.: 163 131 1066 8214
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.313956975937
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'irlap_close' (function is undefined)
Removed calls to 'free_dma' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (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 'irda_setup_dma' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function ktime_get as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'async_unwrap_char' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function net_ratelimit as symbolic
Defining function request_dma as symbolic
Defining function sprintf as symbolic
Defining function irlap_open as symbolic
Defining function request_threaded_irq as symbolic
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 'ldv_initialize' (function is undefined)
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 'platform_driver_unregister' (function is undefined)
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)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_remove_4 as symbolic
Defining function ldv_shutdown_4 as symbolic
Defining function ldv_probe_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 alloc_irdadev as symbolic
Defining function __request_region as symbolic
Defining function register_netdev as symbolic
Defining function __platform_driver_register 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.35649394989
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 160 102 502 3793
INFO: Starting verification
KLEE: WARNING ONCE: function "ali_ircc_net_open" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_net_close" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_fir_hard_xmit" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_net_ioctl" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_change_speed" has inline asm
KLEE: WARNING ONCE: function "SetCOMInterrupts" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_change_dongle_speed" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_dma_receive" has inline asm
KLEE: WARNING ONCE: function "FIR2SIR" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_dma_xmit" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_interrupt" has inline asm
KLEE: WARNING ONCE: function "rcu_read_unlock" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_dma_receive_complete" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_sir_hard_xmit" has inline asm
KLEE: WARNING ONCE: function "ali_ircc_probe_53" has inline asm
KLEE: WARNING ONCE: function "main" 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_968ac132-ed42-4bbf-8964-a641effbed62/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-dA6J3S/linux-4.2-rc1.tar.xz-43_2a-drivers--net--irda--ali-ircc.ko-entry_point_true-unreach-call.cil.out.c:6404: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9409 states (over memory cap)
KLEE: WARNING: killing 6968 states (over memory cap)
KLEE: WARNING: killing 13005 states (over memory cap)
KLEE: WARNING: killing 13296 states (over memory cap)
KLEE: WARNING: killing 13385 states (over memory cap)
KLEE: WARNING: killing 6943 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 13110 states (over memory cap)
KLEE: WARNING: killing 7110 states (over memory cap)
KLEE: WARNING: killing 7033 states (over memory cap)
KLEE: WARNING: killing 7021 states (over memory cap)
KLEE: WARNING: killing 7009 states (over memory cap)
KLEE: WARNING: killing 6864 states (over memory cap)
KLEE: WARNING: killing 7662 states (over memory cap)
KLEE: WARNING: killing 6979 states (over memory cap)
KLEE: WARNING: killing 7375 states (over memory cap)
KLEE: WARNING: killing 7365 states (over memory cap)
KLEE: WARNING: killing 7090 states (over memory cap)
KLEE: WARNING: killing 7413 states (over memory cap)
KLEE: WARNING: killing 7473 states (over memory cap)
KLEE: WARNING: killing 7596 states (over memory cap)
KLEE: WARNING: killing 7389 states (over memory cap)
KLEE: WARNING: killing 7445 states (over memory cap)
KLEE: WARNING: killing 7504 states (over memory cap)
KLEE: WARNING: killing 7294 states (over memory cap)
KLEE: WARNING: killing 7616 states (over memory cap)
KLEE: WARNING: killing 7076 states (over memory cap)
KLEE: WARNING: killing 7330 states (over memory cap)
KLEE: WARNING: killing 7190 states (over memory cap)
KLEE: WARNING: killing 7312 states (over memory cap)
KLEE: WARNING: killing 6970 states (over memory cap)
KLEE: WARNING: killing 7028 states (over memory cap)
KLEE: WARNING: killing 7282 states (over memory cap)
KLEE: WARNING: killing 7670 states (over memory cap)
KLEE: WARNING: killing 7201 states (over memory cap)
KLEE: WARNING: killing 7387 states (over memory cap)
KLEE: WARNING: killing 7247 states (over memory cap)
KLEE: WARNING: killing 6912 states (over memory cap)
KLEE: WARNING: killing 7230 states (over memory cap)
KLEE: WARNING: killing 7549 states (over memory cap)
KLEE: WARNING: killing 7216 states (over memory cap)
KLEE: WARNING: killing 7595 states (over memory cap)
KLEE: WARNING: killing 7000 states (over memory cap)
KLEE: WARNING: killing 7317 states (over memory cap)
KLEE: WARNING: killing 7245 states (over memory cap)
KLEE: WARNING: killing 7300 states (over memory cap)
KLEE: WARNING: killing 7225 states (over memory cap)
KLEE: WARNING: killing 7415 states (over memory cap)
KLEE: WARNING: killing 6759 states (over memory cap)
KLEE: WARNING: killing 7137 states (over memory cap)
KLEE: WARNING: killing 7581 states (over memory cap)
KLEE: WARNING: killing 7444 states (over memory cap)
KLEE: WARNING: killing 7372 states (over memory cap)
KLEE: WARNING: killing 7431 states (over memory cap)
KLEE: WARNING: killing 7163 states (over memory cap)
KLEE: WARNING: killing 7286 states (over memory cap)
KLEE: WARNING: killing 7538 states (over memory cap)
KLEE: WARNING: killing 7593 states (over memory cap)
KLEE: WARNING: killing 7199 states (over memory cap)
KLEE: WARNING: killing 7318 states (over memory cap)
KLEE: WARNING: killing 7568 states (over memory cap)
KLEE: WARNING: killing 7435 states (over memory cap)
KLEE: WARNING: killing 7553 states (over memory cap)
KLEE: WARNING: killing 7165 states (over memory cap)
KLEE: WARNING: killing 6775 states (over memory cap)
KLEE: WARNING: killing 7338 states (over memory cap)
KLEE: WARNING: killing 7267 states (over memory cap)
KLEE: WARNING: killing 7259 states (over memory cap)
KLEE: WARNING: killing 7318 states (over memory cap)
KLEE: WARNING: killing 7371 states (over memory cap)
KLEE: WARNING: killing 7365 states (over memory cap)
KLEE: WARNING: killing 7229 states (over memory cap)
KLEE: WARNING: killing 7285 states (over memory cap)
KLEE: WARNING: killing 7215 states (over memory cap)
KLEE: WARNING: killing 7588 states (over memory cap)
KLEE: WARNING: killing 7326 states (over memory cap)
KLEE: WARNING: killing 7636 states (over memory cap)
KLEE: WARNING: killing 7378 states (over memory cap)
KLEE: WARNING: killing 7308 states (over memory cap)
KLEE: WARNING: killing 7049 states (over memory cap)
KLEE: WARNING: killing 7353 states (over memory cap)
KLEE: WARNING: killing 7223 states (over memory cap)
KLEE: WARNING: killing 7151 states (over memory cap)
KLEE: WARNING: killing 7021 states (over memory cap)
KLEE: WARNING: killing 6951 states (over memory cap)
KLEE: WARNING: killing 7314 states (over memory cap)
KLEE: WARNING: killing 6936 states (over memory cap)
KLEE: WARNING: killing 7302 states (over memory cap)
KLEE: WARNING: killing 7107 states (over memory cap)
KLEE: WARNING: killing 7285 states (over memory cap)
KLEE: WARNING: killing 7339 states (over memory cap)
KLEE: WARNING: killing 7211 states (over memory cap)
KLEE: WARNING: killing 7327 states (over memory cap)
KLEE: WARNING: killing 7319 states (over memory cap)
KLEE: WARNING: killing 7126 states (over memory cap)
KLEE: WARNING: killing 7557 states (over memory cap)
KLEE: WARNING: killing 7551 states (over memory cap)
KLEE: WARNING: killing 7358 states (over memory cap)
KLEE: WARNING: killing 7168 states (over memory cap)
KLEE: WARNING: killing 7345 states (over memory cap)
KLEE: WARNING: killing 7337 states (over memory cap)
KLEE: WARNING: killing 7209 states (over memory cap)
KLEE: WARNING: killing 7081 states (over memory cap)
KLEE: WARNING: killing 7443 states (over memory cap)
KLEE: WARNING: killing 7128 states (over memory cap)
KLEE: WARNING: killing 7118 states (over memory cap)
KLEE: WARNING: killing 7360 states (over memory cap)
KLEE: WARNING: killing 7232 states (over memory cap)
KLEE: WARNING: killing 7221 states (over memory cap)
KLEE: WARNING: killing 7154 states (over memory cap)
KLEE: WARNING: killing 7453 states (over memory cap)
KLEE: WARNING: killing 7204 states (over memory cap)
KLEE: WARNING: killing 7319 states (over memory cap)
KLEE: WARNING: killing 7190 states (over memory cap)
KLEE: WARNING: killing 6879 states (over memory cap)
KLEE: WARNING: killing 7234 states (over memory cap)
KLEE: WARNING: killing 7533 states (over memory cap)
KLEE: WARNING: killing 7283 states (over memory cap)
KLEE: WARNING: killing 7400 states (over memory cap)
KLEE: WARNING: killing 7572 states (over memory cap)
KLEE: WARNING: killing 7024 states (over memory cap)
KLEE: WARNING: killing 7380 states (over memory cap)
KLEE: WARNING: killing 7495 states (over memory cap)
KLEE: WARNING: killing 7250 states (over memory cap)
KLEE: WARNING: killing 7061 states (over memory cap)
KLEE: WARNING: killing 6993 states (over memory cap)
KLEE: WARNING: killing 7046 states (over memory cap)
KLEE: WARNING: killing 7101 states (over memory cap)
KLEE: WARNING: killing 7276 states (over memory cap)
KLEE: WARNING: killing 7328 states (over memory cap)
KLEE: WARNING: killing 7262 states (over memory cap)
KLEE: WARNING: killing 7558 states (over memory cap)
KLEE: WARNING: killing 7309 states (over memory cap)
KLEE: WARNING: killing 7063 states (over memory cap)
KLEE: WARNING: killing 7117 states (over memory cap)
KLEE: WARNING: killing 6989 states (over memory cap)
KLEE: WARNING: killing 7041 states (over memory cap)
KLEE: WARNING: killing 7515 states (over memory cap)
KLEE: WARNING: killing 7212 states (over memory cap)
KLEE: WARNING: killing 7681 states (over memory cap)
KLEE: WARNING: killing 7317 states (over memory cap)
KLEE: WARNING: killing 7192 states (over memory cap)
KLEE: WARNING: killing 7128 states (over memory cap)
KLEE: WARNING: killing 7538 states (over memory cap)
KLEE: WARNING: killing 7470 states (over memory cap)
KLEE: WARNING: killing 7345 states (over memory cap)
KLEE: WARNING: killing 7282 states (over memory cap)
KLEE: WARNING: killing 6861 states (over memory cap)
KLEE: WARNING: killing 7030 states (over memory cap)
KLEE: WARNING: killing 7022 states (over memory cap)
KLEE: WARNING: killing 7135 states (over memory cap)
KLEE: WARNING: killing 7422 states (over memory cap)
KLEE: WARNING: killing 7474 states (over memory cap)
KLEE: WARNING: killing 7175 states (over memory cap)
KLEE: WARNING: killing 7227 states (over memory cap)
KLEE: WARNING: killing 7222 states (over memory cap)
KLEE: WARNING: killing 7271 states (over memory cap)
KLEE: WARNING: killing 7090 states (over memory cap)
KLEE: WARNING: killing 7316 states (over memory cap)
KLEE: WARNING: killing 7193 states (over memory cap)
KLEE: WARNING: killing 7073 states (over memory cap)
KLEE: WARNING: killing 7472 states (over memory cap)
KLEE: WARNING: killing 7116 states (over memory cap)
KLEE: WARNING: killing 7286 states (over memory cap)
KLEE: WARNING: killing 7337 states (over memory cap)
KLEE: WARNING: killing 7276 states (over memory cap)
KLEE: WARNING: killing 7035 states (over memory cap)
KLEE: WARNING: killing 7030 states (over memory cap)
KLEE: WARNING: killing 7491 states (over memory cap)
KLEE: WARNING: killing 7249 states (over memory cap)
KLEE: WARNING: killing 7014 states (over memory cap)
KLEE: WARNING: killing 7122 states (over memory cap)
KLEE: WARNING: killing 7290 states (over memory cap)
KLEE: WARNING: killing 7282 states (over memory cap)
KLEE: WARNING: killing 7104 states (over memory cap)
KLEE: WARNING: killing 7152 states (over memory cap)
KLEE: WARNING: killing 7434 states (over memory cap)
KLEE: WARNING: killing 7257 states (over memory cap)
KLEE: WARNING: killing 7309 states (over memory cap)
KLEE: WARNING: killing 6953 states (over memory cap)
KLEE: WARNING: killing 7466 states (over memory cap)
KLEE: WARNING: killing 7632 states (over memory cap)
KLEE: WARNING: killing 7459 states (over memory cap)
KLEE: WARNING: killing 7049 states (over memory cap)
KLEE: WARNING: killing 7156 states (over memory cap)
KLEE: WARNING: killing 7380 states (over memory cap)
KLEE: WARNING: killing 7261 states (over memory cap)
KLEE: WARNING: killing 7430 states (over memory cap)
KLEE: WARNING: killing 7478 states (over memory cap)
KLEE: WARNING: killing 7073 states (over memory cap)
KLEE: WARNING: killing 6839 states (over memory cap)
KLEE: WARNING: killing 7116 states (over memory cap)
KLEE: WARNING: killing 7166 states (over memory cap)
KLEE: WARNING: killing 7328 states (over memory cap)
KLEE: WARNING: killing 7098 states (over memory cap)
KLEE: WARNING: killing 7374 states (over memory cap)
KLEE: WARNING: killing 7426 states (over memory cap)
KLEE: WARNING: killing 7366 states (over memory cap)
KLEE: WARNING: killing 7417 states (over memory cap)
KLEE: WARNING: killing 7241 states (over memory cap)
KLEE: WARNING: killing 7631 states (over memory cap)
KLEE: WARNING: killing 7284 states (over memory cap)
KLEE: WARNING: killing 7222 states (over memory cap)
KLEE: WARNING: killing 7160 states (over memory cap)
KLEE: WARNING: killing 7435 states (over memory cap)
KLEE: WARNING: killing 7374 states (over memory cap)
KLEE: WARNING: killing 7480 states (over memory cap)
KLEE: WARNING: killing 7082 states (over memory cap)
KLEE: WARNING: killing 7187 states (over memory cap)
KLEE: WARNING: killing 7406 states (over memory cap)
KLEE: WARNING: killing 7065 states (over memory cap)
KLEE: WARNING: killing 7170 states (over memory cap)
KLEE: WARNING: killing 6996 states (over memory cap)
KLEE: WARNING: killing 7045 states (over memory cap)
KLEE: WARNING: killing 7431 states (over memory cap)
KLEE: WARNING: killing 7426 states (over memory cap)
KLEE: WARNING: killing 7810 states (over memory cap)
KLEE: WARNING: killing 6911 states (over memory cap)
KLEE: WARNING: killing 7129 states (over memory cap)
KLEE: WARNING: killing 7406 states (over memory cap)
KLEE: WARNING: killing 7010 states (over memory cap)
KLEE: WARNING: killing 7117 states (over memory cap)
KLEE: WARNING: killing 7166 states (over memory cap)
KLEE: WARNING: killing 7492 states (over memory cap)
KLEE: WARNING: killing 7040 states (over memory cap)
KLEE: WARNING: killing 7090 states (over memory cap)
KLEE: WARNING: killing 7141 states (over memory cap)
KLEE: WARNING: killing 7138 states (over memory cap)
KLEE: WARNING: killing 7132 states (over memory cap)
KLEE: WARNING: killing 7401 states (over memory cap)
KLEE: WARNING: killing 7176 states (over memory cap)
KLEE: WARNING: killing 7225 states (over memory cap)
KLEE: WARNING: killing 7330 states (over memory cap)
KLEE: WARNING: killing 7106 states (over memory cap)
KLEE: WARNING: killing 7046 states (over memory cap)
KLEE: WARNING: killing 7481 states (over memory cap)
KLEE: WARNING: killing 7258 states (over memory cap)
KLEE: WARNING: killing 7144 states (over memory cap)
KLEE: WARNING: killing 7247 states (over memory cap)
KLEE: WARNING: killing 7405 states (over memory cap)
KLEE: WARNING: killing 7180 states (over memory cap)
KLEE: WARNING: killing 7229 states (over memory cap)
KLEE: WARNING: killing 7445 states (over memory cap)
KLEE: WARNING: killing 7059 states (over memory cap)
KLEE: WARNING: killing 6889 states (over memory cap)
KLEE: WARNING: killing 7266 states (over memory cap)
KLEE: WARNING: killing 6878 states (over memory cap)
