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-drivers--staging--speakup--speakup.ko-ldv_main4_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.: 856 344 3304 20863
Removed infinite loop in get_var
Removed infinite loop in arch_local_irq_restore
Removed infinite loop in arch_local_save_flags
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in speakup_register_var
Removed infinite loop in speakup_unregister_var
Removed infinite loop in message_show
Removed infinite loop in message_store
INFO: Compilation, preparation and instrumentation time: 0.744191169739
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function vt_get_leds as symbolic
Defining function vsnprintf as symbolic
Removed calls to 'stop_tty' (function is undefined)
Defining function msecs_to_jiffies as symbolic
Defining function mod_timer as symbolic
Defining function wake_up_process as symbolic
Defining function printk as symbolic
Defining function del_timer as symbolic
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'input_event' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Defining function inverse_translate as symbolic
Defining function snprintf as symbolic
Defining function sprintf as symbolic
Defining function _raw_spin_trylock as symbolic
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)
Defining function default_wake_function as symbolic
Defining function dev_warn as symbolic
Defining function screen_glyph as symbolic
Removed calls to 'might_fault' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function kmemdup as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function sysfs_create_group as symbolic
Removed calls to 'free_irq' (function is undefined)
Defining function scnprintf as symbolic
Removed calls to 'start_tty' (function is undefined)
Defining function mutex_trylock as symbolic
Defining function misc_register as symbolic
Defining function misc_deregister as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to 'input_free_device' (function is undefined)
Defining function input_allocate_device as symbolic
Defining function input_register_device as symbolic
Removed calls to 'input_unregister_device' (function is undefined)
Removed calls to 'set_user_nice' (function is undefined)
Defining function unregister_keyboard_notifier as symbolic
Defining function unregister_vt_notifier as symbolic
Defining function kthread_stop as symbolic
Removed calls to 'kobject_put' (function is undefined)
Defining function register_keyboard_notifier as symbolic
Defining function register_vt_notifier as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'kd_mksound' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function autoremove_wake_function as symbolic
Defining function kthread_should_stop as symbolic
Defining function kobject_create_and_add as symbolic
Removed calls to '__release_region' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function request_threaded_irq as symbolic
Defining function release_resource as symbolic
Defining function request_resource as symbolic
Defining function schedule_timeout as symbolic
Defining function memchr as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strchr
  strcmp
  strcpy
  strlen
  strncpy
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.691992998123
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 937 334 2184 11725
INFO: Starting verification
KLEE: WARNING ONCE: function "keyboard_notifier_call" has inline asm
KLEE: WARNING ONCE: function "get_var" has inline asm
KLEE: WARNING ONCE: function "speakup_fake_down_arrow" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_save" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_restore" has inline asm
KLEE: WARNING ONCE: function "speakup_paste_selection" has inline asm
KLEE: WARNING ONCE: function "speakup_file_open" has inline asm
KLEE: WARNING ONCE: function "speakup_register_var" has inline asm
KLEE: WARNING ONCE: function "speakup_unregister_var" has inline asm
KLEE: WARNING ONCE: function "stop_serial_interrupt" has inline asm
KLEE: WARNING ONCE: function "message_show" has inline asm
KLEE: WARNING ONCE: function "message_store" has inline asm
KLEE: WARNING ONCE: function "speakup_fake_key_pressed" has inline asm
KLEE: WARNING ONCE: function "ldv_main1_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING ONCE: function "speakup_add_virtual_keyboard" has inline asm
KLEE: WARNING ONCE: function "speakup_thread" has inline asm
KLEE: WARNING ONCE: function "spk_serial_init" has inline asm
KLEE: WARNING ONCE: function "synth_readbuf_handler" has inline asm
KLEE: WARNING ONCE: function "wait_for_xmitr" has inline asm
KLEE: WARNING ONCE: function "spk_serial_in" has inline asm
KLEE: WARNING ONCE: function "spk_serial_in_nowait" has inline asm
KLEE: WARNING ONCE: function "spk_serial_out" has inline asm
KLEE: WARNING ONCE: function "serial_synth_probe" has inline asm
KLEE: WARNING ONCE: function "spk_do_catch_up" has inline asm
KLEE: WARNING ONCE: function "spk_synth_immediate" 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 5544 bytes on read, may be slow and/or crash: MO405[5544] allocated at global:vc_cons
KLEE: ERROR: /tmp/symbiotic-xAWuDO/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--speakup--speakup.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c:9662: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xAWuDO/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--speakup--speakup.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c:9667: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xAWuDO/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--speakup--speakup.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c:5423: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xAWuDO/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--speakup--speakup.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c:5423: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xAWuDO/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--speakup--speakup.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c:5424: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xAWuDO/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--staging--speakup--speakup.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c:5426: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
