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--comedi--drivers--ni_660x.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.: 134 99 621 3650
Removed infinite loop in ni_660x_write_register
Removed infinite loop in IOConfigReg
Removed infinite loop in ni_660x_read_register
Removed infinite loop in dma_select_bits
Removed infinite loop in dma_select_mask
Removed infinite loop in ni_660x_request_mite_channel
Removed infinite loop in dma_selection_counter
Removed infinite loop in dma_reset_bit
Removed infinite loop in ni_gpct_to_660x_register
INFO: Compilation, preparation and instrumentation time: 0.219830036163
Removed calls to 'comedi_auto_unconfig' (function is undefined)
Removed calls to 'comedi_pci_driver_unregister' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'ni_gpct_device_destroy' (function is undefined)
Removed calls to 'mite_free_ring' (function is undefined)
Removed calls to 'mite_unsetup' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'ni_tio_init_counter' (function is undefined)
Defining function ldv_ni_660x_driver_release_2 as symbolic
Defining function ldv_ni_660x_driver_open_2 as symbolic
Defining function ldv_ni_660x_driver_close_2 as symbolic
Defining function ldv_ni_660x_driver_attach_2 as symbolic
Defining function ldv_ni_660x_driver_probe_2 as symbolic
Defining function mite_alloc as symbolic
Defining function mite_setup2 as symbolic
Defining function dev_warn as symbolic
Defining function comedi_alloc_subdevices as symbolic
Defining function ni_gpct_device_construct as symbolic
Removed calls to 'ni_tio_set_mite_channel' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'comedi_error' (function is undefined)
Removed calls to 'ni_tio_acknowledge_and_confirm' (function is undefined)
Removed calls to 'mite_release_channel' (function is undefined)
Removed calls to 'ni_tio_handle_interrupt' (function is undefined)
Removed calls to 'comedi_event' (function is undefined)
Defining function _dev_info as symbolic
Defining function request_threaded_irq as symbolic
Defining function _raw_spin_lock_irqsave as symbolic
Defining function mite_buf_change as symbolic
Defining function mite_sync_input_dma as symbolic
Defining function comedi_buf_read_n_available as symbolic
Defining function ni_tio_cancel as symbolic
Defining function ni_tio_cmdtest as symbolic
Defining function ni_tio_cmd as symbolic
Defining function mite_request_channel_in_range as symbolic
Defining function ni_tio_insn_config as symbolic
Defining function ni_tio_winsn as symbolic
Defining function ni_tio_rinsn as symbolic
Defining function mite_alloc_ring as symbolic
Defining function comedi_pci_driver_register as symbolic
Defining function comedi_auto_config as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.187288999557
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 192 92 410 2012
INFO: Starting verification
KLEE: WARNING ONCE: function "ni_660x_write_register" has inline asm
KLEE: WARNING ONCE: function "ni_660x_cmd" has inline asm
KLEE: WARNING ONCE: function "dma_select_bits" has inline asm
KLEE: WARNING ONCE: function "dma_select_mask" has inline asm
KLEE: WARNING ONCE: function "IOConfigReg" has inline asm
KLEE: WARNING ONCE: function "ni_660x_interrupt" has inline asm
KLEE: WARNING ONCE: function "ni_660x_read_register" has inline asm
KLEE: WARNING ONCE: function "ni_gpct_to_660x_register" has inline asm
KLEE: ERROR: /tmp/symbiotic-4GoPxr/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--staging--comedi--drivers--ni_660x.ko-main.cil.out.c:3544: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-4GoPxr/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--staging--comedi--drivers--ni_660x.ko-main.cil.out.c:5044: 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 16345 states (over memory cap)
KLEE: WARNING: killing 17095 states (over memory cap)
KLEE: WARNING: killing 16849 states (over memory cap)
KLEE: WARNING: killing 16898 states (over memory cap)
KLEE: WARNING: killing 16389 states (over memory cap)
KLEE: WARNING: killing 16437 states (over memory cap)
KLEE: WARNING: killing 16623 states (over memory cap)
KLEE: WARNING: killing 16821 states (over memory cap)
KLEE: WARNING: killing 16606 states (over memory cap)
KLEE: WARNING: killing 17075 states (over memory cap)
KLEE: WARNING: killing 17275 states (over memory cap)
KLEE: WARNING: killing 16926 states (over memory cap)
KLEE: WARNING: killing 17128 states (over memory cap)
KLEE: WARNING: killing 16922 states (over memory cap)
KLEE: WARNING: killing 17126 states (over memory cap)
KLEE: WARNING: killing 17328 states (over memory cap)
KLEE: WARNING: killing 17663 states (over memory cap)
KLEE: WARNING: killing 17331 states (over memory cap)
KLEE: WARNING: killing 17015 states (over memory cap)
KLEE: WARNING: killing 17210 states (over memory cap)
KLEE: WARNING: killing 17148 states (over memory cap)
KLEE: WARNING: killing 16955 states (over memory cap)
KLEE: WARNING: killing 17012 states (over memory cap)
KLEE: WARNING: killing 16821 states (over memory cap)
KLEE: WARNING: killing 17015 states (over memory cap)
KLEE: WARNING: killing 16823 states (over memory cap)
KLEE: WARNING: killing 16377 states (over memory cap)
KLEE: WARNING: killing 16827 states (over memory cap)
KLEE: WARNING: killing 16761 states (over memory cap)
KLEE: WARNING: killing 16573 states (over memory cap)
KLEE: WARNING: killing 16641 states (over memory cap)
KLEE: WARNING: killing 16709 states (over memory cap)
KLEE: WARNING: killing 16772 states (over memory cap)
KLEE: WARNING: killing 17211 states (over memory cap)
KLEE: WARNING: killing 16912 states (over memory cap)
KLEE: WARNING: killing 16986 states (over memory cap)
KLEE: WARNING: killing 16686 states (over memory cap)
KLEE: WARNING: killing 16506 states (over memory cap)
KLEE: WARNING: killing 16814 states (over memory cap)
KLEE: WARNING: killing 16880 states (over memory cap)
KLEE: WARNING: killing 16345 states (over memory cap)
KLEE: WARNING: killing 16781 states (over memory cap)
KLEE: WARNING: killing 16725 states (over memory cap)
KLEE: WARNING: killing 16790 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 16811 states (over memory cap)
KLEE: WARNING: killing 16521 states (over memory cap)
KLEE: WARNING: killing 16710 states (over memory cap)
KLEE: WARNING: killing 16658 states (over memory cap)
KLEE: WARNING: killing 16966 states (over memory cap)
KLEE: WARNING: killing 16677 states (over memory cap)
KLEE: WARNING: killing 16748 states (over memory cap)
KLEE: WARNING: killing 16455 states (over memory cap)
KLEE: WARNING: killing 16643 states (over memory cap)
KLEE: WARNING: killing 16834 states (over memory cap)
KLEE: WARNING: killing 16789 states (over memory cap)
KLEE: WARNING: killing 16392 states (over memory cap)
KLEE: WARNING: killing 16469 states (over memory cap)
KLEE: WARNING: killing 16534 states (over memory cap)
KLEE: WARNING: killing 16610 states (over memory cap)
KLEE: WARNING: killing 16676 states (over memory cap)
KLEE: WARNING: killing 16749 states (over memory cap)
KLEE: WARNING: killing 16351 states (over memory cap)
KLEE: WARNING: killing 16540 states (over memory cap)
KLEE: WARNING: killing 16491 states (over memory cap)
KLEE: WARNING: killing 16554 states (over memory cap)
KLEE: WARNING: killing 16408 states (over memory cap)
KLEE: WARNING: killing 16696 states (over memory cap)
KLEE: WARNING: killing 16765 states (over memory cap)
KLEE: WARNING: killing 16840 states (over memory cap)
KLEE: WARNING: killing 16570 states (over memory cap)
KLEE: WARNING: killing 16522 states (over memory cap)
KLEE: WARNING: killing 16587 states (over memory cap)
KLEE: WARNING: killing 16325 states (over memory cap)
KLEE: WARNING: killing 16283 states (over memory cap)
KLEE: WARNING: killing 16792 states (over memory cap)
KLEE: WARNING: killing 16534 states (over memory cap)
KLEE: WARNING: killing 16599 states (over memory cap)
KLEE: WARNING: killing 16556 states (over memory cap)
KLEE: WARNING: killing 16408 states (over memory cap)
KLEE: WARNING: killing 16699 states (over memory cap)
KLEE: WARNING: killing 16437 states (over memory cap)
KLEE: WARNING: killing 16602 states (over memory cap)
KLEE: WARNING: killing 16452 states (over memory cap)
KLEE: WARNING: killing 16413 states (over memory cap)
KLEE: WARNING: killing 16159 states (over memory cap)
KLEE: WARNING: killing 16448 states (over memory cap)
KLEE: WARNING: killing 16727 states (over memory cap)
KLEE: WARNING: killing 16580 states (over memory cap)
KLEE: WARNING: killing 16326 states (over memory cap)
KLEE: WARNING: killing 16598 states (over memory cap)
KLEE: WARNING: killing 16888 states (over memory cap)
KLEE: WARNING: killing 16964 states (over memory cap)
KLEE: WARNING: killing 16711 states (over memory cap)
KLEE: WARNING: killing 16768 states (over memory cap)
KLEE: WARNING: killing 16628 states (over memory cap)
