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-alloc-spinlock__drivers-net-xen-netfront_false-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.: 214 424 2179 13976
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.544926166534
Removed calls to 'xenbus_dev_fatal' (function is undefined)
Removed calls to 'unbind_from_irqhandler' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'netdev_update_features' (function is undefined)
Removed calls to 'rtnl_unlock' (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 'gnttab_grant_foreign_access_ref' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'notify_remote_via_irq' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'netdev_notify_peers' (function is undefined)
Defining function xenbus_switch_state 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_end_foreign_access' (function is undefined)
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to 'gnttab_release_grant_reference' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'skb_add_rx_frag' (function is undefined)
Defining function gnttab_claim_grant_reference as symbolic
Defining function mod_timer as symbolic
Defining function external_allocated_data 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 netpoll_trap 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 xenbus_transaction_start as symbolic
Defining function xenbus_printf as symbolic
Defining function xenbus_write as symbolic
Defining function xenbus_transaction_end as symbolic
Removed calls to 'netif_carrier_off' (function is undefined)
Defining function get_zeroed_page as symbolic
Defining function __phys_addr 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 '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function snprintf as symbolic
Defining function xenbus_read as symbolic
Defining function simple_strtoul as symbolic
Defining function sprintf as symbolic
Defining function capable as symbolic
Removed calls to 'xenbus_unregister_driver' (function is undefined)
Defining function xen_has_pv_nic_devices as symbolic
Defining function xenbus_register_frontend as symbolic
Defining function ethtool_op_get_link as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function find_next_bit as symbolic
Defining function netdev_info as symbolic
Defining function eth_mac_addr as symbolic
Removed calls to 'consume_skb' (function is undefined)
Defining function net_ratelimit as symbolic
Defining function netif_skb_dev_features as symbolic
Removed calls to 'gnttab_free_grant_references' (function is undefined)
Defining function eth_validate_addr as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to 'free_percpu' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to '__might_sleep' (function is undefined)
Defining function device_create_file as symbolic
Defining function register_netdev as symbolic
Defining function ldv_pre_register_netdev as symbolic
Defining function __alloc_percpu as symbolic
Defining function gnttab_alloc_grant_references as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'napi_gro_flush' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to '__napi_complete' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function __pskb_pull_tail as symbolic
Defining function eth_type_trans as symbolic
Defining function napi_gro_receive as symbolic
Defining function skb_checksum_setup as symbolic
Defining function dev_warn as symbolic
Defining function alloc_etherdev_mqs 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_after_alloc' (function is undefined)
Linked our definitions to these undefined functions:
  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.581236124039
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 266 343 943 6525
INFO: Starting verification
KLEE: WARNING ONCE: function "xennet_tx_buf_gc" 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: function "xennet_get_stats64" has inline asm
KLEE: WARNING ONCE: function "xennet_start_xmit" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "xennet_close" has inline asm
KLEE: WARNING ONCE: function "xennet_open" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_a514238d-3d95-4201-ba7d-7be3ac5495b3/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-CZpgHo/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-xen-netfront_false-unreach-call.cil.c:9695: 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 22000 states (over memory cap)
KLEE: WARNING: killing 14734 states (over memory cap)
KLEE: WARNING: killing 14346 states (over memory cap)
KLEE: WARNING: killing 14427 states (over memory cap)
KLEE: WARNING: killing 14052 states (over memory cap)
KLEE: WARNING: killing 13668 states (over memory cap)
KLEE: WARNING: killing 13646 states (over memory cap)
KLEE: WARNING: killing 14090 states (over memory cap)
KLEE: WARNING: killing 14534 states (over memory cap)
KLEE: WARNING: killing 14161 states (over memory cap)
KLEE: WARNING: killing 14250 states (over memory cap)
KLEE: WARNING: killing 14230 states (over memory cap)
KLEE: WARNING: killing 14783 states (over memory cap)
KLEE: WARNING: killing 13955 states (over memory cap)
KLEE: WARNING: killing 14509 states (over memory cap)
KLEE: WARNING: killing 14942 states (over memory cap)
KLEE: WARNING: killing 14919 states (over memory cap)
KLEE: WARNING: killing 15127 states (over memory cap)
KLEE: WARNING: killing 16024 states (over memory cap)
KLEE: WARNING: killing 15423 states (over memory cap)
KLEE: WARNING: killing 15512 states (over memory cap)
KLEE: WARNING: killing 15607 states (over memory cap)
KLEE: WARNING: killing 16268 states (over memory cap)
KLEE: WARNING: killing 15785 states (over memory cap)
KLEE: WARNING: killing 15533 states (over memory cap)
KLEE: WARNING: killing 16078 states (over memory cap)
KLEE: WARNING: killing 16170 states (over memory cap)
KLEE: WARNING: killing 16379 states (over memory cap)
KLEE: WARNING: killing 16810 states (over memory cap)
KLEE: WARNING: killing 16227 states (over memory cap)
KLEE: WARNING: killing 16209 states (over memory cap)
KLEE: WARNING: killing 16523 states (over memory cap)
KLEE: WARNING: killing 16727 states (over memory cap)
KLEE: WARNING: killing 16262 states (over memory cap)
KLEE: WARNING: killing 16132 states (over memory cap)
KLEE: WARNING: killing 15997 states (over memory cap)
KLEE: WARNING: killing 15977 states (over memory cap)
KLEE: WARNING: killing 15616 states (over memory cap)
KLEE: WARNING: killing 16044 states (over memory cap)
KLEE: WARNING: killing 15688 states (over memory cap)
KLEE: WARNING: killing 15114 states (over memory cap)
KLEE: WARNING: killing 15432 states (over memory cap)
KLEE: WARNING: killing 15631 states (over memory cap)
KLEE: WARNING: killing 14838 states (over memory cap)
KLEE: WARNING: killing 15704 states (over memory cap)
KLEE: WARNING: killing 15134 states (over memory cap)
KLEE: WARNING: killing 14998 states (over memory cap)
KLEE: WARNING: killing 16313 states (over memory cap)
KLEE: WARNING: killing 16080 states (over memory cap)
KLEE: WARNING: killing 16062 states (over memory cap)
KLEE: WARNING: killing 15710 states (over memory cap)
KLEE: WARNING: killing 15798 states (over memory cap)
KLEE: WARNING: killing 15342 states (over memory cap)
KLEE: WARNING: killing 15982 states (over memory cap)
KLEE: WARNING: killing 15633 states (over memory cap)
KLEE: WARNING: killing 15732 states (over memory cap)
KLEE: WARNING: killing 15382 states (over memory cap)
KLEE: WARNING: killing 15469 states (over memory cap)
KLEE: WARNING: killing 15238 states (over memory cap)
KLEE: WARNING: killing 15107 states (over memory cap)
KLEE: WARNING: killing 15087 states (over memory cap)
KLEE: WARNING: killing 15946 states (over memory cap)
KLEE: WARNING: killing 16146 states (over memory cap)
KLEE: WARNING: killing 15260 states (over memory cap)
KLEE: WARNING: killing 15896 states (over memory cap)
KLEE: WARNING: killing 15661 states (over memory cap)
KLEE: WARNING: killing 15539 states (over memory cap)
KLEE: WARNING: killing 15305 states (over memory cap)
KLEE: WARNING: killing 15716 states (over memory cap)
KLEE: WARNING: killing 15268 states (over memory cap)
KLEE: WARNING: killing 15789 states (over memory cap)
KLEE: WARNING: killing 16536 states (over memory cap)
KLEE: WARNING: killing 15326 states (over memory cap)
KLEE: WARNING: killing 14769 states (over memory cap)
KLEE: WARNING: killing 14640 states (over memory cap)
KLEE: WARNING: killing 15595 states (over memory cap)
KLEE: WARNING: killing 15037 states (over memory cap)
KLEE: WARNING: killing 15342 states (over memory cap)
KLEE: WARNING: killing 15325 states (over memory cap)
KLEE: WARNING: killing 15628 states (over memory cap)
KLEE: WARNING: killing 15613 states (over memory cap)
KLEE: WARNING: killing 16670 states (over memory cap)
KLEE: WARNING: killing 15801 states (over memory cap)
KLEE: WARNING: killing 15460 states (over memory cap)
KLEE: WARNING: killing 15767 states (over memory cap)
KLEE: WARNING: killing 15749 states (over memory cap)
KLEE: WARNING: killing 15516 states (over memory cap)
KLEE: WARNING: killing 15504 states (over memory cap)
KLEE: WARNING: killing 15059 states (over memory cap)
KLEE: WARNING: killing 15894 states (over memory cap)
KLEE: WARNING: killing 15459 states (over memory cap)
KLEE: WARNING: killing 15655 states (over memory cap)
KLEE: WARNING: killing 15320 states (over memory cap)
KLEE: WARNING: killing 16035 states (over memory cap)
KLEE: WARNING: killing 15390 states (over memory cap)
KLEE: WARNING: killing 15160 states (over memory cap)
KLEE: WARNING: killing 15354 states (over memory cap)
KLEE: WARNING: killing 15971 states (over memory cap)
KLEE: WARNING: killing 16164 states (over memory cap)
KLEE: WARNING: killing 15832 states (over memory cap)
KLEE: WARNING: killing 15924 states (over memory cap)
KLEE: WARNING: killing 15698 states (over memory cap)
KLEE: WARNING: killing 15161 states (over memory cap)
KLEE: WARNING: killing 15350 states (over memory cap)
KLEE: WARNING: killing 15753 states (over memory cap)
KLEE: WARNING: killing 15834 states (over memory cap)
KLEE: WARNING: killing 15821 states (over memory cap)
KLEE: WARNING: killing 15497 states (over memory cap)
KLEE: WARNING: killing 16322 states (over memory cap)
KLEE: WARNING: killing 15786 states (over memory cap)
KLEE: WARNING: killing 15353 states (over memory cap)
KLEE: WARNING: killing 15545 states (over memory cap)
KLEE: WARNING: killing 15530 states (over memory cap)
KLEE: WARNING: killing 15097 states (over memory cap)
KLEE: WARNING: killing 16324 states (over memory cap)
KLEE: WARNING: killing 15377 states (over memory cap)
KLEE: WARNING: killing 15774 states (over memory cap)
KLEE: WARNING: killing 15031 states (over memory cap)
KLEE: WARNING: killing 15123 states (over memory cap)
KLEE: WARNING: killing 16036 states (over memory cap)
KLEE: WARNING: killing 15500 states (over memory cap)
KLEE: WARNING: killing 15385 states (over memory cap)
KLEE: WARNING: killing 15685 states (over memory cap)
KLEE: WARNING: killing 15665 states (over memory cap)
KLEE: WARNING: killing 15345 states (over memory cap)
KLEE: WARNING: killing 15533 states (over memory cap)
KLEE: WARNING: killing 15614 states (over memory cap)
KLEE: WARNING: killing 15600 states (over memory cap)
KLEE: WARNING: killing 15077 states (over memory cap)
KLEE: WARNING: killing 15979 states (over memory cap)
KLEE: WARNING: killing 16165 states (over memory cap)
KLEE: WARNING: killing 15748 states (over memory cap)
KLEE: WARNING: killing 16142 states (over memory cap)
KLEE: WARNING: killing 16029 states (over memory cap)
KLEE: WARNING: killing 16110 states (over memory cap)
KLEE: WARNING: killing 14879 states (over memory cap)
KLEE: WARNING: killing 15373 states (over memory cap)
KLEE: WARNING: killing 15862 states (over memory cap)
KLEE: WARNING: killing 15447 states (over memory cap)
KLEE: WARNING: killing 15633 states (over memory cap)
KLEE: WARNING: killing 15620 states (over memory cap)
KLEE: WARNING: killing 15098 states (over memory cap)
KLEE: WARNING: killing 15182 states (over memory cap)
KLEE: WARNING: killing 15980 states (over memory cap)
KLEE: WARNING: killing 15055 states (over memory cap)
KLEE: WARNING: killing 14742 states (over memory cap)
KLEE: WARNING: killing 15028 states (over memory cap)
KLEE: WARNING: killing 15818 states (over memory cap)
KLEE: WARNING: killing 16408 states (over memory cap)
KLEE: WARNING: killing 15899 states (over memory cap)
KLEE: WARNING: killing 15581 states (over memory cap)
KLEE: WARNING: killing 15565 states (over memory cap)
KLEE: WARNING: killing 14954 states (over memory cap)
KLEE: WARNING: killing 15437 states (over memory cap)
KLEE: WARNING: killing 15726 states (over memory cap)
KLEE: WARNING: killing 15510 states (over memory cap)
KLEE: WARNING: killing 15190 states (over memory cap)
KLEE: WARNING: killing 15577 states (over memory cap)
KLEE: WARNING: killing 14172 states (over memory cap)
KLEE: WARNING: killing 15447 states (over memory cap)
KLEE: WARNING: killing 15338 states (over memory cap)
KLEE: WARNING: killing 15926 states (over memory cap)
KLEE: WARNING: killing 15816 states (over memory cap)
KLEE: WARNING: killing 15500 states (over memory cap)
KLEE: WARNING: killing 15984 states (over memory cap)
KLEE: WARNING: killing 16067 states (over memory cap)
KLEE: WARNING: killing 15561 states (over memory cap)
KLEE: WARNING: killing 15444 states (over memory cap)
KLEE: WARNING: killing 15138 states (over memory cap)
KLEE: WARNING: killing 15715 states (over memory cap)
KLEE: WARNING: killing 15601 states (over memory cap)
KLEE: WARNING: killing 15988 states (over memory cap)
KLEE: WARNING: killing 16171 states (over memory cap)
KLEE: WARNING: killing 14577 states (over memory cap)
KLEE: WARNING: killing 15840 states (over memory cap)
KLEE: WARNING: killing 14458 states (over memory cap)
KLEE: WARNING: killing 14934 states (over memory cap)
KLEE: WARNING: killing 15209 states (over memory cap)
KLEE: WARNING: killing 15689 states (over memory cap)
KLEE: WARNING: killing 15483 states (over memory cap)
KLEE: WARNING: killing 16250 states (over memory cap)
KLEE: WARNING: killing 15554 states (over memory cap)
KLEE: WARNING: killing 16319 states (over memory cap)
KLEE: WARNING: killing 16112 states (over memory cap)
KLEE: WARNING: killing 14929 states (over memory cap)
KLEE: WARNING: killing 16087 states (over memory cap)
KLEE: WARNING: killing 15490 states (over memory cap)
KLEE: WARNING: killing 15482 states (over memory cap)
