bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-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.: 448 493 5187 31979
Removed infinite loop in gpioirq
Removed infinite loop in dvb_get_stc
Removed infinite loop in dma_sync_sg_for_cpu
Removed infinite loop in OSDSetBlock
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.29217290878
Defining function printk as symbolic
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_arg' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function saa7146_wait_for_debi_done as symbolic
Defining function mutex_lock_interruptible as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'dvb_ringbuffer_flush_spinlock_wakeup' (function is undefined)
Defining function dvb_filter_get_ac3info as symbolic
Defining function dvb_ringbuffer_free as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function noop_llseek as symbolic
Defining function dvb_generic_ioctl as symbolic
Defining function dvb_generic_release as symbolic
Defining function dvb_generic_open as symbolic
Defining function i2c_transfer as symbolic
Defining function dvb_ringbuffer_write as symbolic
Defining function default_llseek as symbolic
Removed calls to 'free_pages' (function is undefined)
Defining function dvb_ringbuffer_empty as symbolic
Defining function __get_free_pages as symbolic
Defining function dvb_ringbuffer_avail as symbolic
Defining function dvb_ringbuffer_read_user as symbolic
Removed calls to 'release_firmware' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'saa7146_setgpio' (function is undefined)
Removed calls to 'dvb_frontend_detach' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'saa7146_vfree_destroy_pgtable' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'input_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 'dvb_unregister_device' (function is undefined)
Defining function dvb_unregister_adapter as symbolic
Defining function dvb_unregister_frontend as symbolic
Defining function kthread_stop as symbolic
Defining function saa7146_unregister_device as symbolic
Defining function saa7146_vv_release as symbolic
Defining function del_timer_sync as symbolic
Defining function dvb_register_adapter as symbolic
Defining function strlcpy as symbolic
Defining function saa7146_i2c_adapter_prepare as symbolic
Defining function i2c_add_adapter as symbolic
Defining function ttpci_eeprom_parse_mac as symbolic
Defining function saa7146_vmalloc_build_pgtable as symbolic
Removed calls to 'debug_dma_sync_sg_for_cpu' (function is undefined)
Removed calls to 'dvb_dmx_swfilter_packets' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'dvb_ringbuffer_read' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function vmalloc as symbolic
Removed calls to 'dvb_ringbuffer_init' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Removed calls to 'input_free_device' (function is undefined)
Removed calls to 'proc_set_size' (function is undefined)
Removed calls to 'input_event' (function is undefined)
Defining function input_allocate_device as symbolic
Defining function snprintf as symbolic
Defining function input_register_device as symbolic
Removed calls to 'add_timer' (function is undefined)
Defining function del_timer as symbolic
Defining function proc_create_data as symbolic
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Defining function dvb_register_frontend as symbolic
Defining function saa7146_vv_init as symbolic
Removed calls to 'saa7146_set_hps_source_and_sync' (function is undefined)
Defining function saa7146_register_device as symbolic
Defining function saa7146_stop_preview as symbolic
Defining function saa7146_start_preview as symbolic
Defining function dvb_dmx_init as symbolic
Defining function dvb_dmxdev_init as symbolic
Defining function dvb_register_device as symbolic
Defining function dvb_net_init as symbolic
Removed calls to 'dvb_filter_pes2ts_init' (function is undefined)
Defining function kthread_should_stop as symbolic
Defining function schedule_timeout as symbolic
Defining function request_firmware as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function dvb_filter_pes2ts as symbolic
Defining function crc32_le as symbolic
Defining function strncpy_from_user as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Defining function ldv_release_3 as symbolic
Defining function ldv_open_3 as symbolic
Defining function ldv_close_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function saa7146_register_extension as symbolic
Defining function saa7146_unregister_extension as symbolic
Defining function ldv_open_2 as symbolic
Defining function ldv_release_2 as symbolic
Linked our definitions to these undefined functions:
  strcpy
  strlen
  __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: 1.15997505188
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 557 464 2980 17105
INFO: Starting verification
KLEE: WARNING ONCE: function "av7110_debiwrite" has inline asm
KLEE: WARNING ONCE: function "av7110_debiread" has inline asm
KLEE: WARNING ONCE: function "dvb_video_ioctl" has inline asm
KLEE: WARNING ONCE: function "dvb_video_write" has inline asm
KLEE: WARNING ONCE: function "dvb_audio_write" has inline asm
KLEE: WARNING ONCE: function "av7110_attach" has inline asm
KLEE: WARNING ONCE: function "av7110_detach" has inline asm
KLEE: WARNING ONCE: function "av7110_irq" has inline asm
KLEE: WARNING ONCE: function "SAA7146_IER_DISABLE" has inline asm
KLEE: WARNING ONCE: function "tasklet_schedule" has inline asm
KLEE: WARNING ONCE: function "av7110_bootarm" has inline asm
KLEE: WARNING ONCE: function "av7110_start_feed" has inline asm
KLEE: WARNING ONCE: function "av7110_stop_feed" has inline asm
KLEE: WARNING ONCE: function "dvb_get_stc" has inline asm
KLEE: WARNING ONCE: function "av7110_emit_keyup" has inline asm
KLEE: WARNING ONCE: function "input_register_keys" has inline asm
KLEE: WARNING ONCE: function "av7110_init_analog_module" has inline asm
KLEE: WARNING ONCE: function "SAA7146_IER_ENABLE" has inline asm
KLEE: WARNING ONCE: function "av7110_osd_cmd" 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_ee5f0a30-85b5-43fa-b787-a7bc048c7b30/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 19399 states (over memory cap)
KLEE: WARNING: killing 20589 states (over memory cap)
KLEE: WARNING: killing 19024 states (over memory cap)
KLEE: WARNING: killing 18366 states (over memory cap)
KLEE: WARNING: killing 18142 states (over memory cap)
KLEE: WARNING: killing 18713 states (over memory cap)
KLEE: WARNING: killing 17791 states (over memory cap)
KLEE: WARNING: killing 19150 states (over memory cap)
KLEE: WARNING: killing 18583 states (over memory cap)
KLEE: WARNING: killing 18368 states (over memory cap)
KLEE: WARNING: killing 20061 states (over memory cap)
KLEE: WARNING: killing 20369 states (over memory cap)
KLEE: WARNING: killing 21640 states (over memory cap)
KLEE: WARNING: killing 21343 states (over memory cap)
KLEE: WARNING: killing 22433 states (over memory cap)
KLEE: WARNING: killing 21622 states (over memory cap)
KLEE: WARNING: killing 22540 states (over memory cap)
KLEE: WARNING: killing 23118 states (over memory cap)
KLEE: WARNING: killing 21893 states (over memory cap)
KLEE: WARNING: killing 22464 states (over memory cap)
KLEE: WARNING: killing 22955 states (over memory cap)
KLEE: WARNING: killing 22239 states (over memory cap)
KLEE: WARNING: killing 22892 states (over memory cap)
KLEE: WARNING: killing 22953 states (over memory cap)
KLEE: WARNING: killing 21397 states (over memory cap)
KLEE: WARNING: killing 21971 states (over memory cap)
KLEE: WARNING: killing 22363 states (over memory cap)
KLEE: WARNING: killing 21906 states (over memory cap)
KLEE: WARNING: killing 21705 states (over memory cap)
KLEE: WARNING: killing 22704 states (over memory cap)
KLEE: WARNING: killing 20805 states (over memory cap)
KLEE: WARNING: killing 21279 states (over memory cap)
KLEE: WARNING: killing 21752 states (over memory cap)
KLEE: WARNING: killing 21977 states (over memory cap)
KLEE: WARNING: killing 21953 states (over memory cap)
KLEE: WARNING: killing 21760 states (over memory cap)
KLEE: WARNING: killing 20801 states (over memory cap)
KLEE: WARNING: killing 22543 states (over memory cap)
KLEE: WARNING: killing 22269 states (over memory cap)
KLEE: WARNING: killing 21313 states (over memory cap)
KLEE: WARNING: killing 23723 states (over memory cap)
KLEE: WARNING: killing 21604 states (over memory cap)
KLEE: WARNING: killing 21576 states (over memory cap)
KLEE: WARNING: killing 21966 states (over memory cap)
KLEE: WARNING: killing 21683 states (over memory cap)
KLEE: WARNING: killing 23326 states (over memory cap)
KLEE: WARNING: killing 21458 states (over memory cap)
KLEE: WARNING: killing 21676 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:19544: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22884 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:14635: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22708 states (over memory cap)
KLEE: WARNING: killing 22514 states (over memory cap)
KLEE: WARNING: killing 20824 states (over memory cap)
KLEE: WARNING: killing 20637 states (over memory cap)
KLEE: WARNING: killing 22752 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:14330: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22888 states (over memory cap)
KLEE: WARNING: killing 22204 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:15081: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:14384: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22264 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:14903: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21423 states (over memory cap)
KLEE: WARNING: killing 22211 states (over memory cap)
KLEE: WARNING: killing 22021 states (over memory cap)
KLEE: WARNING: killing 21921 states (over memory cap)
KLEE: WARNING: killing 22225 states (over memory cap)
KLEE: WARNING: killing 22276 states (over memory cap)
KLEE: WARNING: killing 21277 states (over memory cap)
KLEE: WARNING: killing 21745 states (over memory cap)
KLEE: WARNING: killing 21468 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:15142: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22099 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:14429: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:14464: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21507 states (over memory cap)
KLEE: WARNING: killing 22783 states (over memory cap)
KLEE: WARNING: killing 23013 states (over memory cap)
KLEE: WARNING: killing 21523 states (over memory cap)
KLEE: WARNING: killing 21905 states (over memory cap)
KLEE: WARNING: killing 22442 states (over memory cap)
KLEE: WARNING: killing 21852 states (over memory cap)
KLEE: WARNING: killing 22150 states (over memory cap)
KLEE: WARNING: killing 22293 states (over memory cap)
KLEE: WARNING: killing 21949 states (over memory cap)
KLEE: WARNING: killing 22646 states (over memory cap)
KLEE: WARNING: killing 22063 states (over memory cap)
KLEE: WARNING: killing 21562 states (over memory cap)
KLEE: WARNING: killing 21853 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:16331: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22391 states (over memory cap)
KLEE: WARNING: killing 22535 states (over memory cap)
KLEE: WARNING: killing 21471 states (over memory cap)
KLEE: WARNING: killing 22722 states (over memory cap)
KLEE: WARNING: killing 22067 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:16212: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 23161 states (over memory cap)
KLEE: WARNING: killing 21545 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:16182: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21838 states (over memory cap)
KLEE: WARNING: killing 22458 states (over memory cap)
KLEE: WARNING: killing 21635 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:11863: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 21921 states (over memory cap)
KLEE: WARNING: killing 21818 states (over memory cap)
KLEE: WARNING: killing 22897 states (over memory cap)
KLEE: WARNING: killing 23033 states (over memory cap)
KLEE: WARNING: killing 22143 states (over memory cap)
KLEE: WARNING: killing 21804 states (over memory cap)
KLEE: WARNING: killing 22105 states (over memory cap)
KLEE: WARNING: killing 21287 states (over memory cap)
KLEE: WARNING: killing 22519 states (over memory cap)
KLEE: WARNING: killing 22582 states (over memory cap)
KLEE: WARNING: killing 22260 states (over memory cap)
KLEE: WARNING: killing 21762 states (over memory cap)
KLEE: WARNING: killing 21974 states (over memory cap)
KLEE: WARNING: killing 21719 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-8LcJvF/linux-4.2-rc1.tar.xz-32_7a-drivers--media--pci--ttpci--dvb-ttpci.ko-entry_point_true-unreach-call.cil.out.c:18103: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 22710 states (over memory cap)
