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/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.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.: 119 207 1508 10933
Removed infinite loop in xennet_tx_buf_gc
Removed infinite loop in xennet_alloc_rx_buffers
Removed infinite loop in get_page
Removed infinite loop in xennet_get_responses
Removed infinite loop in xennet_fill_frags
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 xennet_move_rx_slot
Removed infinite loop in xennet_start_xmit
Removed infinite loop in xennet_make_frags
Removed infinite loop in napi_enable
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.51668381691
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'xenbus_dev_fatal' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'netdev_notify_peers' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Removed calls to 'unbind_from_irqhandler' (function is undefined)
Removed calls to 'gnttab_end_foreign_access' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function xenbus_frontend_closed as symbolic
Defining function xenbus_scanf as symbolic
Defining function _dev_info as symbolic
Removed calls to 'gnttab_release_grant_reference' (function is undefined)
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to '__netif_schedule' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'skb_add_rx_frag' (function is undefined)
Removed calls to 'gnttab_grant_foreign_access_ref' (function is undefined)
Removed calls to 'notify_remote_via_irq' (function is undefined)
Defining function gnttab_claim_grant_reference as symbolic
Defining function mod_timer as symbolic
Defining function alloc_pages_current as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function gnttab_query_foreign_access as symbolic
Defining function printk as symbolic
Defining function gnttab_end_foreign_access_ref as symbolic
Defining function get_phys_to_machine as symbolic
Removed calls to 'dump_page' (function is undefined)
Defining function __get_page_tail as symbolic
Defining function netif_set_real_num_tx_queues as symbolic
Defining function __phys_addr as symbolic
Removed calls to '__napi_schedule' (function is undefined)
Defining function net_ratelimit as symbolic
Defining function xenbus_read as symbolic
Defining function simple_strtoul as symbolic
Defining function device_create_file as symbolic
Defining function register_netdev as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function __alloc_percpu as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function find_next_bit as symbolic
Removed calls to 'gnttab_free_grant_references' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to '__skb_get_hash' (function is undefined)
Defining function eth_mac_addr as symbolic
Defining function eth_validate_addr as symbolic
Defining function netdev_info as symbolic
Defining function netif_skb_features as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function sprintf as symbolic
Defining function capable as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'xenbus_unregister_driver' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_ndo_init_4 as symbolic
Defining function ldv_suspend_2 as symbolic
Defining function xen_has_pv_nic_devices as symbolic
Defining function xenbus_register_frontend as symbolic
Defining function __bitmap_weight as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_clone as symbolic
Defining function skb_copy as symbolic
Defining function vmalloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strlen
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_u32_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.400568008423
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 161 127 592 3640
INFO: Starting verification
KLEE: WARNING ONCE: function "xennet_open" has inline asm
KLEE: WARNING ONCE: function "xennet_close" has inline asm
KLEE: WARNING ONCE: function "xennet_start_xmit" has inline asm
KLEE: WARNING ONCE: function "xennet_get_stats64" has inline asm
KLEE: WARNING ONCE: function "xennet_tx_buf_gc" has inline asm
KLEE: WARNING ONCE: function "napi_schedule" has inline asm
KLEE: WARNING ONCE: function "netif_tx_stop_queue" has inline asm
KLEE: WARNING ONCE: function "xennet_alloc_rx_buffers" has inline asm
KLEE: WARNING ONCE: function "get_page" 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_49595201-1b1f-4aa5-8a8e-9bda71a05c08/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:10983: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:6338: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9432: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 65536 bytes on read, may be slow and/or crash: MO36[65536] allocated at global:__per_cpu_offset
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9432: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9434: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:10378: 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 9829 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9457: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13046 states (over memory cap)
KLEE: WARNING: killing 12569 states (over memory cap)
KLEE: WARNING: killing 13332 states (over memory cap)
KLEE: WARNING: killing 7257 states (over memory cap)
KLEE: WARNING: killing 7106 states (over memory cap)
KLEE: WARNING: killing 7024 states (over memory cap)
KLEE: WARNING: killing 13080 states (over memory cap)
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 6922 states (over memory cap)
KLEE: WARNING: killing 13292 states (over memory cap)
KLEE: WARNING: killing 7367 states (over memory cap)
KLEE: WARNING: killing 6952 states (over memory cap)
KLEE: WARNING: killing 6805 states (over memory cap)
KLEE: WARNING: killing 7203 states (over memory cap)
KLEE: WARNING: killing 13062 states (over memory cap)
KLEE: WARNING: killing 7111 states (over memory cap)
KLEE: WARNING: killing 7034 states (over memory cap)
KLEE: WARNING: killing 6825 states (over memory cap)
KLEE: WARNING: killing 7150 states (over memory cap)
KLEE: WARNING: killing 7144 states (over memory cap)
KLEE: WARNING: killing 6934 states (over memory cap)
KLEE: WARNING: killing 6795 states (over memory cap)
KLEE: WARNING: killing 7120 states (over memory cap)
KLEE: WARNING: killing 6842 states (over memory cap)
KLEE: WARNING: killing 7102 states (over memory cap)
KLEE: WARNING: killing 7430 states (over memory cap)
KLEE: WARNING: killing 7087 states (over memory cap)
KLEE: WARNING: killing 6813 states (over memory cap)
KLEE: WARNING: killing 7071 states (over memory cap)
KLEE: WARNING: killing 6729 states (over memory cap)
KLEE: WARNING: killing 6986 states (over memory cap)
KLEE: WARNING: killing 7178 states (over memory cap)
KLEE: WARNING: killing 6771 states (over memory cap)
KLEE: WARNING: killing 6632 states (over memory cap)
KLEE: WARNING: killing 7215 states (over memory cap)
KLEE: WARNING: killing 7206 states (over memory cap)
KLEE: WARNING: killing 6938 states (over memory cap)
KLEE: WARNING: killing 7192 states (over memory cap)
KLEE: WARNING: killing 6858 states (over memory cap)
KLEE: WARNING: killing 7045 states (over memory cap)
KLEE: WARNING: killing 7037 states (over memory cap)
KLEE: WARNING: killing 7162 states (over memory cap)
KLEE: WARNING: killing 7088 states (over memory cap)
KLEE: WARNING: killing 6622 states (over memory cap)
KLEE: WARNING: killing 6872 states (over memory cap)
KLEE: WARNING: killing 7320 states (over memory cap)
KLEE: WARNING: killing 6726 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9463: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 7044 states (over memory cap)
KLEE: WARNING: killing 7164 states (over memory cap)
KLEE: WARNING: killing 7419 states (over memory cap)
KLEE: WARNING: killing 7149 states (over memory cap)
KLEE: WARNING: killing 6753 states (over memory cap)
KLEE: WARNING: killing 7004 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-VN7S0G/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9465: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 6864 states (over memory cap)
KLEE: WARNING: killing 6790 states (over memory cap)
KLEE: WARNING: killing 7037 states (over memory cap)
KLEE: WARNING: killing 7158 states (over memory cap)
KLEE: WARNING: killing 7021 states (over memory cap)
KLEE: WARNING: killing 7140 states (over memory cap)
KLEE: WARNING: killing 6942 states (over memory cap)
KLEE: WARNING: killing 6997 states (over memory cap)
KLEE: WARNING: killing 7373 states (over memory cap)
KLEE: WARNING: killing 7431 states (over memory cap)
KLEE: WARNING: killing 6912 states (over memory cap)
KLEE: WARNING: killing 6779 states (over memory cap)
KLEE: WARNING: killing 7279 states (over memory cap)
KLEE: WARNING: killing 6952 states (over memory cap)
KLEE: WARNING: killing 6755 states (over memory cap)
KLEE: WARNING: killing 7129 states (over memory cap)
KLEE: WARNING: killing 6992 states (over memory cap)
KLEE: WARNING: killing 6982 states (over memory cap)
KLEE: WARNING: killing 7038 states (over memory cap)
KLEE: WARNING: killing 7285 states (over memory cap)
KLEE: WARNING: killing 7152 states (over memory cap)
KLEE: WARNING: killing 7081 states (over memory cap)
KLEE: WARNING: killing 7139 states (over memory cap)
KLEE: WARNING: killing 7006 states (over memory cap)
KLEE: WARNING: killing 7249 states (over memory cap)
KLEE: WARNING: killing 7307 states (over memory cap)
KLEE: WARNING: killing 6921 states (over memory cap)
KLEE: WARNING: killing 7165 states (over memory cap)
KLEE: WARNING: killing 7096 states (over memory cap)
KLEE: WARNING: killing 7087 states (over memory cap)
KLEE: WARNING: killing 7207 states (over memory cap)
KLEE: WARNING: killing 7012 states (over memory cap)
KLEE: WARNING: killing 7065 states (over memory cap)
KLEE: WARNING: killing 7183 states (over memory cap)
KLEE: WARNING: killing 6928 states (over memory cap)
KLEE: WARNING: killing 7232 states (over memory cap)
