bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.0/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 42 64 780 4103
Removed infinite loop in ldv_assume_stop
INFO: Compilation, preparation and instrumentation time: 0.243208885193
Defining function printk as symbolic
Defining function usb_register_driver as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Defining function dev_set_drvdata as symbolic
Defining function dev_get_drvdata as symbolic
Defining function usb_set_interface as symbolic
Defining function alloc_etherdev_mqs as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Defining function dev_warn as symbolic
Defining function register_netdev as symbolic
Defining function crc32_le as symbolic
Defining function usb_control_msg as symbolic
Defining function usb_submit_urb as symbolic
Defining function dev_alloc_skb as symbolic
Defining function skb_put as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_rx as symbolic
Removed calls to '__netif_schedule' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function netpoll_trap as symbolic
Defining function ldv_undefined_pointer as symbolic
Defining function mod_timer as symbolic
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Defining function eth_mac_addr as symbolic
Defining function eth_validate_addr as symbolic
Defining function eth_change_mtu as symbolic
Defining function usb_unlink_urb as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function snprintf as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Linked our definitions to these undefined functions:
  strncpy
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.182463884354
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 93 61 315 2401
INFO: Starting verification
KLEE: WARNING ONCE: function "catc_ctrl_done" has inline asm
KLEE: WARNING ONCE: function "catc_tx_done" has inline asm
KLEE: WARNING ONCE: function "catc_rx_done" has inline asm
KLEE: WARNING ONCE: function "catc_irq_done" has inline asm
KLEE: WARNING ONCE: function "netif_wake_queue" has inline asm
KLEE: WARNING ONCE: function "catc_ctrl_async" has inline asm
KLEE: WARNING ONCE: function "catc_open" has inline asm
KLEE: WARNING ONCE: function "catc_start_xmit" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6200: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6206: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6206: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6207: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5734: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5e9e6ffa-501a-4a5f-9f92-bcc3e12a1acd/symbiotic/lib/libc/strncpy.c:9: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5e9e6ffa-501a-4a5f-9f92-bcc3e12a1acd/symbiotic/lib/libc/strncpy.c:9: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6277: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:4922: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6277: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:4923: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5664: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5956: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5957: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5958: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5666: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5959: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5e9e6ffa-501a-4a5f-9f92-bcc3e12a1acd/symbiotic/lib/libc/strncpy.c:11: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5960: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5961: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5092: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6390: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5962: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:5963: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6390: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:4741: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6412: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6412: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6413: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-699yHb/usb_urb-drivers-net-usb-catc.ko_false-unreach-call.cil.out.i.pp.i:6415: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
