bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-challenges/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-broadcom-b44_true-unreach-call.cil.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.: 143 408 2122 13933
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.530790090561
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function netdev_info as symbolic
Removed calls to 'ssb_driver_unregister' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __ssb_driver_register as symbolic
Defining function ssb_pcihost_register as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function strlcpy as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function ethtool_op_get_link as symbolic
Defining function phy_ethtool_gset as symbolic
Removed calls to 'dql_reset' (function is undefined)
Removed calls to 'ssb_device_enable' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function net_ratelimit as symbolic
Defining function netdev_err as symbolic
Defining function ssb_device_is_enabled as symbolic
Defining function ssb_pcicore_dev_irqvecs_enable as symbolic
Defining function ssb_clockspeed as symbolic
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function __alloc_skb as symbolic
Defining function __phys_addr as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function phy_mii_ioctl as symbolic
Defining function generic_mii_ioctl as symbolic
Removed calls to 'phy_print_status' (function is undefined)
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function skb_put as symbolic
Defining function printk as symbolic
Defining function netpoll_trap as symbolic
Defining function eth_validate_addr as symbolic
Defining function phy_ethtool_sset as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'mdiobus_unregister' (function is undefined)
Removed calls to 'mdiobus_free' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'phy_disconnect' (function is undefined)
Removed calls to 'ssb_device_disable' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Defining function ssb_bus_powerup as symbolic
Defining function dev_err as symbolic
Defining function mod_timer as symbolic
Defining function request_threaded_irq as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Defining function pci_set_power_state as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function del_timer_sync as symbolic
Defining function ssb_bus_may_powerdown as symbolic
Removed calls to 'phy_stop' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to 'dql_completed' (function is undefined)
Removed calls to 'napi_complete' (function is undefined)
Defining function snprintf as symbolic
Defining function mdiobus_register as symbolic
Defining function _dev_info as symbolic
Defining function phy_connect as symbolic
Defining function mdiobus_alloc_size as symbolic
Defining function register_netdev as symbolic
Defining function ldv_pre_register_netdev as symbolic
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'phy_start' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Defining function round_jiffies as symbolic
Defining function netdev_warn as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Defining function ssb_dma_translation as symbolic
Defining function dma_set_mask as symbolic
Defining function dma_supported as symbolic
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Defining function skb_pull as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_receive_skb as symbolic
Defining function alloc_etherdev_mqs as symbolic
Removed calls to 'disable_irq' (function is undefined)
Removed calls to 'enable_irq' (function is undefined)
Defining function external_allocated_data as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __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.543277025223
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 219 331 1118 7686
INFO: Starting verification
KLEE: WARNING ONCE: function "b44_get_settings" has inline asm
KLEE: WARNING ONCE: function "b44_init_hw" has inline asm
KLEE: WARNING ONCE: function "dma_sync_single_for_device" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "b44_ioctl" has inline asm
KLEE: WARNING ONCE: function "b44_adjust_link" has inline asm
KLEE: WARNING ONCE: function "b44_start_xmit" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "b44_tx_timeout" has inline asm
KLEE: WARNING ONCE: function "b44_set_ringparam" has inline asm
KLEE: WARNING ONCE: function "b44_set_settings" has inline asm
KLEE: WARNING ONCE: function "b44_resume" has inline asm
KLEE: WARNING ONCE: function "b44_magic_pattern" has inline asm
KLEE: WARNING ONCE: function "b44_close" has inline asm
KLEE: WARNING ONCE: function "dma_free_attrs" has inline asm
KLEE: WARNING ONCE: function "b44_open" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_e90660ee-8cbb-467f-a5c9-22473979e673/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-5Eb35k/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-ethernet-broadcom-b44_true-unreach-call.cil.c:11052: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15983 states (over memory cap)
KLEE: WARNING: killing 13965 states (over memory cap)
KLEE: WARNING: killing 13429 states (over memory cap)
KLEE: WARNING: killing 13380 states (over memory cap)
KLEE: WARNING: killing 13333 states (over memory cap)
KLEE: WARNING: killing 12803 states (over memory cap)
KLEE: WARNING: killing 12527 states (over memory cap)
KLEE: WARNING: killing 13202 states (over memory cap)
KLEE: WARNING: killing 13160 states (over memory cap)
KLEE: WARNING: killing 12884 states (over memory cap)
KLEE: WARNING: killing 13083 states (over memory cap)
KLEE: WARNING: killing 13398 states (over memory cap)
KLEE: WARNING: killing 13598 states (over memory cap)
KLEE: WARNING: killing 14032 states (over memory cap)
KLEE: WARNING: killing 13994 states (over memory cap)
KLEE: WARNING: killing 14080 states (over memory cap)
KLEE: WARNING: killing 14632 states (over memory cap)
KLEE: WARNING: killing 13665 states (over memory cap)
KLEE: WARNING: killing 14333 states (over memory cap)
KLEE: WARNING: killing 13952 states (over memory cap)
KLEE: WARNING: killing 14267 states (over memory cap)
KLEE: WARNING: killing 13885 states (over memory cap)
KLEE: WARNING: killing 13387 states (over memory cap)
KLEE: WARNING: killing 13474 states (over memory cap)
KLEE: WARNING: killing 13443 states (over memory cap)
KLEE: WARNING: killing 13761 states (over memory cap)
KLEE: WARNING: killing 13395 states (over memory cap)
KLEE: WARNING: killing 13585 states (over memory cap)
KLEE: WARNING: killing 13331 states (over memory cap)
KLEE: WARNING: killing 13186 states (over memory cap)
KLEE: WARNING: killing 13381 states (over memory cap)
KLEE: WARNING: killing 13580 states (over memory cap)
KLEE: WARNING: killing 13213 states (over memory cap)
KLEE: WARNING: killing 12732 states (over memory cap)
KLEE: WARNING: killing 13489 states (over memory cap)
KLEE: WARNING: killing 13238 states (over memory cap)
KLEE: WARNING: killing 13765 states (over memory cap)
KLEE: WARNING: killing 13521 states (over memory cap)
KLEE: WARNING: killing 13269 states (over memory cap)
KLEE: WARNING: killing 13244 states (over memory cap)
KLEE: WARNING: killing 13439 states (over memory cap)
KLEE: WARNING: killing 13629 states (over memory cap)
KLEE: WARNING: killing 12939 states (over memory cap)
KLEE: WARNING: killing 13135 states (over memory cap)
KLEE: WARNING: killing 13547 states (over memory cap)
KLEE: WARNING: killing 13629 states (over memory cap)
KLEE: WARNING: killing 13494 states (over memory cap)
KLEE: WARNING: killing 13470 states (over memory cap)
KLEE: WARNING: killing 13227 states (over memory cap)
KLEE: WARNING: killing 13316 states (over memory cap)
KLEE: WARNING: killing 13726 states (over memory cap)
KLEE: WARNING: killing 13372 states (over memory cap)
KLEE: WARNING: killing 13676 states (over memory cap)
KLEE: WARNING: killing 13208 states (over memory cap)
KLEE: WARNING: killing 13613 states (over memory cap)
KLEE: WARNING: killing 13588 states (over memory cap)
KLEE: WARNING: killing 13346 states (over memory cap)
KLEE: WARNING: killing 13214 states (over memory cap)
KLEE: WARNING: killing 13187 states (over memory cap)
KLEE: WARNING: killing 13372 states (over memory cap)
KLEE: WARNING: killing 13031 states (over memory cap)
KLEE: WARNING: killing 13436 states (over memory cap)
KLEE: WARNING: killing 13523 states (over memory cap)
KLEE: WARNING: killing 13381 states (over memory cap)
KLEE: WARNING: killing 13249 states (over memory cap)
KLEE: WARNING: killing 13655 states (over memory cap)
KLEE: WARNING: killing 13628 states (over memory cap)
KLEE: WARNING: killing 13079 states (over memory cap)
KLEE: WARNING: killing 13161 states (over memory cap)
KLEE: WARNING: killing 13347 states (over memory cap)
KLEE: WARNING: killing 13529 states (over memory cap)
KLEE: WARNING: killing 13609 states (over memory cap)
KLEE: WARNING: killing 13583 states (over memory cap)
KLEE: WARNING: killing 12933 states (over memory cap)
KLEE: WARNING: killing 13434 states (over memory cap)
KLEE: WARNING: killing 13204 states (over memory cap)
KLEE: WARNING: killing 13597 states (over memory cap)
KLEE: WARNING: killing 13361 states (over memory cap)
KLEE: WARNING: killing 13554 states (over memory cap)
KLEE: WARNING: killing 13627 states (over memory cap)
KLEE: WARNING: killing 13395 states (over memory cap)
KLEE: WARNING: killing 13269 states (over memory cap)
KLEE: WARNING: killing 13346 states (over memory cap)
KLEE: WARNING: killing 13015 states (over memory cap)
KLEE: WARNING: killing 13406 states (over memory cap)
KLEE: WARNING: killing 13585 states (over memory cap)
KLEE: WARNING: killing 13662 states (over memory cap)
KLEE: WARNING: killing 13538 states (over memory cap)
KLEE: WARNING: killing 13415 states (over memory cap)
KLEE: WARNING: killing 13489 states (over memory cap)
KLEE: WARNING: killing 13160 states (over memory cap)
KLEE: WARNING: killing 13440 states (over memory cap)
KLEE: WARNING: killing 13011 states (over memory cap)
KLEE: WARNING: killing 13598 states (over memory cap)
KLEE: WARNING: killing 13774 states (over memory cap)
KLEE: WARNING: killing 13449 states (over memory cap)
KLEE: WARNING: killing 13424 states (over memory cap)
KLEE: WARNING: killing 13506 states (over memory cap)
KLEE: WARNING: killing 13485 states (over memory cap)
KLEE: WARNING: killing 12764 states (over memory cap)
KLEE: WARNING: killing 13032 states (over memory cap)
KLEE: WARNING: killing 13117 states (over memory cap)
KLEE: WARNING: killing 13590 states (over memory cap)
KLEE: WARNING: killing 13472 states (over memory cap)
KLEE: WARNING: killing 13341 states (over memory cap)
KLEE: WARNING: killing 13425 states (over memory cap)
KLEE: WARNING: killing 13803 states (over memory cap)
KLEE: WARNING: killing 13478 states (over memory cap)
KLEE: WARNING: killing 13562 states (over memory cap)
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: WARNING: killing 13417 states (over memory cap)
KLEE: WARNING: killing 13489 states (over memory cap)
KLEE: WARNING: killing 13078 states (over memory cap)
KLEE: WARNING: killing 13153 states (over memory cap)
KLEE: WARNING: killing 13524 states (over memory cap)
KLEE: WARNING: killing 13303 states (over memory cap)
KLEE: WARNING: killing 13085 states (over memory cap)
KLEE: WARNING: killing 13446 states (over memory cap)
KLEE: WARNING: killing 13621 states (over memory cap)
KLEE: WARNING: killing 13502 states (over memory cap)
KLEE: WARNING: killing 13382 states (over memory cap)
KLEE: WARNING: killing 13750 states (over memory cap)
KLEE: WARNING: killing 13432 states (over memory cap)
KLEE: WARNING: killing 13024 states (over memory cap)
KLEE: WARNING: killing 13194 states (over memory cap)
KLEE: WARNING: killing 13176 states (over memory cap)
KLEE: WARNING: killing 13055 states (over memory cap)
KLEE: WARNING: killing 13511 states (over memory cap)
KLEE: WARNING: killing 13401 states (over memory cap)
KLEE: WARNING: killing 13762 states (over memory cap)
KLEE: WARNING: killing 13447 states (over memory cap)
KLEE: WARNING: killing 13709 states (over memory cap)
KLEE: WARNING: killing 13305 states (over memory cap)
KLEE: WARNING: killing 13479 states (over memory cap)
KLEE: WARNING: killing 13740 states (over memory cap)
KLEE: WARNING: killing 13534 states (over memory cap)
KLEE: WARNING: killing 13134 states (over memory cap)
KLEE: WARNING: killing 13306 states (over memory cap)
KLEE: WARNING: killing 13473 states (over memory cap)
KLEE: WARNING: killing 13360 states (over memory cap)
