bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--bcm--bcm_wimax.ko-ldv_main17_sequence_infinite_withcheck_stateful.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.: 1301 535 13714 79592
INFO: Compilation, preparation and instrumentation time: 2.62879014015
Defining function vfs_read as symbolic
Defining function printk as symbolic
Defining function usb_control_msg as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'usb_put_dev' (function is undefined)
Removed calls to 'pm_runtime_set_autosuspend_delay' (function is undefined)
Removed calls to 'usb_enable_autosuspend' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'usb_disable_autosuspend' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Defining function usb_submit_urb as symbolic
Defining function skb_put as symbolic
Defining function skb_pull as symbolic
Defining function skb_push as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_rx as symbolic
Defining function pskb_expand_head as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function dev_get_drvdata as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Defining function kthread_stop as symbolic
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Defining function _dev_info as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Defining function usb_reset_device as symbolic
Defining function dev_set_drvdata as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function dev_err as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Defining function device_init_wakeup as symbolic
Removed calls to 'usb_autopm_put_interface' (function is undefined)
Defining function usb_get_dev as symbolic
Defining function usb_set_interface as symbolic
Removed calls to 'do_gettimeofday' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Defining function device_create as symbolic
Defining function __register_chrdev as symbolic
Defining function vfs_llseek as symbolic
Defining function filp_close as symbolic
Defining function filp_open as symbolic
Removed calls to 'schedule' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'down' (function is undefined)
Removed calls to 'up' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function register_netdev as symbolic
Defining function kernel_read as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'print_hex_dump' (function is undefined)
Defining function skb_copy as symbolic
Defining function usb_clear_halt as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Defining function skb_clone as symbolic
Defining function down_trylock as symbolic
Defining function get_seconds as symbolic
Removed calls to 'sort' (function is undefined)
Defining function usb_autopm_get_interface as symbolic
Defining function usb_interrupt_msg as symbolic
Defining function usb_alloc_urb as symbolic
Defining function usb_alloc_coherent as symbolic
Removed calls to 'usb_free_coherent' (function is undefined)
Defining function schedule_work as symbolic
Defining function eth_mac_addr as symbolic
Defining function eth_validate_addr as symbolic
Defining function eth_change_mtu as symbolic
Defining function snprintf as symbolic
Defining function no_llseek as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Defining function nonseekable_open as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function memdup_user as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'ldv_check_return_value_probe' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function __class_create as symbolic
Defining function usb_register_driver as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 3.29656004906
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1475 454 8803 49830
INFO: Starting verification
KLEE: WARNING ONCE: function "InterfaceFileDownload" has inline asm
KLEE: WARNING ONCE: function "usbbcm_device_probe" has inline asm
KLEE: WARNING ONCE: function "InterfaceRx" has inline asm
KLEE: WARNING ONCE: function "read_bulk_callback" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "flush_all_queues" has inline asm
KLEE: WARNING ONCE: function "InterfaceFileReadbackFromChip" has inline asm
KLEE: WARNING ONCE: function "InterfaceTransmitPacket" has inline asm
KLEE: WARNING ONCE: function "control_packet_handler" has inline asm
KLEE: WARNING ONCE: function "tx_pkt_handler" has inline asm
KLEE: WARNING ONCE: function "LEDControlThread" has inline asm
KLEE: WARNING ONCE: function "LED_Blink" has inline asm
KLEE: WARNING ONCE: function "PruneQueueAllSF" has inline asm
KLEE: WARNING ONCE: function "CheckAndSendPacketFromIndex" has inline asm
KLEE: WARNING ONCE: function "SetupNextSend" has inline asm
KLEE: WARNING ONCE: function "SendControlPacket" has inline asm
KLEE: WARNING ONCE: function "CopyBufferToControlPacket" has inline asm
KLEE: WARNING ONCE: function "flush_queue" has inline asm
KLEE: WARNING ONCE: function "CmControlResponseMessage" has inline asm
KLEE: WARNING ONCE: function "LinkControlResponseMessage" has inline asm
KLEE: WARNING ONCE: function "SendIdleModeResponse" has inline asm
KLEE: WARNING ONCE: function "write_bulk_callback" has inline asm
KLEE: WARNING ONCE: function "bcm_open" has inline asm
KLEE: WARNING ONCE: function "bcm_transmit" has inline asm
KLEE: WARNING ONCE: function "bcm_char_read" has inline asm
KLEE: WARNING ONCE: function "bcm_char_ioctl" has inline asm
KLEE: WARNING ONCE: function "bcm_char_open" has inline asm
KLEE: WARNING ONCE: function "bcm_char_release" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-60bQXz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--bcm--bcm_wimax.ko-ldv_main17_sequence_infinite_withcheck_stateful.cil.out.c:23304: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-60bQXz/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--bcm--bcm_wimax.ko-ldv_main17_sequence_infinite_withcheck_stateful.cil.out.c:23513: 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 5822 states (over memory cap)
KLEE: WARNING: killing 4408 states (over memory cap)
KLEE: WARNING: killing 4408 states (over memory cap)
KLEE: WARNING: killing 6097 states (over memory cap)
KLEE: WARNING: killing 4398 states (over memory cap)
KLEE: WARNING: killing 5893 states (over memory cap)
KLEE: WARNING: killing 5519 states (over memory cap)
KLEE: WARNING: killing 4833 states (over memory cap)
KLEE: WARNING: killing 4487 states (over memory cap)
KLEE: WARNING: killing 4229 states (over memory cap)
KLEE: WARNING: killing 4065 states (over memory cap)
KLEE: WARNING: killing 4292 states (over memory cap)
KLEE: WARNING: killing 4165 states (over memory cap)
KLEE: WARNING: killing 4121 states (over memory cap)
KLEE: WARNING: killing 4079 states (over memory cap)
KLEE: WARNING: killing 4144 states (over memory cap)
KLEE: WARNING: killing 4098 states (over memory cap)
KLEE: WARNING: killing 3882 states (over memory cap)
KLEE: WARNING: killing 3988 states (over memory cap)
KLEE: WARNING: killing 3778 states (over memory cap)
KLEE: WARNING: killing 3563 states (over memory cap)
KLEE: WARNING: killing 3610 states (over memory cap)
KLEE: WARNING: killing 3547 states (over memory cap)
KLEE: WARNING: killing 4203 states (over memory cap)
KLEE: WARNING: killing 4025 states (over memory cap)
KLEE: WARNING: killing 4201 states (over memory cap)
KLEE: WARNING: killing 4205 states (over memory cap)
KLEE: WARNING: killing 4210 states (over memory cap)
KLEE: WARNING: killing 4088 states (over memory cap)
KLEE: WARNING: killing 4033 states (over memory cap)
KLEE: WARNING: killing 3767 states (over memory cap)
KLEE: WARNING: killing 3811 states (over memory cap)
KLEE: WARNING: killing 3661 states (over memory cap)
KLEE: WARNING: killing 3710 states (over memory cap)
KLEE: WARNING: killing 3697 states (over memory cap)
KLEE: WARNING: killing 3786 states (over memory cap)
KLEE: WARNING: killing 3348 states (over memory cap)
KLEE: WARNING: killing 3311 states (over memory cap)
KLEE: WARNING: killing 3523 states (over memory cap)
KLEE: WARNING: killing 3520 states (over memory cap)
KLEE: WARNING: killing 3613 states (over memory cap)
KLEE: WARNING: killing 3413 states (over memory cap)
KLEE: WARNING: killing 3307 states (over memory cap)
KLEE: WARNING: killing 3422 states (over memory cap)
KLEE: WARNING: killing 3199 states (over memory cap)
KLEE: WARNING: killing 3219 states (over memory cap)
KLEE: WARNING: killing 3505 states (over memory cap)
KLEE: WARNING: killing 3398 states (over memory cap)
KLEE: WARNING: killing 3355 states (over memory cap)
KLEE: WARNING: killing 3226 states (over memory cap)
KLEE: WARNING: killing 3377 states (over memory cap)
KLEE: WARNING: killing 3407 states (over memory cap)
KLEE: WARNING: killing 3367 states (over memory cap)
KLEE: WARNING: killing 3297 states (over memory cap)
KLEE: WARNING: killing 3360 states (over memory cap)
KLEE: WARNING: killing 3476 states (over memory cap)
KLEE: WARNING: killing 3249 states (over memory cap)
KLEE: WARNING: killing 3396 states (over memory cap)
KLEE: WARNING: killing 3424 states (over memory cap)
KLEE: WARNING: killing 3267 states (over memory cap)
KLEE: WARNING: killing 3384 states (over memory cap)
KLEE: WARNING: killing 3197 states (over memory cap)
KLEE: WARNING: killing 3344 states (over memory cap)
KLEE: WARNING: killing 3523 states (over memory cap)
KLEE: WARNING: killing 3393 states (over memory cap)
KLEE: WARNING: killing 3229 states (over memory cap)
KLEE: WARNING: killing 3258 states (over memory cap)
KLEE: WARNING: killing 3462 states (over memory cap)
KLEE: WARNING: killing 3308 states (over memory cap)
KLEE: WARNING: killing 3330 states (over memory cap)
KLEE: WARNING: killing 3264 states (over memory cap)
KLEE: WARNING: killing 3260 states (over memory cap)
KLEE: WARNING: killing 3165 states (over memory cap)
KLEE: WARNING: killing 3194 states (over memory cap)
KLEE: WARNING: killing 3125 states (over memory cap)
KLEE: WARNING: killing 3064 states (over memory cap)
KLEE: WARNING: killing 3268 states (over memory cap)
KLEE: WARNING: killing 3530 states (over memory cap)
KLEE: WARNING: killing 3221 states (over memory cap)
KLEE: WARNING: killing 3191 states (over memory cap)
KLEE: WARNING: killing 3275 states (over memory cap)
KLEE: WARNING: killing 3420 states (over memory cap)
KLEE: WARNING: killing 3205 states (over memory cap)
KLEE: WARNING: killing 3113 states (over memory cap)
KLEE: WARNING: killing 3073 states (over memory cap)
KLEE: WARNING: killing 3215 states (over memory cap)
KLEE: WARNING: killing 3127 states (over memory cap)
KLEE: WARNING: killing 3297 states (over memory cap)
