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-stable-42f9f8d-1-111_1a-sound--oss--opl3.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.: 36 53 694 4698
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.222727060318
Removed calls to 'might_fault' (function is undefined)
Defining function compute_finetune as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function printk as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function note_to_freq as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'sound_unload_synthdev' (function is undefined)
Removed calls to 'sequencer_init' (function is undefined)
Removed calls to 'conf_printf2' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function sound_alloc_synthdev as symbolic
Defining function __request_region as symbolic
Defining function __copy_user_nocache as symbolic
Linked our definitions to these undefined functions:
  strcpy
  __kmalloc
  kfree
  __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.25096988678
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 79 59 376 2857
INFO: Starting verification
KLEE: WARNING ONCE: function "opl3_command" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
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_1c819d32-4ca5-44b3-996d-dbb23008521d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-16nXg1/linux-stable-42f9f8d-1-111_1a-sound--oss--opl3.ko-entry_point_ldv-val-v0.8_false-unreach-call.cil.out.c:2608: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 6181 states (over memory cap)
KLEE: WARNING: killing 5775 states (over memory cap)
KLEE: WARNING: killing 6788 states (over memory cap)
KLEE: WARNING: killing 6985 states (over memory cap)
KLEE: WARNING: killing 7175 states (over memory cap)
KLEE: WARNING: killing 7305 states (over memory cap)
KLEE: WARNING: killing 7480 states (over memory cap)
KLEE: WARNING: killing 7277 states (over memory cap)
KLEE: WARNING: killing 7231 states (over memory cap)
KLEE: WARNING: killing 7411 states (over memory cap)
KLEE: WARNING: killing 7318 states (over memory cap)
KLEE: WARNING: killing 7344 states (over memory cap)
KLEE: WARNING: killing 7144 states (over memory cap)
KLEE: WARNING: killing 7162 states (over memory cap)
KLEE: WARNING: killing 7299 states (over memory cap)
KLEE: WARNING: killing 6945 states (over memory cap)
KLEE: WARNING: killing 7127 states (over memory cap)
KLEE: WARNING: killing 7094 states (over memory cap)
KLEE: WARNING: killing 7221 states (over memory cap)
KLEE: WARNING: killing 7144 states (over memory cap)
KLEE: WARNING: killing 7058 states (over memory cap)
KLEE: WARNING: killing 7188 states (over memory cap)
KLEE: WARNING: killing 6955 states (over memory cap)
KLEE: WARNING: killing 7144 states (over memory cap)
KLEE: WARNING: killing 7006 states (over memory cap)
KLEE: WARNING: killing 6985 states (over memory cap)
KLEE: WARNING: killing 7025 states (over memory cap)
KLEE: WARNING: killing 6800 states (over memory cap)
KLEE: WARNING: killing 6682 states (over memory cap)
KLEE: WARNING: killing 6865 states (over memory cap)
KLEE: WARNING: killing 6956 states (over memory cap)
KLEE: WARNING: killing 7094 states (over memory cap)
KLEE: WARNING: killing 6719 states (over memory cap)
KLEE: WARNING: killing 6806 states (over memory cap)
KLEE: WARNING: killing 6582 states (over memory cap)
KLEE: WARNING: killing 6928 states (over memory cap)
KLEE: WARNING: killing 6861 states (over memory cap)
KLEE: WARNING: killing 6944 states (over memory cap)
KLEE: WARNING: killing 6989 states (over memory cap)
KLEE: WARNING: killing 6718 states (over memory cap)
KLEE: WARNING: killing 6807 states (over memory cap)
KLEE: WARNING: killing 6739 states (over memory cap)
KLEE: WARNING: killing 6568 states (over memory cap)
KLEE: WARNING: killing 6850 states (over memory cap)
KLEE: WARNING: killing 4956 states (over memory cap)
KLEE: WARNING: killing 6876 states (over memory cap)
KLEE: WARNING: killing 6951 states (over memory cap)
KLEE: WARNING: killing 6841 states (over memory cap)
KLEE: WARNING: killing 6776 states (over memory cap)
KLEE: WARNING: killing 6819 states (over memory cap)
KLEE: WARNING: killing 6857 states (over memory cap)
KLEE: WARNING: killing 6742 states (over memory cap)
KLEE: WARNING: killing 6779 states (over memory cap)
KLEE: WARNING: killing 6803 states (over memory cap)
KLEE: WARNING: killing 6881 states (over memory cap)
KLEE: WARNING: killing 6871 states (over memory cap)
KLEE: WARNING: killing 6899 states (over memory cap)
KLEE: WARNING: killing 6690 states (over memory cap)
KLEE: WARNING: killing 4854 states (over memory cap)
KLEE: WARNING: killing 6616 states (over memory cap)
KLEE: WARNING: killing 6657 states (over memory cap)
KLEE: WARNING: killing 6789 states (over memory cap)
KLEE: WARNING: killing 6718 states (over memory cap)
KLEE: WARNING: killing 4813 states (over memory cap)
KLEE: WARNING: killing 6744 states (over memory cap)
KLEE: WARNING: killing 4886 states (over memory cap)
KLEE: WARNING: killing 6519 states (over memory cap)
KLEE: WARNING: killing 4861 states (over memory cap)
KLEE: WARNING: killing 6545 states (over memory cap)
KLEE: WARNING: killing 4701 states (over memory cap)
KLEE: WARNING: killing 6612 states (over memory cap)
KLEE: WARNING: killing 4727 states (over memory cap)
KLEE: WARNING: killing 6627 states (over memory cap)
KLEE: WARNING: killing 6658 states (over memory cap)
KLEE: WARNING: killing 4785 states (over memory cap)
KLEE: WARNING: killing 4693 states (over memory cap)
KLEE: WARNING: killing 4736 states (over memory cap)
KLEE: WARNING: killing 6447 states (over memory cap)
KLEE: WARNING: killing 4678 states (over memory cap)
KLEE: WARNING: killing 6369 states (over memory cap)
KLEE: WARNING: killing 4708 states (over memory cap)
