bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-validator-v0.8/linux-stable-47dffc7-1-144_2a-drivers--net--usb--cdc-phonet.ko-entry_point_ldv-val-v0.8_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.: 45 85 477 2899
Removed infinite loop in ldv_stop
Removed infinite loop in __skb_pull
INFO: Compilation, preparation and instrumentation time: 0.186328887939
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'dev_kfree_skb_any' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function printk as symbolic
Removed calls to '__netif_schedule' (function is undefined)
Defining function netpoll_trap as symbolic
Defining function usb_set_interface as symbolic
Removed calls to 'put_page' (function is undefined)
Removed calls to 'skb_add_rx_frag' (function is undefined)
Defining function __phys_addr as symbolic
Defining function skb_put as symbolic
Defining function netif_rx as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function __alloc_pages_nodemask as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'usb_driver_release_interface' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Defining function usb_ifnum_to_if as symbolic
Defining function alloc_netdev_mqs as symbolic
Defining function usb_driver_claim_interface as symbolic
Defining function register_netdev as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function ldv_ndo_init_2 as symbolic
Defining function ldv_ndo_uninit_2 as symbolic
Defining function usb_register_driver 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.223288059235
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 105 77 283 1720
INFO: Starting verification
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "netif_wake_queue" has inline asm
KLEE: WARNING ONCE: function "rx_submit" has inline asm
KLEE: WARNING ONCE: function "rx_complete" has inline asm
KLEE: WARNING: undefined reference to function: free_netdev
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_dcfa762b-e1b8-4ee2-addd-1361f62ceda6/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-WpQdXf/linux-stable-47dffc7-1-144_2a-drivers--net--usb--cdc-phonet.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:6138: 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 11667 states (over memory cap)
KLEE: WARNING: killing 11499 states (over memory cap)
KLEE: WARNING: killing 11651 states (over memory cap)
KLEE: WARNING: killing 11284 states (over memory cap)
KLEE: WARNING: killing 11228 states (over memory cap)
KLEE: WARNING: killing 11175 states (over memory cap)
KLEE: WARNING: killing 11233 states (over memory cap)
KLEE: WARNING: killing 11806 states (over memory cap)
KLEE: WARNING: killing 12173 states (over memory cap)
KLEE: WARNING: killing 12029 states (over memory cap)
KLEE: WARNING: killing 11878 states (over memory cap)
KLEE: WARNING: killing 11826 states (over memory cap)
KLEE: WARNING: killing 12086 states (over memory cap)
KLEE: WARNING: killing 11947 states (over memory cap)
KLEE: WARNING: killing 12002 states (over memory cap)
KLEE: WARNING: killing 12261 states (over memory cap)
KLEE: WARNING: killing 12321 states (over memory cap)
KLEE: WARNING: killing 12579 states (over memory cap)
KLEE: WARNING: killing 12635 states (over memory cap)
KLEE: WARNING: killing 12286 states (over memory cap)
KLEE: WARNING: killing 12144 states (over memory cap)
KLEE: WARNING: killing 12096 states (over memory cap)
KLEE: WARNING: killing 12042 states (over memory cap)
KLEE: WARNING: killing 12500 states (over memory cap)
KLEE: WARNING: killing 12451 states (over memory cap)
KLEE: WARNING: killing 12506 states (over memory cap)
KLEE: WARNING: killing 12368 states (over memory cap)
KLEE: WARNING: killing 12227 states (over memory cap)
KLEE: WARNING: killing 12570 states (over memory cap)
KLEE: WARNING: killing 12532 states (over memory cap)
KLEE: WARNING: killing 12201 states (over memory cap)
KLEE: WARNING: killing 12445 states (over memory cap)
KLEE: WARNING: killing 12022 states (over memory cap)
KLEE: WARNING: killing 12365 states (over memory cap)
KLEE: WARNING: killing 12242 states (over memory cap)
KLEE: WARNING: killing 12300 states (over memory cap)
KLEE: WARNING: killing 12637 states (over memory cap)
KLEE: WARNING: killing 12412 states (over memory cap)
KLEE: WARNING: killing 12467 states (over memory cap)
KLEE: WARNING: killing 12330 states (over memory cap)
KLEE: WARNING: killing 12198 states (over memory cap)
KLEE: WARNING: killing 12348 states (over memory cap)
KLEE: WARNING: killing 12401 states (over memory cap)
KLEE: WARNING: killing 12170 states (over memory cap)
KLEE: WARNING: killing 12415 states (over memory cap)
KLEE: WARNING: killing 12383 states (over memory cap)
KLEE: WARNING: killing 12526 states (over memory cap)
KLEE: WARNING: killing 12398 states (over memory cap)
KLEE: WARNING: killing 12641 states (over memory cap)
KLEE: WARNING: killing 12053 states (over memory cap)
KLEE: WARNING: killing 12472 states (over memory cap)
KLEE: WARNING: killing 12253 states (over memory cap)
KLEE: WARNING: killing 12219 states (over memory cap)
KLEE: WARNING: killing 12094 states (over memory cap)
KLEE: WARNING: killing 8882 states (over memory cap)
KLEE: WARNING: killing 11862 states (over memory cap)
KLEE: WARNING: killing 12279 states (over memory cap)
KLEE: WARNING: killing 12336 states (over memory cap)
KLEE: WARNING: killing 8969 states (over memory cap)
KLEE: WARNING: killing 11838 states (over memory cap)
KLEE: WARNING: killing 11987 states (over memory cap)
KLEE: WARNING: killing 8733 states (over memory cap)
KLEE: WARNING: killing 12025 states (over memory cap)
KLEE: WARNING: killing 12080 states (over memory cap)
KLEE: WARNING: killing 12048 states (over memory cap)
KLEE: WARNING: killing 8909 states (over memory cap)
KLEE: WARNING: killing 11736 states (over memory cap)
KLEE: WARNING: killing 8789 states (over memory cap)
KLEE: WARNING: killing 11862 states (over memory cap)
KLEE: WARNING: killing 8664 states (over memory cap)
KLEE: WARNING: killing 11902 states (over memory cap)
KLEE: WARNING: killing 8630 states (over memory cap)
KLEE: WARNING: killing 11765 states (over memory cap)
KLEE: WARNING: killing 8510 states (over memory cap)
KLEE: WARNING: killing 11542 states (over memory cap)
KLEE: WARNING: killing 8812 states (over memory cap)
KLEE: WARNING: killing 11752 states (over memory cap)
KLEE: WARNING: killing 8782 states (over memory cap)
KLEE: WARNING: killing 8433 states (over memory cap)
KLEE: WARNING: killing 11446 states (over memory cap)
KLEE: WARNING: killing 8736 states (over memory cap)
KLEE: WARNING: killing 8387 states (over memory cap)
KLEE: WARNING: killing 11381 states (over memory cap)
KLEE: WARNING: killing 8770 states (over memory cap)
KLEE: WARNING: killing 11413 states (over memory cap)
KLEE: WARNING: killing 8645 states (over memory cap)
KLEE: WARNING: killing 8305 states (over memory cap)
KLEE: WARNING: killing 8373 states (over memory cap)
