bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--isdn--hisax--hisax_st5481.ko-entry_point_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.: 170 148 1084 6849
Removed infinite loop in ldv_stop___0
Removed infinite loop in st5481_d_l2l1
Removed infinite loop in st5481_b_l2l1
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.331890821457
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'hisax_unregister' (function is undefined)
Defining function printk as symbolic
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'FsmInitTimer' (function is undefined)
Defining function hisax_register as symbolic
Defining function sprintf as symbolic
Defining function isdnhdlc_decode as symbolic
Defining function skb_put as symbolic
Defining function __netdev_alloc_skb as symbolic
Defining function usb_ifnum_to_if as symbolic
Defining function usb_altnum_to_altsetting as symbolic
Removed calls to 'dev_kfree_skb_any' (function is undefined)
Defining function isdnhdlc_encode as symbolic
Defining function skb_pull as symbolic
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function vsnprintf as symbolic
Defining function FsmEvent as symbolic
Defining function usb_reset_configuration as symbolic
Defining function usb_set_interface as symbolic
Removed calls to 'usb_reset_endpoint' (function is undefined)
Removed calls to 'isdnhdlc_out_init' (function is undefined)
Defining function usb_unlink_urb as symbolic
Removed calls to 'isdnhdlc_rcv_init' (function is undefined)
Removed calls to 'FsmChangeState' (function is undefined)
Removed calls to 'FsmDelTimer' (function is undefined)
Removed calls to 'FsmRestartTimer' (function is undefined)
Defining function usb_get_current_frame_number as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'FsmFree' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function FsmNew as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  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.331753015518
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 223 138 656 3732
INFO: Starting verification
KLEE: WARNING ONCE: function "usb_next_ctrl_msg" has inline asm
KLEE: WARNING ONCE: function "st5481_d_l2l1" has inline asm
KLEE: WARNING ONCE: function "st5481_b_l2l1" has inline asm
KLEE: WARNING ONCE: function "usb_b_out_complete" has inline asm
KLEE: WARNING ONCE: function "usb_b_out" has inline asm
KLEE: WARNING ONCE: function "usb_d_out_complete" has inline asm
KLEE: WARNING ONCE: function "usb_ctrl_complete" has inline asm
KLEE: WARNING ONCE: function "dout_start_xmit" has inline asm
KLEE: WARNING ONCE: function "usb_d_out" has inline asm
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_f3e39ed0-495a-4bef-b2b0-30057eb638ec/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wIIvvN/linux-3.12-rc1.tar.xz-144_2a-drivers--isdn--hisax--hisax_st5481.ko-entry_point_false-unreach-call.cil.out.c:5549: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wIIvvN/linux-3.12-rc1.tar.xz-144_2a-drivers--isdn--hisax--hisax_st5481.ko-entry_point_false-unreach-call.cil.out.c:6583: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wIIvvN/linux-3.12-rc1.tar.xz-144_2a-drivers--isdn--hisax--hisax_st5481.ko-entry_point_false-unreach-call.cil.out.c:6590: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-wIIvvN/linux-3.12-rc1.tar.xz-144_2a-drivers--isdn--hisax--hisax_st5481.ko-entry_point_false-unreach-call.cil.out.c:6590: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
