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--media--firewire--firedtv.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.: 132 229 1324 9770
Removed infinite loop in avc_tuner_dsd
INFO: Compilation, preparation and instrumentation time: 0.431921005249
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'input_event' (function is undefined)
Defining function schedule_work as symbolic
Defining function _dev_info as symbolic
Defining function dev_err as symbolic
Defining function printk as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Defining function fw_run_transaction as symbolic
Defining function crc32_be as symbolic
Defining function noop_llseek as symbolic
Defining function dvb_generic_ioctl as symbolic
Defining function dvb_generic_open as symbolic
Defining function dvb_generic_release as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function dev_get_drvdata as symbolic
Removed calls to 'dvb_unregister_device' (function is undefined)
Removed calls to 'dvb_net_release' (function is undefined)
Removed calls to 'dvb_dmxdev_release' (function is undefined)
Removed calls to 'dvb_dmx_release' (function is undefined)
Removed calls to 'input_unregister_device' (function is undefined)
Defining function cancel_work_sync as symbolic
Defining function dvb_unregister_frontend as symbolic
Defining function dvb_unregister_adapter as symbolic
Defining function dev_set_drvdata as symbolic
Defining function fw_csr_string as symbolic
Removed calls to 'input_free_device' (function is undefined)
Defining function dvb_register_adapter as symbolic
Defining function dvb_dmx_init as symbolic
Defining function dvb_dmxdev_init as symbolic
Defining function dvb_net_init as symbolic
Defining function dvb_register_frontend as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'fw_iso_buffer_destroy' (function is undefined)
Removed calls to 'fw_iso_context_destroy' (function is undefined)
Defining function fw_iso_context_stop as symbolic
Removed calls to 'dvb_dmx_swfilter_packets' (function is undefined)
Removed calls to 'fw_iso_context_queue_flush' (function is undefined)
Defining function fw_iso_context_create as symbolic
Defining function fw_iso_buffer_init as symbolic
Defining function fw_iso_context_start as symbolic
Defining function fw_iso_context_queue as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function input_allocate_device as symbolic
Defining function kmemdup as symbolic
Defining function input_register_device as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function mutex_trylock as symbolic
Removed calls to 'driver_unregister' (function is undefined)
Removed calls to 'fw_core_remove_address_handler' (function is undefined)
Defining function fw_core_add_address_handler as symbolic
Defining function driver_register as symbolic
Linked our definitions to these undefined functions:
  strcpy
  strlen
  strncmp
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.358879089355
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 178 219 954 5969
INFO: Starting verification
KLEE: WARNING ONCE: function "fdtv_register_rc" has inline asm
KLEE: WARNING ONCE: function "avc_write" has inline asm
KLEE: WARNING ONCE: function "fdtv_start_feed" has inline asm
KLEE: WARNING ONCE: function "fdtv_stop_feed" has inline asm
KLEE: WARNING ONCE: function "avc_tuner_dsd" has inline asm
KLEE: WARNING ONCE: function "add_pid_filter" has inline asm
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO45[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-FYhyPN/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--firewire--firedtv.ko-main.cil.out.c:9741: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-FYhyPN/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--firewire--firedtv.ko-main.cil.out.c:9742: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-FYhyPN/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--firewire--firedtv.ko-main.cil.out.c:8148: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-FYhyPN/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--firewire--firedtv.ko-main.cil.out.c:7439: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-FYhyPN/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--firewire--firedtv.ko-main.cil.out.c:9661: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-FYhyPN/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--firewire--firedtv.ko-main.cil.out.c:7439: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-FYhyPN/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--media--firewire--firedtv.ko-main.cil.out.c:9342: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
