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--oss--snd-mixer-oss.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.: 93 97 1087 6366
INFO: Compilation, preparation and instrumentation time: 0.274873018265
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Defining function strlcpy as symbolic
Defining function _copy_to_user as symbolic
Defining function no_llseek as symbolic
Removed calls to 'snd_card_unref' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Defining function snd_card_file_remove as symbolic
Defining function nonseekable_open as symbolic
Defining function snd_lookup_oss_minor_data as symbolic
Defining function snd_card_file_add as symbolic
Defining function try_module_get as symbolic
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'ldv_check_return_value' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__snd_printk' (function is undefined)
Removed calls to 'snd_info_free_entry' (function is undefined)
Defining function sprintf as symbolic
Defining function snd_register_oss_device as symbolic
Defining function snd_oss_info_register as symbolic
Defining function snd_unregister_oss_device as symbolic
Defining function snd_info_create_card_entry as symbolic
Defining function snd_info_register as symbolic
Defining function snd_info_get_str as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function simple_strtoul as symbolic
Defining function kstrdup as symbolic
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function snd_info_get_line as symbolic
Removed calls to 'snd_ctl_notify' (function is undefined)
Defining function snd_ctl_find_numid as symbolic
Defining function snd_ctl_find_id as symbolic
Defining function snd_iprintf as symbolic
Linked our definitions to these undefined functions:
  strcmp
  strcpy
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.268550872803
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 167 97 667 3672
INFO: Starting verification
KLEE: WARNING ONCE: function "snd_mixer_oss_ioctl1" has inline asm
KLEE: WARNING: undefined reference to variable: snd_mixer_oss_notify_callback
KLEE: ERROR: unable to load symbol(snd_mixer_oss_notify_callback) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-MtPof7/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "snd_mixer_oss_ioctl1" has inline asm
KLEE: WARNING: undefined reference to variable: snd_mixer_oss_notify_callback
KLEE: ERROR: unable to load symbol(snd_mixer_oss_notify_callback) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 0.632344007492
