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-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.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.: 54 161 1391 8399
INFO: Compilation, preparation and instrumentation time: 0.384884119034
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function no_llseek as symbolic
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'add_wait_queue' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'remove_wait_queue' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__snd_printk' (function is undefined)
Removed calls to 'snd_card_unref' (function is undefined)
Removed calls to '_raw_read_lock' (function is undefined)
Removed calls to '_raw_read_unlock' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Defining function snd_card_file_remove as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'put_pid' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function cancel_work_sync as symbolic
Defining function nonseekable_open as symbolic
Defining function snd_lookup_minor_data as symbolic
Defining function snd_lookup_oss_minor_data as symbolic
Defining function try_module_get as symbolic
Defining function snd_card_file_add as symbolic
Removed calls to '__raw_spin_lock_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)
Defining function default_wake_function as symbolic
Defining function krealloc as symbolic
Defining function _copy_to_user as symbolic
Defining function schedule_work as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'snd_info_free_entry' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Defining function strlcpy as symbolic
Defining function snd_device_new as symbolic
Defining function snd_unregister_oss_device as symbolic
Defining function snd_oss_info_register as symbolic
Defining function snd_unregister_device as symbolic
Defining function sprintf as symbolic
Defining function snd_register_oss_device as symbolic
Defining function snd_info_create_card_entry as symbolic
Defining function snd_info_register as symbolic
Defining function snd_seq_device_new as symbolic
Defining function snd_device_register as symbolic
Defining function snd_iprintf as symbolic
Defining function pid_vnr as symbolic
Defining function snd_register_device_for_dev as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Defining function snd_ctl_unregister_ioctl as symbolic
Defining function snd_ctl_unregister_ioctl_compat as symbolic
Defining function snd_ctl_register_ioctl as symbolic
Defining function snd_ctl_register_ioctl_compat as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.440647125244
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 133 162 896 7049
INFO: Starting verification
KLEE: WARNING ONCE: function "snd_rawmidi_read" has inline asm
KLEE: WARNING ONCE: function "snd_rawmidi_write" has inline asm
KLEE: WARNING ONCE: function "snd_rawmidi_ioctl" has inline asm
KLEE: WARNING ONCE: function "snd_rawmidi_ioctl_compat" has inline asm
KLEE: WARNING ONCE: function "snd_rawmidi_open" has inline asm
KLEE: WARNING ONCE: function "snd_rawmidi_drain_output" has inline asm
KLEE: WARNING ONCE: function "open_substream" has inline asm
KLEE: WARNING ONCE: function "snd_rawmidi_control_ioctl" has inline asm
KLEE: WARNING ONCE: flushing 9576 bytes on read, may be slow and/or crash: MO14[9576] allocated at global:
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6281: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:5635: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:5636: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:5637: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6309: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6255: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3426: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6310: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:5644: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3206: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6256: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:6422: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3431: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:5643: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3431: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-jBXE6r/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-sound--core--snd-rawmidi.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c:3822: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
