bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-validator-v0.8/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_ldv-val-v0.8_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.: 204 313 4129 23733
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.747730016708
Removed calls to 'add_timer' (function is undefined)
Defining function no_llseek as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'mutex_lock' (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 'mutex_unlock' (function is undefined)
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 debug_lockdep_rcu_enabled as symbolic
Defining function vmalloc 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)
Defining function mutex_trylock as symbolic
Defining function request_dma as symbolic
Removed calls to 'free_dma' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'unregister_sound_special' (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
  __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.828972101212
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 290 268 2200 13528
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 "sound_open" 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___0" 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: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_a667e9e9-f01f-4e50-bbcc-45c2dbfd4f5b/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3of6Q6/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4159: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3of6Q6/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4553: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3of6Q6/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4521: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3of6Q6/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:4213: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3of6Q6/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:14795: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3of6Q6/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:14180: 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 14276 states (over memory cap)
KLEE: WARNING: killing 10354 states (over memory cap)
KLEE: WARNING: killing 9521 states (over memory cap)
KLEE: WARNING: killing 9945 states (over memory cap)
KLEE: WARNING: killing 9295 states (over memory cap)
KLEE: WARNING: killing 9094 states (over memory cap)
KLEE: WARNING: killing 10139 states (over memory cap)
KLEE: WARNING: killing 9854 states (over memory cap)
KLEE: WARNING: killing 10099 states (over memory cap)
KLEE: WARNING: killing 10343 states (over memory cap)
KLEE: WARNING: killing 10235 states (over memory cap)
KLEE: WARNING: killing 10128 states (over memory cap)
KLEE: WARNING: killing 10552 states (over memory cap)
KLEE: WARNING: killing 10445 states (over memory cap)
KLEE: WARNING: killing 10604 states (over memory cap)
KLEE: WARNING: killing 11027 states (over memory cap)
KLEE: WARNING: killing 11101 states (over memory cap)
KLEE: WARNING: killing 11087 states (over memory cap)
KLEE: WARNING: killing 11154 states (over memory cap)
KLEE: WARNING: killing 11665 states (over memory cap)
KLEE: WARNING: killing 11216 states (over memory cap)
KLEE: WARNING: killing 11377 states (over memory cap)
KLEE: WARNING: killing 11015 states (over memory cap)
KLEE: WARNING: killing 11437 states (over memory cap)
KLEE: WARNING: killing 11334 states (over memory cap)
KLEE: WARNING: killing 11493 states (over memory cap)
KLEE: WARNING: killing 11568 states (over memory cap)
KLEE: WARNING: killing 11205 states (over memory cap)
KLEE: WARNING: killing 11014 states (over memory cap)
KLEE: WARNING: killing 10914 states (over memory cap)
KLEE: WARNING: killing 10809 states (over memory cap)
KLEE: WARNING: killing 10793 states (over memory cap)
KLEE: WARNING: killing 10861 states (over memory cap)
KLEE: WARNING: killing 11190 states (over memory cap)
KLEE: WARNING: killing 10832 states (over memory cap)
KLEE: WARNING: killing 10990 states (over memory cap)
KLEE: WARNING: killing 10370 states (over memory cap)
KLEE: WARNING: killing 11128 states (over memory cap)
KLEE: WARNING: killing 10768 states (over memory cap)
KLEE: WARNING: killing 10837 states (over memory cap)
KLEE: WARNING: killing 10821 states (over memory cap)
KLEE: WARNING: killing 10892 states (over memory cap)
KLEE: WARNING: killing 10875 states (over memory cap)
KLEE: WARNING: killing 11199 states (over memory cap)
KLEE: WARNING: killing 10676 states (over memory cap)
KLEE: WARNING: killing 10917 states (over memory cap)
KLEE: WARNING: killing 10989 states (over memory cap)
KLEE: WARNING: killing 11229 states (over memory cap)
KLEE: WARNING: killing 11298 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-3of6Q6/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:14168: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10950 states (over memory cap)
KLEE: WARNING: killing 10936 states (over memory cap)
KLEE: WARNING: killing 11172 states (over memory cap)
KLEE: WARNING: killing 11409 states (over memory cap)
KLEE: WARNING: killing 10896 states (over memory cap)
KLEE: WARNING: killing 11130 states (over memory cap)
KLEE: WARNING: killing 10620 states (over memory cap)
KLEE: WARNING: killing 11023 states (over memory cap)
KLEE: WARNING: killing 10759 states (over memory cap)
KLEE: WARNING: killing 10911 states (over memory cap)
KLEE: WARNING: killing 11147 states (over memory cap)
KLEE: WARNING: killing 10806 states (over memory cap)
KLEE: WARNING: killing 11284 states (over memory cap)
KLEE: WARNING: killing 11192 states (over memory cap)
KLEE: WARNING: killing 11097 states (over memory cap)
KLEE: WARNING: killing 11082 states (over memory cap)
KLEE: WARNING: killing 10824 states (over memory cap)
KLEE: WARNING: killing 10894 states (over memory cap)
KLEE: WARNING: killing 10636 states (over memory cap)
KLEE: WARNING: killing 11117 states (over memory cap)
KLEE: WARNING: killing 11351 states (over memory cap)
KLEE: WARNING: killing 11256 states (over memory cap)
KLEE: WARNING: killing 11001 states (over memory cap)
KLEE: WARNING: killing 10985 states (over memory cap)
KLEE: WARNING: killing 10978 states (over memory cap)
KLEE: WARNING: killing 11044 states (over memory cap)
KLEE: WARNING: killing 11115 states (over memory cap)
KLEE: WARNING: killing 11183 states (over memory cap)
KLEE: WARNING: killing 11254 states (over memory cap)
KLEE: WARNING: killing 11246 states (over memory cap)
KLEE: WARNING: killing 11069 states (over memory cap)
KLEE: WARNING: killing 11135 states (over memory cap)
KLEE: WARNING: killing 10803 states (over memory cap)
KLEE: WARNING: killing 10871 states (over memory cap)
KLEE: WARNING: killing 10778 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 10916 states (over memory cap)
KLEE: WARNING: killing 10985 states (over memory cap)
KLEE: WARNING: killing 10653 states (over memory cap)
KLEE: WARNING: killing 11047 states (over memory cap)
KLEE: WARNING: killing 11599 states (over memory cap)
KLEE: WARNING: killing 11022 states (over memory cap)
KLEE: WARNING: killing 10774 states (over memory cap)
KLEE: WARNING: killing 11004 states (over memory cap)
KLEE: WARNING: killing 10748 states (over memory cap)
KLEE: WARNING: killing 10901 states (over memory cap)
KLEE: WARNING: killing 10969 states (over memory cap)
KLEE: WARNING: killing 11195 states (over memory cap)
KLEE: WARNING: killing 11266 states (over memory cap)
KLEE: WARNING: killing 11174 states (over memory cap)
KLEE: WARNING: killing 10766 states (over memory cap)
KLEE: WARNING: killing 11148 states (over memory cap)
KLEE: WARNING: killing 11378 states (over memory cap)
KLEE: WARNING: killing 10815 states (over memory cap)
KLEE: WARNING: killing 11118 states (over memory cap)
KLEE: WARNING: killing 10874 states (over memory cap)
KLEE: WARNING: killing 10782 states (over memory cap)
KLEE: WARNING: killing 11326 states (over memory cap)
KLEE: WARNING: killing 11316 states (over memory cap)
KLEE: WARNING: killing 10906 states (over memory cap)
KLEE: WARNING: killing 11292 states (over memory cap)
KLEE: WARNING: killing 10891 states (over memory cap)
KLEE: WARNING: killing 10723 states (over memory cap)
KLEE: WARNING: killing 11181 states (over memory cap)
KLEE: WARNING: killing 10933 states (over memory cap)
KLEE: WARNING: killing 10684 states (over memory cap)
KLEE: WARNING: killing 10441 states (over memory cap)
KLEE: WARNING: killing 10978 states (over memory cap)
KLEE: WARNING: killing 10888 states (over memory cap)
KLEE: WARNING: killing 10643 states (over memory cap)
KLEE: WARNING: killing 11026 states (over memory cap)
KLEE: WARNING: killing 11174 states (over memory cap)
KLEE: WARNING: killing 10693 states (over memory cap)
KLEE: WARNING: killing 10835 states (over memory cap)
KLEE: WARNING: killing 10906 states (over memory cap)
KLEE: WARNING: killing 11208 states (over memory cap)
KLEE: WARNING: killing 11433 states (over memory cap)
KLEE: WARNING: killing 11032 states (over memory cap)
KLEE: WARNING: killing 10945 states (over memory cap)
KLEE: WARNING: killing 11170 states (over memory cap)
KLEE: WARNING: killing 11238 states (over memory cap)
KLEE: WARNING: killing 11075 states (over memory cap)
KLEE: WARNING: killing 11221 states (over memory cap)
KLEE: WARNING: killing 11056 states (over memory cap)
KLEE: WARNING: killing 10888 states (over memory cap)
KLEE: WARNING: killing 10957 states (over memory cap)
KLEE: WARNING: killing 10944 states (over memory cap)
KLEE: WARNING: killing 11015 states (over memory cap)
KLEE: WARNING: killing 10929 states (over memory cap)
KLEE: WARNING: killing 10915 states (over memory cap)
KLEE: WARNING: killing 10983 states (over memory cap)
KLEE: WARNING: killing 10972 states (over memory cap)
KLEE: WARNING: killing 11117 states (over memory cap)
KLEE: WARNING: killing 10727 states (over memory cap)
KLEE: WARNING: killing 10713 states (over memory cap)
KLEE: WARNING: killing 10781 states (over memory cap)
KLEE: WARNING: killing 10848 states (over memory cap)
KLEE: WARNING: killing 11296 states (over memory cap)
KLEE: WARNING: killing 10829 states (over memory cap)
KLEE: WARNING: killing 10819 states (over memory cap)
KLEE: WARNING: killing 10807 states (over memory cap)
KLEE: WARNING: killing 10873 states (over memory cap)
KLEE: WARNING: killing 11015 states (over memory cap)
KLEE: WARNING: killing 10551 states (over memory cap)
KLEE: WARNING: killing 10841 states (over memory cap)
KLEE: WARNING: killing 11061 states (over memory cap)
KLEE: WARNING: killing 10981 states (over memory cap)
KLEE: WARNING: killing 10890 states (over memory cap)
KLEE: WARNING: killing 10883 states (over memory cap)
KLEE: WARNING: killing 11177 states (over memory cap)
KLEE: WARNING: killing 11245 states (over memory cap)
KLEE: WARNING: killing 10851 states (over memory cap)
KLEE: WARNING: killing 11524 states (over memory cap)
KLEE: WARNING: killing 11136 states (over memory cap)
KLEE: WARNING: killing 10904 states (over memory cap)
KLEE: WARNING: killing 10971 states (over memory cap)
KLEE: WARNING: killing 11035 states (over memory cap)
KLEE: WARNING: killing 11400 states (over memory cap)
KLEE: WARNING: killing 11090 states (over memory cap)
KLEE: WARNING: killing 10855 states (over memory cap)
KLEE: WARNING: killing 10625 states (over memory cap)
KLEE: WARNING: killing 11437 states (over memory cap)
KLEE: WARNING: killing 11204 states (over memory cap)
KLEE: WARNING: killing 11194 states (over memory cap)
KLEE: WARNING: killing 11034 states (over memory cap)
KLEE: WARNING: killing 10578 states (over memory cap)
KLEE: WARNING: killing 10937 states (over memory cap)
KLEE: WARNING: killing 10556 states (over memory cap)
KLEE: WARNING: killing 11215 states (over memory cap)
KLEE: WARNING: killing 10532 states (over memory cap)
KLEE: WARNING: killing 10969 states (over memory cap)
KLEE: WARNING: killing 11184 states (over memory cap)
KLEE: WARNING: killing 11175 states (over memory cap)
KLEE: WARNING: killing 11021 states (over memory cap)
KLEE: WARNING: killing 11084 states (over memory cap)
KLEE: WARNING: killing 10926 states (over memory cap)
KLEE: WARNING: killing 11433 states (over memory cap)
KLEE: WARNING: killing 10980 states (over memory cap)
KLEE: WARNING: killing 10897 states (over memory cap)
KLEE: WARNING: killing 11327 states (over memory cap)
KLEE: WARNING: killing 11245 states (over memory cap)
KLEE: WARNING: killing 11163 states (over memory cap)
KLEE: WARNING: killing 11232 states (over memory cap)
KLEE: WARNING: killing 10999 states (over memory cap)
KLEE: WARNING: killing 11060 states (over memory cap)
KLEE: WARNING: killing 10760 states (over memory cap)
KLEE: WARNING: killing 11043 states (over memory cap)
KLEE: WARNING: killing 11253 states (over memory cap)
KLEE: WARNING: killing 11316 states (over memory cap)
KLEE: WARNING: killing 11083 states (over memory cap)
KLEE: WARNING: killing 10778 states (over memory cap)
KLEE: WARNING: killing 10769 states (over memory cap)
KLEE: WARNING: killing 10982 states (over memory cap)
KLEE: WARNING: killing 10821 states (over memory cap)
KLEE: WARNING: killing 10740 states (over memory cap)
KLEE: WARNING: killing 10875 states (over memory cap)
KLEE: WARNING: killing 11311 states (over memory cap)
KLEE: WARNING: killing 10859 states (over memory cap)
KLEE: WARNING: killing 10992 states (over memory cap)
