bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-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.: 77 100 730 4700
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in arch_local_irq_enable
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.22648191452
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function netdev_err as symbolic
Defining function crc32_le as symbolic
Defining function bitrev32 as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function printk as symbolic
Removed calls to 'disable_irq_nosync' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'skb_clone_tx_timestamp' (function is undefined)
Removed calls to 'skb_tstamp_tx' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to 'enable_irq' (function is undefined)
Defining function netdev_warn as symbolic
Defining function dev_trans_start as symbolic
Removed calls to '__netif_schedule' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function skb_put as symbolic
Defining function eth_type_trans as symbolic
Defining function skb_defer_rx_timestamp as symbolic
Defining function netdev_notice as symbolic
Removed calls to 'disable_irq' (function is undefined)
Defining function eth_mac_addr as symbolic
Defining function eth_validate_addr as symbolic
Defining function eth_change_mtu as symbolic
Removed calls to 'ether_setup' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function alloc_netdev_mqs as symbolic
Defining function ldv_ndo_init_1 as symbolic
Defining function ldv_ndo_uninit_1 as symbolic
Defining function ldv_ndo_init_2 as symbolic
Defining function ldv_ndo_uninit_2 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.268566131592
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 116 80 382 2385
INFO: Starting verification
KLEE: WARNING ONCE: function "ei_open" has inline asm
KLEE: WARNING ONCE: function "__NS8390_init" has inline asm
KLEE: WARNING ONCE: function "do_set_multicast_list" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "ei_start_xmit" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_disable" has inline asm
KLEE: WARNING ONCE: function "NS8390_trigger_send" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "ei_get_stats" has inline asm
KLEE: WARNING ONCE: function "ei_tx_timeout" has inline asm
KLEE: WARNING ONCE: function "netif_wake_queue" has inline asm
KLEE: WARNING ONCE: function "__ei_interrupt" has inline asm
KLEE: WARNING ONCE: function "ei_receive" has inline asm
KLEE: WARNING ONCE: function "ei_tx_intr" 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_b7504461-036f-462f-8a85-b7c073c91ade/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:5791: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:6116: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:6505: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:6570: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:5742: 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 9858 states (over memory cap)
KLEE: WARNING: killing 9630 states (over memory cap)
KLEE: WARNING: killing 9793 states (over memory cap)
KLEE: WARNING: killing 9953 states (over memory cap)
KLEE: WARNING: killing 9927 states (over memory cap)
KLEE: WARNING: killing 10275 states (over memory cap)
KLEE: WARNING: killing 10248 states (over memory cap)
KLEE: WARNING: killing 10788 states (over memory cap)
KLEE: WARNING: killing 11425 states (over memory cap)
KLEE: WARNING: killing 11495 states (over memory cap)
KLEE: WARNING: killing 12041 states (over memory cap)
KLEE: WARNING: killing 11646 states (over memory cap)
KLEE: WARNING: killing 12092 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:6574: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:5333: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12256 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:5998: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12796 states (over memory cap)
KLEE: WARNING: killing 12869 states (over memory cap)
KLEE: WARNING: killing 12664 states (over memory cap)
KLEE: WARNING: killing 13016 states (over memory cap)
KLEE: WARNING: killing 12716 states (over memory cap)
KLEE: WARNING: killing 12793 states (over memory cap)
KLEE: WARNING: killing 13050 states (over memory cap)
KLEE: WARNING: killing 13024 states (over memory cap)
KLEE: WARNING: killing 13276 states (over memory cap)
KLEE: WARNING: killing 13715 states (over memory cap)
KLEE: WARNING: killing 13689 states (over memory cap)
KLEE: WARNING: killing 14219 states (over memory cap)
KLEE: WARNING: killing 14011 states (over memory cap)
KLEE: WARNING: killing 14262 states (over memory cap)
KLEE: WARNING: killing 14056 states (over memory cap)
KLEE: WARNING: killing 14035 states (over memory cap)
KLEE: WARNING: killing 15105 states (over memory cap)
KLEE: WARNING: killing 13987 states (over memory cap)
KLEE: WARNING: killing 13867 states (over memory cap)
KLEE: WARNING: killing 14297 states (over memory cap)
KLEE: WARNING: killing 14454 states (over memory cap)
KLEE: WARNING: killing 14518 states (over memory cap)
KLEE: WARNING: killing 14848 states (over memory cap)
KLEE: WARNING: killing 14103 states (over memory cap)
KLEE: WARNING: killing 14707 states (over memory cap)
KLEE: WARNING: killing 14406 states (over memory cap)
KLEE: WARNING: killing 14914 states (over memory cap)
KLEE: WARNING: killing 14700 states (over memory cap)
KLEE: WARNING: killing 14668 states (over memory cap)
KLEE: WARNING: killing 13929 states (over memory cap)
KLEE: WARNING: killing 13721 states (over memory cap)
KLEE: WARNING: killing 14937 states (over memory cap)
KLEE: WARNING: killing 14904 states (over memory cap)
KLEE: WARNING: killing 14696 states (over memory cap)
KLEE: WARNING: killing 14932 states (over memory cap)
KLEE: WARNING: killing 14824 states (over memory cap)
KLEE: WARNING: killing 14966 states (over memory cap)
KLEE: WARNING: killing 15115 states (over memory cap)
KLEE: WARNING: killing 14640 states (over memory cap)
KLEE: WARNING: killing 14793 states (over memory cap)
KLEE: WARNING: killing 15459 states (over memory cap)
KLEE: WARNING: killing 14651 states (over memory cap)
KLEE: WARNING: killing 14445 states (over memory cap)
KLEE: WARNING: killing 14852 states (over memory cap)
KLEE: WARNING: killing 15166 states (over memory cap)
KLEE: WARNING: killing 15660 states (over memory cap)
KLEE: WARNING: killing 9036 states (over memory cap)
KLEE: WARNING: killing 14596 states (over memory cap)
KLEE: WARNING: killing 14646 states (over memory cap)
KLEE: WARNING: killing 15138 states (over memory cap)
KLEE: WARNING: killing 15370 states (over memory cap)
KLEE: WARNING: killing 14913 states (over memory cap)
KLEE: WARNING: killing 8692 states (over memory cap)
KLEE: WARNING: killing 14459 states (over memory cap)
KLEE: WARNING: killing 14597 states (over memory cap)
KLEE: WARNING: killing 14823 states (over memory cap)
KLEE: WARNING: killing 15396 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-GotAqC/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--8390--8390.ko-entry_point_false-unreach-call.cil.out.c:6683: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8709 states (over memory cap)
KLEE: WARNING: killing 14428 states (over memory cap)
KLEE: WARNING: killing 15076 states (over memory cap)
KLEE: WARNING: killing 14703 states (over memory cap)
KLEE: WARNING: killing 8480 states (over memory cap)
KLEE: WARNING: killing 14073 states (over memory cap)
KLEE: WARNING: killing 15232 states (over memory cap)
KLEE: WARNING: killing 8447 states (over memory cap)
KLEE: WARNING: killing 15031 states (over memory cap)
KLEE: WARNING: killing 15001 states (over memory cap)
KLEE: WARNING: killing 8496 states (over memory cap)
KLEE: WARNING: killing 14465 states (over memory cap)
KLEE: WARNING: killing 8394 states (over memory cap)
KLEE: WARNING: killing 14429 states (over memory cap)
KLEE: WARNING: killing 15158 states (over memory cap)
KLEE: WARNING: killing 8523 states (over memory cap)
KLEE: WARNING: killing 14286 states (over memory cap)
KLEE: WARNING: killing 8258 states (over memory cap)
KLEE: WARNING: killing 14676 states (over memory cap)
KLEE: WARNING: killing 14898 states (over memory cap)
KLEE: WARNING: killing 8226 states (over memory cap)
KLEE: WARNING: killing 14526 states (over memory cap)
KLEE: WARNING: killing 8202 states (over memory cap)
KLEE: WARNING: killing 14902 states (over memory cap)
KLEE: WARNING: killing 8589 states (over memory cap)
KLEE: WARNING: killing 14709 states (over memory cap)
KLEE: WARNING: killing 8322 states (over memory cap)
KLEE: WARNING: killing 15076 states (over memory cap)
KLEE: WARNING: killing 8383 states (over memory cap)
KLEE: WARNING: killing 14883 states (over memory cap)
KLEE: WARNING: killing 8365 states (over memory cap)
KLEE: WARNING: killing 14270 states (over memory cap)
KLEE: WARNING: killing 8102 states (over memory cap)
KLEE: WARNING: killing 14806 states (over memory cap)
KLEE: WARNING: killing 8482 states (over memory cap)
KLEE: WARNING: killing 8151 states (over memory cap)
KLEE: WARNING: killing 8066 states (over memory cap)
KLEE: WARNING: killing 14671 states (over memory cap)
KLEE: WARNING: killing 8212 states (over memory cap)
KLEE: WARNING: killing 14720 states (over memory cap)
KLEE: WARNING: killing 8190 states (over memory cap)
KLEE: WARNING: killing 8027 states (over memory cap)
KLEE: WARNING: killing 15082 states (over memory cap)
KLEE: WARNING: killing 8733 states (over memory cap)
KLEE: WARNING: killing 15053 states (over memory cap)
KLEE: WARNING: killing 8551 states (over memory cap)
KLEE: WARNING: killing 14694 states (over memory cap)
KLEE: WARNING: killing 8286 states (over memory cap)
KLEE: WARNING: killing 14732 states (over memory cap)
KLEE: WARNING: killing 8590 states (over memory cap)
KLEE: WARNING: killing 7947 states (over memory cap)
KLEE: WARNING: killing 14614 states (over memory cap)
