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-drivers--staging--bcm--bcm_wimax.ko-main.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.: 1339 544 13753 79808
INFO: Compilation, preparation and instrumentation time: 2.29960298538
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 'usb_deregister' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Defining function ldv_usbbcm_driver_reset_resume_4 as symbolic
Defining function ldv_bcmNetDevOps_ndo_init_3 as symbolic
Defining function ldv_bcmNetDevOps_ndo_uninit_3 as symbolic
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: 2.82214903831
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1497 464 8829 49942
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: ERROR: /tmp/symbiotic-jUtddy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--staging--bcm--bcm_wimax.ko-main.cil.out.c:17374: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jUtddy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--staging--bcm--bcm_wimax.ko-main.cil.out.c:17397: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jUtddy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--staging--bcm--bcm_wimax.ko-main.cil.out.c:17435: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jUtddy/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--staging--bcm--bcm_wimax.ko-main.cil.out.c:8177: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9198 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 10979 states (over memory cap)
KLEE: WARNING: killing 10399 states (over memory cap)
KLEE: WARNING: killing 10292 states (over memory cap)
KLEE: WARNING: killing 10105 states (over memory cap)
KLEE: WARNING: killing 10154 states (over memory cap)
KLEE: WARNING: killing 10204 states (over memory cap)
KLEE: WARNING: killing 10640 states (over memory cap)
KLEE: WARNING: killing 10386 states (over memory cap)
KLEE: WARNING: killing 10510 states (over memory cap)
KLEE: WARNING: killing 10718 states (over memory cap)
KLEE: WARNING: killing 11004 states (over memory cap)
KLEE: WARNING: killing 10984 states (over memory cap)
KLEE: WARNING: killing 10805 states (over memory cap)
KLEE: WARNING: killing 10786 states (over memory cap)
KLEE: WARNING: killing 10762 states (over memory cap)
KLEE: WARNING: killing 11051 states (over memory cap)
KLEE: WARNING: killing 11034 states (over memory cap)
KLEE: WARNING: killing 11317 states (over memory cap)
KLEE: WARNING: killing 10996 states (over memory cap)
KLEE: WARNING: killing 10977 states (over memory cap)
KLEE: WARNING: killing 10807 states (over memory cap)
KLEE: WARNING: killing 11013 states (over memory cap)
KLEE: WARNING: killing 10772 states (over memory cap)
KLEE: WARNING: killing 10749 states (over memory cap)
KLEE: WARNING: killing 10957 states (over memory cap)
KLEE: WARNING: killing 10263 states (over memory cap)
KLEE: WARNING: killing 10316 states (over memory cap)
KLEE: WARNING: killing 10375 states (over memory cap)
KLEE: WARNING: killing 10727 states (over memory cap)
KLEE: WARNING: killing 10417 states (over memory cap)
KLEE: WARNING: killing 10771 states (over memory cap)
KLEE: WARNING: killing 10602 states (over memory cap)
KLEE: WARNING: killing 11035 states (over memory cap)
KLEE: WARNING: killing 10500 states (over memory cap)
KLEE: WARNING: killing 10633 states (over memory cap)
KLEE: WARNING: killing 10692 states (over memory cap)
KLEE: WARNING: killing 10231 states (over memory cap)
KLEE: WARNING: killing 10730 states (over memory cap)
KLEE: WARNING: killing 10715 states (over memory cap)
KLEE: WARNING: killing 10627 states (over memory cap)
KLEE: WARNING: killing 10754 states (over memory cap)
KLEE: WARNING: killing 10522 states (over memory cap)
KLEE: WARNING: killing 11094 states (over memory cap)
KLEE: WARNING: killing 10563 states (over memory cap)
KLEE: WARNING: killing 10693 states (over memory cap)
KLEE: WARNING: killing 10460 states (over memory cap)
KLEE: WARNING: killing 10669 states (over memory cap)
KLEE: WARNING: killing 10795 states (over memory cap)
KLEE: WARNING: killing 10560 states (over memory cap)
KLEE: WARNING: killing 10546 states (over memory cap)
KLEE: WARNING: killing 10314 states (over memory cap)
KLEE: WARNING: killing 10731 states (over memory cap)
KLEE: WARNING: killing 10575 states (over memory cap)
KLEE: WARNING: killing 10558 states (over memory cap)
KLEE: WARNING: killing 10255 states (over memory cap)
KLEE: WARNING: killing 10603 states (over memory cap)
KLEE: WARNING: killing 10943 states (over memory cap)
KLEE: WARNING: killing 10502 states (over memory cap)
KLEE: WARNING: killing 10489 states (over memory cap)
KLEE: WARNING: killing 10332 states (over memory cap)
KLEE: WARNING: killing 10318 states (over memory cap)
KLEE: WARNING: killing 10451 states (over memory cap)
KLEE: WARNING: killing 10577 states (over memory cap)
KLEE: WARNING: killing 10777 states (over memory cap)
KLEE: WARNING: killing 10626 states (over memory cap)
KLEE: WARNING: killing 10682 states (over memory cap)
KLEE: WARNING: killing 10453 states (over memory cap)
KLEE: WARNING: killing 11011 states (over memory cap)
KLEE: WARNING: killing 10783 states (over memory cap)
KLEE: WARNING: killing 10698 states (over memory cap)
KLEE: WARNING: killing 10402 states (over memory cap)
KLEE: WARNING: killing 10817 states (over memory cap)
KLEE: WARNING: killing 10451 states (over memory cap)
KLEE: WARNING: killing 10647 states (over memory cap)
KLEE: WARNING: killing 10351 states (over memory cap)
KLEE: WARNING: killing 10480 states (over memory cap)
KLEE: WARNING: killing 10603 states (over memory cap)
KLEE: WARNING: killing 10451 states (over memory cap)
KLEE: WARNING: killing 10159 states (over memory cap)
KLEE: WARNING: killing 10283 states (over memory cap)
KLEE: WARNING: killing 10477 states (over memory cap)
KLEE: WARNING: killing 10740 states (over memory cap)
KLEE: WARNING: killing 10799 states (over memory cap)
KLEE: WARNING: killing 10713 states (over memory cap)
KLEE: WARNING: killing 10357 states (over memory cap)
KLEE: WARNING: killing 10623 states (over memory cap)
KLEE: WARNING: killing 10468 states (over memory cap)
KLEE: WARNING: killing 10665 states (over memory cap)
KLEE: WARNING: killing 10515 states (over memory cap)
KLEE: WARNING: killing 10435 states (over memory cap)
KLEE: WARNING: killing 10561 states (over memory cap)
KLEE: WARNING: killing 10689 states (over memory cap)
KLEE: WARNING: killing 10327 states (over memory cap)
KLEE: WARNING: killing 10727 states (over memory cap)
KLEE: WARNING: killing 10582 states (over memory cap)
KLEE: WARNING: killing 10502 states (over memory cap)
KLEE: WARNING: killing 10764 states (over memory cap)
KLEE: WARNING: killing 10823 states (over memory cap)
KLEE: WARNING: killing 10398 states (over memory cap)
KLEE: WARNING: killing 10383 states (over memory cap)
KLEE: WARNING: killing 10164 states (over memory cap)
KLEE: WARNING: killing 10491 states (over memory cap)
KLEE: WARNING: killing 10411 states (over memory cap)
KLEE: WARNING: killing 10602 states (over memory cap)
KLEE: WARNING: killing 10454 states (over memory cap)
KLEE: WARNING: killing 10374 states (over memory cap)
KLEE: WARNING: killing 10431 states (over memory cap)
KLEE: WARNING: killing 10620 states (over memory cap)
KLEE: WARNING: killing 10680 states (over memory cap)
KLEE: WARNING: killing 10873 states (over memory cap)
KLEE: WARNING: killing 10317 states (over memory cap)
KLEE: WARNING: killing 10710 states (over memory cap)
KLEE: WARNING: killing 10156 states (over memory cap)
KLEE: WARNING: killing 10615 states (over memory cap)
KLEE: WARNING: killing 10672 states (over memory cap)
KLEE: WARNING: killing 10658 states (over memory cap)
KLEE: WARNING: killing 10308 states (over memory cap)
KLEE: WARNING: killing 10704 states (over memory cap)
KLEE: WARNING: killing 10827 states (over memory cap)
KLEE: WARNING: killing 10878 states (over memory cap)
KLEE: WARNING: killing 10335 states (over memory cap)
KLEE: WARNING: killing 10588 states (over memory cap)
KLEE: WARNING: killing 10775 states (over memory cap)
KLEE: WARNING: killing 10435 states (over memory cap)
KLEE: WARNING: killing 10290 states (over memory cap)
KLEE: WARNING: killing 10609 states (over memory cap)
KLEE: WARNING: killing 10268 states (over memory cap)
KLEE: WARNING: killing 10456 states (over memory cap)
KLEE: WARNING: killing 10178 states (over memory cap)
KLEE: WARNING: killing 10562 states (over memory cap)
KLEE: WARNING: killing 10688 states (over memory cap)
KLEE: WARNING: killing 10684 states (over memory cap)
KLEE: WARNING: killing 10538 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10579 states (over memory cap)
KLEE: WARNING: killing 10367 states (over memory cap)
KLEE: WARNING: killing 10947 states (over memory cap)
KLEE: WARNING: killing 10608 states (over memory cap)
KLEE: WARNING: killing 10596 states (over memory cap)
KLEE: WARNING: killing 10518 states (over memory cap)
KLEE: WARNING: killing 10706 states (over memory cap)
KLEE: WARNING: killing 10629 states (over memory cap)
KLEE: WARNING: killing 10680 states (over memory cap)
KLEE: WARNING: killing 10540 states (over memory cap)
KLEE: WARNING: killing 10134 states (over memory cap)
KLEE: WARNING: killing 10320 states (over memory cap)
KLEE: WARNING: killing 10697 states (over memory cap)
KLEE: WARNING: killing 10363 states (over memory cap)
KLEE: WARNING: killing 10607 states (over memory cap)
KLEE: WARNING: killing 10531 states (over memory cap)
KLEE: WARNING: killing 10778 states (over memory cap)
KLEE: WARNING: killing 10444 states (over memory cap)
KLEE: WARNING: killing 10756 states (over memory cap)
KLEE: WARNING: killing 10553 states (over memory cap)
KLEE: WARNING: killing 10609 states (over memory cap)
KLEE: WARNING: killing 10466 states (over memory cap)
KLEE: WARNING: killing 10585 states (over memory cap)
KLEE: WARNING: killing 10379 states (over memory cap)
KLEE: WARNING: killing 10555 states (over memory cap)
KLEE: WARNING: killing 10676 states (over memory cap)
KLEE: WARNING: killing 10344 states (over memory cap)
KLEE: WARNING: killing 10590 states (over memory cap)
KLEE: WARNING: killing 10900 states (over memory cap)
KLEE: WARNING: killing 10441 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 10291 states (over memory cap)
KLEE: WARNING: killing 10531 states (over memory cap)
KLEE: WARNING: killing 10454 states (over memory cap)
KLEE: WARNING: killing 10316 states (over memory cap)
KLEE: WARNING: killing 10495 states (over memory cap)
KLEE: WARNING: killing 10488 states (over memory cap)
KLEE: WARNING: killing 10476 states (over memory cap)
KLEE: WARNING: killing 10211 states (over memory cap)
KLEE: WARNING: killing 10514 states (over memory cap)
KLEE: WARNING: killing 10628 states (over memory cap)
KLEE: WARNING: killing 10744 states (over memory cap)
KLEE: WARNING: killing 10671 states (over memory cap)
KLEE: WARNING: killing 10533 states (over memory cap)
KLEE: WARNING: killing 10589 states (over memory cap)
KLEE: WARNING: killing 10572 states (over memory cap)
KLEE: WARNING: killing 10437 states (over memory cap)
KLEE: WARNING: killing 10488 states (over memory cap)
KLEE: WARNING: killing 10481 states (over memory cap)
KLEE: WARNING: killing 10537 states (over memory cap)
KLEE: WARNING: killing 10654 states (over memory cap)
KLEE: WARNING: killing 10646 states (over memory cap)
KLEE: WARNING: killing 10631 states (over memory cap)
KLEE: WARNING: killing 10499 states (over memory cap)
KLEE: WARNING: killing 10737 states (over memory cap)
