bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-validator-v0.6/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_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.: 208 300 4102 23689
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.676010131836
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 '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
  __memcpy
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.729106903076
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 319 260 2179 13516
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_c344a667-a201-449e-af78-68cdbb52c9b4/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:4171: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:3482: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:4565: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:4533: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 7789 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 10389 states (over memory cap)
KLEE: WARNING: killing 10364 states (over memory cap)
KLEE: WARNING: killing 10259 states (over memory cap)
KLEE: WARNING: killing 10464 states (over memory cap)
KLEE: WARNING: killing 9981 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14368: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9958 states (over memory cap)
KLEE: WARNING: killing 10315 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14209: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10901 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14457: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10122 states (over memory cap)
KLEE: WARNING: killing 10707 states (over memory cap)
KLEE: WARNING: killing 10917 states (over memory cap)
KLEE: WARNING: killing 11051 states (over memory cap)
KLEE: WARNING: killing 11107 states (over memory cap)
KLEE: WARNING: killing 11091 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14416: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11451 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14984: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14840: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11584 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14325: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:15056: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:15133: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11568 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14948: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11776 states (over memory cap)
KLEE: WARNING: killing 11690 states (over memory cap)
KLEE: WARNING: killing 11746 states (over memory cap)
KLEE: WARNING: killing 11585 states (over memory cap)
KLEE: WARNING: killing 11119 states (over memory cap)
KLEE: WARNING: killing 11399 states (over memory cap)
KLEE: WARNING: killing 11011 states (over memory cap)
KLEE: WARNING: killing 11066 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:15194: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10683 states (over memory cap)
KLEE: WARNING: killing 11188 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:4171: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10801 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:4533: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11004 states (over memory cap)
KLEE: WARNING: killing 11358 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:4565: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10898 states (over memory cap)
KLEE: WARNING: killing 10734 states (over memory cap)
KLEE: WARNING: killing 11597 states (over memory cap)
KLEE: WARNING: killing 11438 states (over memory cap)
KLEE: WARNING: killing 10906 states (over memory cap)
KLEE: WARNING: killing 11184 states (over memory cap)
KLEE: WARNING: killing 11242 states (over memory cap)
KLEE: WARNING: killing 10939 states (over memory cap)
KLEE: WARNING: killing 11139 states (over memory cap)
KLEE: WARNING: killing 11340 states (over memory cap)
KLEE: WARNING: killing 11403 states (over memory cap)
KLEE: WARNING: killing 11314 states (over memory cap)
KLEE: WARNING: killing 10650 states (over memory cap)
KLEE: WARNING: killing 11290 states (over memory cap)
KLEE: WARNING: killing 11425 states (over memory cap)
KLEE: WARNING: killing 10899 states (over memory cap)
KLEE: WARNING: killing 11317 states (over memory cap)
KLEE: WARNING: killing 11306 states (over memory cap)
KLEE: WARNING: killing 11221 states (over memory cap)
KLEE: WARNING: killing 11138 states (over memory cap)
KLEE: WARNING: killing 11265 states (over memory cap)
KLEE: WARNING: killing 11540 states (over memory cap)
KLEE: WARNING: killing 10955 states (over memory cap)
KLEE: WARNING: killing 11443 states (over memory cap)
KLEE: WARNING: killing 11499 states (over memory cap)
KLEE: WARNING: killing 10631 states (over memory cap)
KLEE: WARNING: killing 11613 states (over memory cap)
KLEE: WARNING: killing 10960 states (over memory cap)
KLEE: WARNING: killing 11160 states (over memory cap)
KLEE: WARNING: killing 11434 states (over memory cap)
KLEE: WARNING: killing 11425 states (over memory cap)
KLEE: WARNING: killing 11197 states (over memory cap)
KLEE: WARNING: killing 11111 states (over memory cap)
KLEE: WARNING: killing 11170 states (over memory cap)
KLEE: WARNING: killing 11159 states (over memory cap)
KLEE: WARNING: killing 11572 states (over memory cap)
KLEE: WARNING: killing 11350 states (over memory cap)
KLEE: WARNING: killing 11477 states (over memory cap)
KLEE: WARNING: killing 10976 states (over memory cap)
KLEE: WARNING: killing 10892 states (over memory cap)
KLEE: WARNING: killing 10808 states (over memory cap)
KLEE: WARNING: killing 11361 states (over memory cap)
KLEE: WARNING: killing 11209 states (over memory cap)
KLEE: WARNING: killing 11195 states (over memory cap)
KLEE: WARNING: killing 10761 states (over memory cap)
KLEE: WARNING: killing 10888 states (over memory cap)
KLEE: WARNING: killing 11226 states (over memory cap)
KLEE: WARNING: killing 11494 states (over memory cap)
KLEE: WARNING: killing 11134 states (over memory cap)
KLEE: WARNING: killing 11541 states (over memory cap)
KLEE: WARNING: killing 11116 states (over memory cap)
KLEE: WARNING: killing 11244 states (over memory cap)
KLEE: WARNING: killing 11088 states (over memory cap)
KLEE: WARNING: killing 11429 states (over memory cap)
KLEE: WARNING: killing 11275 states (over memory cap)
KLEE: WARNING: killing 11197 states (over memory cap)
KLEE: WARNING: killing 11673 states (over memory cap)
KLEE: WARNING: killing 11386 states (over memory cap)
KLEE: WARNING: killing 10961 states (over memory cap)
KLEE: WARNING: killing 10809 states (over memory cap)
KLEE: WARNING: killing 11074 states (over memory cap)
KLEE: WARNING: killing 11271 states (over memory cap)
KLEE: WARNING: killing 11187 states (over memory cap)
KLEE: WARNING: killing 11386 states (over memory cap)
KLEE: WARNING: killing 10689 states (over memory cap)
KLEE: WARNING: killing 11015 states (over memory cap)
KLEE: WARNING: killing 10872 states (over memory cap)
KLEE: WARNING: killing 10921 states (over memory cap)
KLEE: WARNING: killing 11115 states (over memory cap)
KLEE: WARNING: killing 11172 states (over memory cap)
KLEE: WARNING: killing 11367 states (over memory cap)
KLEE: WARNING: killing 11083 states (over memory cap)
KLEE: WARNING: killing 11621 states (over memory cap)
KLEE: WARNING: killing 11674 states (over memory cap)
KLEE: WARNING: killing 11257 states (over memory cap)
KLEE: WARNING: killing 11454 states (over memory cap)
KLEE: WARNING: killing 11169 states (over memory cap)
KLEE: WARNING: killing 10887 states (over memory cap)
KLEE: WARNING: killing 11483 states (over memory cap)
KLEE: WARNING: killing 11274 states (over memory cap)
KLEE: WARNING: killing 11324 states (over memory cap)
KLEE: WARNING: killing 11113 states (over memory cap)
KLEE: WARNING: killing 10761 states (over memory cap)
KLEE: WARNING: killing 10952 states (over memory cap)
KLEE: WARNING: killing 11141 states (over memory cap)
KLEE: WARNING: killing 11535 states (over memory cap)
KLEE: WARNING: killing 11192 states (over memory cap)
KLEE: WARNING: killing 11179 states (over memory cap)
KLEE: WARNING: killing 11031 states (over memory cap)
KLEE: WARNING: killing 11018 states (over memory cap)
KLEE: WARNING: killing 11478 states (over memory cap)
KLEE: WARNING: killing 11195 states (over memory cap)
KLEE: WARNING: killing 11383 states (over memory cap)
KLEE: WARNING: killing 11173 states (over memory cap)
KLEE: WARNING: killing 10965 states (over memory cap)
KLEE: WARNING: killing 10950 states (over memory cap)
KLEE: WARNING: killing 11340 states (over memory cap)
KLEE: WARNING: killing 11126 states (over memory cap)
KLEE: WARNING: killing 11177 states (over memory cap)
KLEE: WARNING: killing 11104 states (over memory cap)
KLEE: WARNING: killing 11227 states (over memory cap)
KLEE: WARNING: killing 11483 states (over memory cap)
KLEE: WARNING: killing 11338 states (over memory cap)
KLEE: WARNING: killing 11588 states (over memory cap)
KLEE: WARNING: killing 10850 states (over memory cap)
KLEE: WARNING: killing 10640 states (over memory cap)
KLEE: WARNING: killing 11021 states (over memory cap)
KLEE: WARNING: killing 11209 states (over memory cap)
KLEE: WARNING: killing 11595 states (over memory cap)
KLEE: WARNING: killing 11521 states (over memory cap)
KLEE: WARNING: killing 11116 states (over memory cap)
KLEE: WARNING: killing 11304 states (over memory cap)
KLEE: WARNING: killing 11555 states (over memory cap)
KLEE: WARNING: killing 11215 states (over memory cap)
KLEE: WARNING: killing 10874 states (over memory cap)
KLEE: WARNING: killing 11389 states (over memory cap)
KLEE: WARNING: killing 11314 states (over memory cap)
KLEE: WARNING: killing 11432 states (over memory cap)
KLEE: WARNING: killing 11293 states (over memory cap)
KLEE: WARNING: killing 10958 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:14197: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11341 states (over memory cap)
KLEE: WARNING: killing 11132 states (over memory cap)
KLEE: WARNING: killing 11385 states (over memory cap)
KLEE: WARNING: killing 10724 states (over memory cap)
KLEE: WARNING: killing 10906 states (over memory cap)
KLEE: WARNING: killing 11412 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-YO1ld_/linux-torvalds-645ef9e-32_7a-sound--oss--sound.ko-entry_point_false-unreach-call.cil.out.c:4141: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10818 states (over memory cap)
KLEE: WARNING: killing 10999 states (over memory cap)
KLEE: WARNING: killing 10987 states (over memory cap)
KLEE: WARNING: killing 11173 states (over memory cap)
KLEE: WARNING: killing 11161 states (over memory cap)
KLEE: WARNING: killing 11407 states (over memory cap)
KLEE: WARNING: killing 11081 states (over memory cap)
KLEE: WARNING: killing 11325 states (over memory cap)
KLEE: WARNING: killing 11380 states (over memory cap)
KLEE: WARNING: killing 11434 states (over memory cap)
KLEE: WARNING: killing 11361 states (over memory cap)
KLEE: WARNING: killing 10772 states (over memory cap)
KLEE: WARNING: killing 11659 states (over memory cap)
KLEE: WARNING: killing 11074 states (over memory cap)
KLEE: WARNING: killing 11260 states (over memory cap)
