bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-commit-tester/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.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.: 192 262 3851 22592
INFO: Compilation, preparation and instrumentation time: 0.637022018433
Removed calls to 'add_timer' (function is undefined)
Defining function no_llseek as symbolic
Removed calls to '_lock_kernel' (function is undefined)
Removed calls to '_unlock_kernel' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'interruptible_sleep_on' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function printk as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'free_pages' (function is undefined)
Defining function __phys_addr as symbolic
Defining function interruptible_sleep_on_timeout as symbolic
Defining function del_timer_sync as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function del_timer as symbolic
Defining function __request_module as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function __get_free_pages as symbolic
Defining function vmalloc as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function remap_pfn_range as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function strlcpy as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function copy_user_generic_unrolled as symbolic
Defining function copy_user_generic_string as symbolic
Removed calls to 'unregister_sound_dsp' (function is undefined)
Removed calls to 'panic' (function is undefined)
Defining function register_sound_dsp as symbolic
Defining function register_sound_mixer as symbolic
Defining function register_sound_midi as symbolic
Removed calls to 'unregister_sound_mixer' (function is undefined)
Removed calls to 'unregister_sound_midi' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function mutex_trylock as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function request_dma as symbolic
Removed calls to 'free_dma' (function is undefined)
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'unregister_sound_special' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Defining function device_create as symbolic
Defining function register_sound_special as symbolic
Removed calls to 'schedule' (function is undefined)
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  __memcpy
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.629353046417
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 278 216 2039 12898
INFO: Starting verification
KLEE: WARNING ONCE: function "def_tmr_ioctl" has inline asm
KLEE: WARNING ONCE: function "sound_ioctl" has inline asm
KLEE: WARNING ONCE: function "sequencer_release" has inline asm
KLEE: WARNING ONCE: function "MIDIbuf_release" has inline asm
KLEE: WARNING ONCE: function "DMAbuf_release" has inline asm
KLEE: WARNING ONCE: function "DMAbuf_sync" has inline asm
KLEE: WARNING ONCE: function "close_dmap" has inline asm
KLEE: WARNING ONCE: function "sound_free_dmap" has inline asm
KLEE: WARNING ONCE: function "dma_reset_output" has inline asm
KLEE: WARNING ONCE: function "sound_start_dma" has inline asm
KLEE: WARNING ONCE: function "seq_sync" has inline asm
KLEE: WARNING ONCE: function "seq_drain_midi_queues" has inline asm
KLEE: WARNING ONCE: function "try_module_get" has inline asm
KLEE: WARNING ONCE: function "default_set_speed" has inline asm
KLEE: WARNING ONCE: function "default_set_bits" has inline asm
KLEE: WARNING ONCE: function "default_set_channels" has inline asm
KLEE: WARNING ONCE: function "sound_alloc_dmap" has inline asm
KLEE: WARNING ONCE: function "sound_mixer_ioctl" has inline asm
KLEE: WARNING ONCE: function "sequencer_ioctl" has inline asm
KLEE: WARNING ONCE: function "audio_ioctl" has inline asm
KLEE: WARNING ONCE: function "MIDIbuf_ioctl" has inline asm
KLEE: WARNING ONCE: function "dma_ioctl" has inline asm
KLEE: WARNING ONCE: function "DMAbuf_get_buffer_pointer" has inline asm
KLEE: WARNING ONCE: function "MIDIbuf_write" has inline asm
KLEE: WARNING ONCE: function "DMAbuf_getwrbuffer" has inline asm
KLEE: WARNING ONCE: function "MIDIbuf_read" has inline asm
KLEE: WARNING ONCE: function "timer_ioctl" has inline asm
KLEE: WARNING ONCE: function "DMAbuf_outputintr" has inline asm
KLEE: WARNING ONCE: function "DMAbuf_inputintr" has inline asm
KLEE: WARNING ONCE: function "midi_synth_ioctl" has inline asm
KLEE: WARNING ONCE: function "midi_synth_load_patch" has inline asm
KLEE: WARNING: undefined reference to variable: boot_tvec_bases
KLEE: WARNING: Type for boot_tvec_bases is not sized
KLEE: WARNING: Unable to find size for global variable: boot_tvec_bases (use will result in out of bounds access)
KLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash: MO95[8192] allocated at global:sound_mem_blocks
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:4416: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:4448: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:4448: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:4416: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:3345: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:4280: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:4280: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:4416: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3IvjsT/main1_true-unreach-call_sound-oss-sound-ko--32_7a--c4cb1dd.c:4448: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
