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-08_1a-drivers--net--xen-netback--xen-netback.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.: 201 263 1962 15335
Removed infinite loop in set_backend_state
Removed infinite loop in napi_enable
Removed infinite loop in xenvif_connect
Removed infinite loop in xenvif_tx_dealloc_action
Removed infinite loop in xenvif_grant_handle_reset
Removed infinite loop in xenvif_rx_action
Removed infinite loop in xenvif_gop_frag_copy
Removed infinite loop in xenvif_tx_action
Removed infinite loop in xenvif_handle_frag_list
Removed infinite loop in get_page
Removed infinite loop in xenvif_grant_handle_set
Removed infinite loop in xenvif_idx_unmap
Removed infinite loop in __skb_put
Removed infinite loop in xenvif_get_requests
Removed infinite loop in xenvif_zerocopy_callback
Removed infinite loop in xenvif_start_xmit
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.739890098572
Removed calls to 'xenbus_dev_fatal' (function is undefined)
Removed calls to 'device_unregister' (function is undefined)
Defining function add_uevent_var as symbolic
Removed calls to 'gnttab_free_pages' (function is undefined)
Removed calls to 'netdev_warn' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Removed calls to 'unregister_xenbus_watch' (function is undefined)
Defining function kobject_uevent as symbolic
Defining function xenbus_rm as symbolic
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Defining function printk as symbolic
Removed calls to '__put_task_struct' (function is undefined)
Removed calls to 'unbind_from_irqhandler' (function is undefined)
Removed calls to 'netif_napi_del' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Defining function kthread_stop as symbolic
Defining function xenbus_unmap_ring_vfree as symbolic
Removed calls to 'disable_irq' (function is undefined)
Removed calls to 'napi_disable' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function xenbus_scanf as symbolic
Defining function vzalloc as symbolic
Defining function snprintf as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'netdev_err' (function is undefined)
Defining function netif_set_real_num_tx_queues as symbolic
Defining function netif_set_real_num_rx_queues as symbolic
Removed calls to 'netdev_update_features' (function is undefined)
Defining function xenbus_watch_pathfmt as symbolic
Defining function xenbus_read as symbolic
Defining function xenbus_switch_state as symbolic
Defining function dev_set_mtu as symbolic
Removed calls to 'enable_irq' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function xenbus_gather as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function bind_interdomain_evtchn_to_irqhandler as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'gnttab_batch_copy' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'notify_remote_via_irq' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'netdev_info' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'kfree_skb' (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 '___might_sleep' (function is undefined)
Defining function kthread_create_on_node as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Defining function wake_up_process as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function _cond_resched as symbolic
Defining function gnttab_unmap_refs as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function __phys_addr as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Defining function get_phys_to_machine as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Removed calls to 'put_page' (function is undefined)
Defining function gnttab_map_refs as symbolic
Removed calls to 'dump_page' (function is undefined)
Defining function net_ratelimit as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_receive_skb_sk as symbolic
Defining function __skb_flow_dissect as symbolic
Defining function skb_checksum_setup as symbolic
Defining function skb_copy_bits as symbolic
Defining function alloc_pages_current as symbolic
Defining function __get_page_tail as symbolic
Defining function __alloc_skb as symbolic
Defining function mod_timer as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function xenbus_map_ring_valloc as symbolic
Defining function gnttab_alloc_pages as symbolic
Defining function register_xenbus_watch as symbolic
Defining function mod_timer_pending as symbolic
Defining function simple_strtoul as symbolic
Defining function xenbus_dev_is_online as symbolic
Defining function xenbus_transaction_start as symbolic
Defining function xenbus_printf as symbolic
Defining function xenbus_transaction_end as symbolic
Defining function alloc_netdev_mqs as symbolic
Defining function register_netdev as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function simple_write_to_buffer as symbolic
Removed calls to 'netif_tx_stop_all_queues' (function is undefined)
Defining function eth_mac_addr as symbolic
Defining function eth_validate_addr as symbolic
Defining function ___ratelimit as symbolic
Defining function ethtool_op_get_link as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Defining function ldv_ndo_init_2 as symbolic
Defining function ldv_ndo_uninit_2 as symbolic
Defining function __xenbus_register_backend as symbolic
Defining function __bitmap_weight as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  strlen
  strncmp
  __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.857672214508
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 273 197 1148 8623
INFO: Starting verification
KLEE: WARNING ONCE: function "set_backend_state" has inline asm
KLEE: WARNING ONCE: function "xenvif_connect" has inline asm
KLEE: WARNING ONCE: function "xenvif_carrier_on" has inline asm
KLEE: WARNING ONCE: function "xenvif_disconnect" has inline asm
KLEE: WARNING ONCE: function "xenvif_carrier_off" has inline asm
KLEE: WARNING ONCE: function "xenvif_up" has inline asm
KLEE: WARNING ONCE: function "xenvif_napi_schedule_or_enable_events" has inline asm
KLEE: WARNING ONCE: function "napi_schedule" has inline asm
KLEE: WARNING ONCE: function "xenvif_zerocopy_callback" has inline asm
KLEE: WARNING ONCE: function "xenvif_kthread_guest_rx" has inline asm
KLEE: WARNING ONCE: function "xenvif_tx_dealloc_action" has inline asm
KLEE: WARNING ONCE: function "xenvif_grant_handle_reset" has inline asm
KLEE: WARNING ONCE: function "push_tx_responses" has inline asm
KLEE: WARNING ONCE: function "xenvif_have_rx_work" has inline asm
KLEE: WARNING ONCE: function "xenvif_gop_frag_copy" has inline asm
KLEE: WARNING ONCE: function "xenvif_open" has inline asm
KLEE: WARNING ONCE: function "xenvif_start_xmit" has inline asm
KLEE: WARNING ONCE: function "xenvif_rx_queue_tail" has inline asm
KLEE: WARNING ONCE: function "xenvif_rx_ring_slots_available" has inline asm
KLEE: WARNING ONCE: function "xenvif_tx_action" has inline asm
KLEE: WARNING ONCE: function "xenvif_fill_frags" has inline asm
KLEE: WARNING ONCE: function "xenvif_idx_unmap" has inline asm
KLEE: WARNING ONCE: function "xenvif_skb_zerocopy_prepare" has inline asm
KLEE: WARNING ONCE: function "xenvif_skb_zerocopy_complete" has inline asm
KLEE: WARNING: undefined reference to function: ether_setup
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_c81744db-0901-425d-af24-0e60c8b059f4/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: WARNING: killing 9545 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 9857 states (over memory cap)
KLEE: WARNING: killing 9157 states (over memory cap)
KLEE: WARNING: killing 9303 states (over memory cap)
KLEE: WARNING: killing 8947 states (over memory cap)
KLEE: WARNING: killing 8925 states (over memory cap)
KLEE: WARNING: killing 8901 states (over memory cap)
KLEE: WARNING: killing 9298 states (over memory cap)
KLEE: WARNING: killing 9030 states (over memory cap)
KLEE: WARNING: killing 9847 states (over memory cap)
KLEE: WARNING: killing 9660 states (over memory cap)
KLEE: WARNING: killing 9479 states (over memory cap)
KLEE: WARNING: killing 10122 states (over memory cap)
KLEE: WARNING: killing 9859 states (over memory cap)
KLEE: WARNING: killing 10254 states (over memory cap)
KLEE: WARNING: killing 9988 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-fCcsYH/linux-4.2-rc1.tar.xz-08_1a-drivers--net--xen-netback--xen-netback.ko-entry_point_false-unreach-call.cil.out.c:13031: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10302 states (over memory cap)
KLEE: WARNING: killing 10287 states (over memory cap)
KLEE: WARNING: killing 10518 states (over memory cap)
KLEE: WARNING: killing 10257 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-fCcsYH/linux-4.2-rc1.tar.xz-08_1a-drivers--net--xen-netback--xen-netback.ko-entry_point_false-unreach-call.cil.out.c:10903: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10162 states (over memory cap)
KLEE: WARNING: killing 10472 states (over memory cap)
KLEE: WARNING: killing 10378 states (over memory cap)
KLEE: WARNING: killing 10446 states (over memory cap)
KLEE: WARNING: killing 9942 states (over memory cap)
KLEE: WARNING: killing 10251 states (over memory cap)
KLEE: WARNING: killing 10314 states (over memory cap)
KLEE: WARNING: killing 10543 states (over memory cap)
KLEE: WARNING: killing 10769 states (over memory cap)
KLEE: WARNING: killing 10593 states (over memory cap)
KLEE: WARNING: killing 10342 states (over memory cap)
KLEE: WARNING: killing 10727 states (over memory cap)
KLEE: WARNING: killing 10954 states (over memory cap)
KLEE: WARNING: killing 10133 states (over memory cap)
KLEE: WARNING: killing 10922 states (over memory cap)
KLEE: WARNING: killing 10425 states (over memory cap)
KLEE: WARNING: killing 10495 states (over memory cap)
KLEE: WARNING: killing 11036 states (over memory cap)
KLEE: WARNING: killing 10466 states (over memory cap)
KLEE: WARNING: killing 10288 states (over memory cap)
KLEE: WARNING: killing 10597 states (over memory cap)
KLEE: WARNING: killing 10581 states (over memory cap)
KLEE: WARNING: killing 10725 states (over memory cap)
KLEE: WARNING: killing 10477 states (over memory cap)
KLEE: WARNING: killing 10621 states (over memory cap)
KLEE: WARNING: killing 10684 states (over memory cap)
KLEE: WARNING: killing 10196 states (over memory cap)
KLEE: WARNING: killing 10652 states (over memory cap)
KLEE: WARNING: killing 10639 states (over memory cap)
KLEE: WARNING: killing 10470 states (over memory cap)
KLEE: WARNING: killing 10533 states (over memory cap)
KLEE: WARNING: killing 10834 states (over memory cap)
KLEE: WARNING: killing 10354 states (over memory cap)
KLEE: WARNING: killing 10810 states (over memory cap)
KLEE: WARNING: killing 10719 states (over memory cap)
KLEE: WARNING: killing 10547 states (over memory cap)
KLEE: WARNING: killing 10533 states (over memory cap)
KLEE: WARNING: killing 10133 states (over memory cap)
KLEE: WARNING: killing 10743 states (over memory cap)
KLEE: WARNING: killing 10338 states (over memory cap)
KLEE: WARNING: killing 10636 states (over memory cap)
KLEE: WARNING: killing 10467 states (over memory cap)
KLEE: WARNING: killing 10304 states (over memory cap)
KLEE: WARNING: killing 10598 states (over memory cap)
KLEE: WARNING: killing 10667 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-fCcsYH/linux-4.2-rc1.tar.xz-08_1a-drivers--net--xen-netback--xen-netback.ko-entry_point_false-unreach-call.cil.out.c:11500: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10728 states (over memory cap)
KLEE: WARNING: killing 10874 states (over memory cap)
KLEE: WARNING: killing 10476 states (over memory cap)
KLEE: WARNING: killing 10775 states (over memory cap)
KLEE: WARNING: killing 10603 states (over memory cap)
KLEE: WARNING: killing 10207 states (over memory cap)
KLEE: WARNING: killing 10965 states (over memory cap)
KLEE: WARNING: killing 10800 states (over memory cap)
KLEE: WARNING: killing 10558 states (over memory cap)
KLEE: WARNING: killing 10932 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10743 states (over memory cap)
KLEE: WARNING: killing 10503 states (over memory cap)
KLEE: WARNING: killing 10493 states (over memory cap)
KLEE: WARNING: killing 10783 states (over memory cap)
KLEE: WARNING: killing 11231 states (over memory cap)
KLEE: WARNING: killing 11071 states (over memory cap)
KLEE: WARNING: killing 11057 states (over memory cap)
KLEE: WARNING: killing 10366 states (over memory cap)
KLEE: WARNING: killing 10202 states (over memory cap)
KLEE: WARNING: killing 10416 states (over memory cap)
KLEE: WARNING: killing 10627 states (over memory cap)
KLEE: WARNING: killing 10389 states (over memory cap)
KLEE: WARNING: killing 10605 states (over memory cap)
KLEE: WARNING: killing 10063 states (over memory cap)
KLEE: WARNING: killing 10806 states (over memory cap)
KLEE: WARNING: killing 10644 states (over memory cap)
KLEE: WARNING: killing 10558 states (over memory cap)
KLEE: WARNING: killing 10546 states (over memory cap)
KLEE: WARNING: killing 10382 states (over memory cap)
KLEE: WARNING: killing 10597 states (over memory cap)
KLEE: WARNING: killing 10738 states (over memory cap)
KLEE: WARNING: killing 10429 states (over memory cap)
KLEE: WARNING: killing 10863 states (over memory cap)
KLEE: WARNING: killing 10630 states (over memory cap)
KLEE: WARNING: killing 11068 states (over memory cap)
KLEE: WARNING: killing 10541 states (over memory cap)
KLEE: WARNING: killing 10672 states (over memory cap)
KLEE: WARNING: killing 10742 states (over memory cap)
KLEE: WARNING: killing 10732 states (over memory cap)
KLEE: WARNING: killing 10717 states (over memory cap)
KLEE: WARNING: killing 10187 states (over memory cap)
KLEE: WARNING: killing 10327 states (over memory cap)
KLEE: WARNING: killing 10607 states (over memory cap)
KLEE: WARNING: killing 10669 states (over memory cap)
KLEE: WARNING: killing 10656 states (over memory cap)
KLEE: WARNING: killing 10651 states (over memory cap)
KLEE: WARNING: killing 10419 states (over memory cap)
KLEE: WARNING: killing 10920 states (over memory cap)
KLEE: WARNING: killing 10617 states (over memory cap)
KLEE: WARNING: killing 10834 states (over memory cap)
KLEE: WARNING: killing 10527 states (over memory cap)
KLEE: WARNING: killing 10078 states (over memory cap)
KLEE: WARNING: killing 10359 states (over memory cap)
KLEE: WARNING: killing 11010 states (over memory cap)
KLEE: WARNING: killing 10491 states (over memory cap)
KLEE: WARNING: killing 10992 states (over memory cap)
KLEE: WARNING: killing 11054 states (over memory cap)
KLEE: WARNING: killing 10095 states (over memory cap)
KLEE: WARNING: killing 10736 states (over memory cap)
KLEE: WARNING: killing 10724 states (over memory cap)
KLEE: WARNING: killing 10134 states (over memory cap)
KLEE: WARNING: killing 10704 states (over memory cap)
KLEE: WARNING: killing 10473 states (over memory cap)
KLEE: WARNING: killing 10824 states (over memory cap)
KLEE: WARNING: killing 10674 states (over memory cap)
KLEE: WARNING: killing 10734 states (over memory cap)
KLEE: WARNING: killing 10510 states (over memory cap)
KLEE: WARNING: killing 10719 states (over memory cap)
KLEE: WARNING: killing 10418 states (over memory cap)
KLEE: WARNING: killing 10478 states (over memory cap)
KLEE: WARNING: killing 10973 states (over memory cap)
KLEE: WARNING: killing 10603 states (over memory cap)
KLEE: WARNING: killing 10883 states (over memory cap)
KLEE: WARNING: killing 10368 states (over memory cap)
KLEE: WARNING: killing 10713 states (over memory cap)
KLEE: WARNING: killing 10420 states (over memory cap)
KLEE: WARNING: killing 10912 states (over memory cap)
KLEE: WARNING: killing 10544 states (over memory cap)
KLEE: WARNING: killing 10893 states (over memory cap)
KLEE: WARNING: killing 10884 states (over memory cap)
KLEE: WARNING: killing 10297 states (over memory cap)
KLEE: WARNING: killing 10361 states (over memory cap)
KLEE: WARNING: killing 10347 states (over memory cap)
KLEE: WARNING: killing 10766 states (over memory cap)
KLEE: WARNING: killing 10618 states (over memory cap)
KLEE: WARNING: killing 10531 states (over memory cap)
KLEE: WARNING: killing 10805 states (over memory cap)
KLEE: WARNING: killing 10728 states (over memory cap)
KLEE: WARNING: killing 10858 states (over memory cap)
KLEE: WARNING: killing 10783 states (over memory cap)
KLEE: WARNING: killing 10346 states (over memory cap)
KLEE: WARNING: killing 10333 states (over memory cap)
KLEE: WARNING: killing 10956 states (over memory cap)
KLEE: WARNING: killing 10451 states (over memory cap)
KLEE: WARNING: killing 10866 states (over memory cap)
KLEE: WARNING: killing 10713 states (over memory cap)
KLEE: WARNING: killing 10562 states (over memory cap)
KLEE: WARNING: killing 10273 states (over memory cap)
KLEE: WARNING: killing 10194 states (over memory cap)
KLEE: WARNING: killing 10601 states (over memory cap)
KLEE: WARNING: killing 10659 states (over memory cap)
KLEE: WARNING: killing 10440 states (over memory cap)
KLEE: WARNING: killing 10361 states (over memory cap)
KLEE: WARNING: killing 10281 states (over memory cap)
KLEE: WARNING: killing 10968 states (over memory cap)
KLEE: WARNING: killing 10263 states (over memory cap)
KLEE: WARNING: killing 10735 states (over memory cap)
KLEE: WARNING: killing 10729 states (over memory cap)
KLEE: WARNING: killing 11002 states (over memory cap)
KLEE: WARNING: killing 10644 states (over memory cap)
KLEE: WARNING: killing 10499 states (over memory cap)
KLEE: WARNING: killing 10903 states (over memory cap)
KLEE: WARNING: killing 10547 states (over memory cap)
KLEE: WARNING: killing 10330 states (over memory cap)
KLEE: WARNING: killing 10873 states (over memory cap)
KLEE: WARNING: killing 10654 states (over memory cap)
KLEE: WARNING: killing 10780 states (over memory cap)
KLEE: WARNING: killing 10358 states (over memory cap)
KLEE: WARNING: killing 10759 states (over memory cap)
KLEE: WARNING: killing 10887 states (over memory cap)
KLEE: WARNING: killing 10402 states (over memory cap)
KLEE: WARNING: killing 10391 states (over memory cap)
KLEE: WARNING: killing 10654 states (over memory cap)
KLEE: WARNING: killing 10296 states (over memory cap)
KLEE: WARNING: killing 10354 states (over memory cap)
KLEE: WARNING: killing 10552 states (over memory cap)
KLEE: WARNING: killing 10611 states (over memory cap)
KLEE: WARNING: killing 10595 states (over memory cap)
KLEE: WARNING: killing 10519 states (over memory cap)
