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--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.: 137 204 1447 9913
Removed infinite loop in xennet_tx_buf_gc
Removed infinite loop in xennet_make_one_txreq
Removed infinite loop in napi_enable
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 xennet_move_rx_slot
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.542906999588
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to 'netif_tx_stop_all_queues' (function is undefined)
Removed calls to 'napi_disable' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'notify_remote_via_irq' (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
Removed calls to 'netdev_info' (function is undefined)
Defining function xenbus_scanf as symbolic
Removed calls to '__napi_schedule' (function is undefined)
Removed calls to 'gnttab_release_grant_reference' (function is undefined)
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Defining function gnttab_query_foreign_access as symbolic
Defining function printk as symbolic
Defining function gnttab_end_foreign_access_ref as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function find_next_bit as symbolic
Defining function net_ratelimit as symbolic
Defining function __phys_addr as symbolic
Defining function netif_skb_features as symbolic
Removed calls to 'gnttab_grant_foreign_access_ref' (function is undefined)
Defining function gnttab_claim_grant_reference as symbolic
Defining function get_phys_to_machine as symbolic
Defining function __pskb_pull_tail as symbolic
Removed calls to 'skb_add_rx_frag' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Defining function mod_timer as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function capable as symbolic
Defining function simple_strtoul as symbolic
Defining function sprintf as symbolic
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'xenbus_dev_fatal' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'gnttab_free_grant_references' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'unbind_from_irqhandler' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to 'netdev_update_features' (function is undefined)
Removed calls to 'netif_carrier_on' (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 'netdev_notify_peers' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'gnttab_end_foreign_access' (function is undefined)
Removed calls to 'dump_page' (function is undefined)
Defining function __get_page_tail as symbolic
Removed calls to 'netif_napi_del' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function xenbus_switch_state as symbolic
Defining function xenbus_frontend_closed as symbolic
Defining function netif_set_real_num_tx_queues as symbolic
Defining function xenbus_transaction_start as symbolic
Defining function xenbus_printf as symbolic
Defining function xenbus_write as symbolic
Defining function xenbus_transaction_end as symbolic
Defining function snprintf as symbolic
Defining function get_zeroed_page as symbolic
Defining function xenbus_grant_ring as symbolic
Defining function xenbus_alloc_evtchn as symbolic
Defining function bind_evtchn_to_irqhandler as symbolic
Defining function xenbus_free_evtchn as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function eth_type_trans as symbolic
Defining function napi_gro_receive as symbolic
Defining function skb_checksum_setup as symbolic
Defining function gnttab_alloc_grant_references as symbolic
Defining function xenbus_read as symbolic
Defining function register_netdev as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function __alloc_percpu 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_7 as symbolic
Defining function ldv_ndo_uninit_7 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 ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strlen
  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.589575052261
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 207 140 697 4296
INFO: Starting verification
KLEE: WARNING ONCE: function "xennet_open" 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 "xennet_make_one_txreq" has inline asm
KLEE: WARNING ONCE: function "xennet_make_txreqs" has inline asm
KLEE: WARNING ONCE: function "xennet_alloc_rx_buffers" has inline asm
KLEE: WARNING ONCE: function "napi_enable" 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_b45374c9-4a34-44d7-933a-2d804097a687/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:6512: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:10206: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9254: 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: MO43[65536] allocated at global:__per_cpu_offset
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9254: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9255: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9279: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9216: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9279: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9307: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14655 states (over memory cap)
KLEE: WARNING: killing 11291 states (over memory cap)
KLEE: WARNING: killing 10650 states (over memory cap)
KLEE: WARNING: killing 10709 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 10891 states (over memory cap)
KLEE: WARNING: killing 10473 states (over memory cap)
KLEE: WARNING: killing 11364 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9313: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11141 states (over memory cap)
KLEE: WARNING: killing 11265 states (over memory cap)
KLEE: WARNING: killing 11250 states (over memory cap)
KLEE: WARNING: killing 10824 states (over memory cap)
KLEE: WARNING: killing 10805 states (over memory cap)
KLEE: WARNING: killing 11339 states (over memory cap)
KLEE: WARNING: killing 12010 states (over memory cap)
KLEE: WARNING: killing 12274 states (over memory cap)
KLEE: WARNING: killing 11980 states (over memory cap)
KLEE: WARNING: killing 12033 states (over memory cap)
KLEE: WARNING: killing 11813 states (over memory cap)
KLEE: WARNING: killing 12142 states (over memory cap)
KLEE: WARNING: killing 11853 states (over memory cap)
KLEE: WARNING: killing 12103 states (over memory cap)
KLEE: WARNING: killing 11950 states (over memory cap)
KLEE: WARNING: killing 12072 states (over memory cap)
KLEE: WARNING: killing 11447 states (over memory cap)
KLEE: WARNING: killing 11559 states (over memory cap)
KLEE: WARNING: killing 11816 states (over memory cap)
KLEE: WARNING: killing 11859 states (over memory cap)
KLEE: WARNING: killing 12113 states (over memory cap)
KLEE: WARNING: killing 11893 states (over memory cap)
KLEE: WARNING: killing 12143 states (over memory cap)
KLEE: WARNING: killing 11717 states (over memory cap)
KLEE: WARNING: killing 11700 states (over memory cap)
KLEE: WARNING: killing 11414 states (over memory cap)
KLEE: WARNING: killing 11858 states (over memory cap)
KLEE: WARNING: killing 12241 states (over memory cap)
KLEE: WARNING: killing 11695 states (over memory cap)
KLEE: WARNING: killing 11545 states (over memory cap)
KLEE: WARNING: killing 11658 states (over memory cap)
KLEE: WARNING: killing 11378 states (over memory cap)
KLEE: WARNING: killing 11560 states (over memory cap)
KLEE: WARNING: killing 12269 states (over memory cap)
KLEE: WARNING: killing 11862 states (over memory cap)
KLEE: WARNING: killing 12043 states (over memory cap)
KLEE: WARNING: killing 11897 states (over memory cap)
KLEE: WARNING: killing 11550 states (over memory cap)
KLEE: WARNING: killing 11799 states (over memory cap)
KLEE: WARNING: killing 11649 states (over memory cap)
KLEE: WARNING: killing 12099 states (over memory cap)
KLEE: WARNING: killing 11752 states (over memory cap)
KLEE: WARNING: killing 12590 states (over memory cap)
KLEE: WARNING: killing 12048 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-opuLiA/linux-4.2-rc1.tar.xz-43_2a-drivers--net--xen-netfront.ko-entry_point_true-unreach-call.cil.out.c:9315: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11575 states (over memory cap)
KLEE: WARNING: killing 11627 states (over memory cap)
KLEE: WARNING: killing 11679 states (over memory cap)
KLEE: WARNING: killing 11274 states (over memory cap)
KLEE: WARNING: killing 11782 states (over memory cap)
KLEE: WARNING: killing 11703 states (over memory cap)
KLEE: WARNING: killing 11820 states (over memory cap)
KLEE: WARNING: killing 11738 states (over memory cap)
KLEE: WARNING: killing 11983 states (over memory cap)
KLEE: WARNING: killing 11582 states (over memory cap)
KLEE: WARNING: killing 11504 states (over memory cap)
KLEE: WARNING: killing 12262 states (over memory cap)
KLEE: WARNING: killing 12060 states (over memory cap)
KLEE: WARNING: killing 12175 states (over memory cap)
KLEE: WARNING: killing 11712 states (over memory cap)
