bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-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.: 96 112 871 5453
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.270137071609
Removed calls to '__mutex_init' (function is undefined)
Defining function snd_card_free as symbolic
Defining function snd_card_new as symbolic
Removed calls to 'snd_pcm_set_ops' (function is undefined)
Defining function sprintf as symbolic
Defining function snd_card_register as symbolic
Defining function snprintf as symbolic
Defining function snd_card_proc_new as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function snd_iprintf as symbolic
Defining function snd_ctl_new1 as symbolic
Defining function snd_ctl_add as symbolic
Defining function snd_pcm_new as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function snd_pcm_suspend_all as symbolic
Defining function snd_pcm_lib_ioctl as symbolic
Removed calls to 'snd_ctl_notify' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function snd_pcm_lib_get_vmalloc_page as symbolic
Defining function snd_pcm_format_set_silence as symbolic
Removed calls to 'add_timer' (function is undefined)
Defining function del_timer as symbolic
Defining function snd_pcm_stop as symbolic
Defining function snd_pcm_format_width as symbolic
Defining function snd_pcm_lib_free_vmalloc_buffer as symbolic
Defining function _snd_pcm_lib_alloc_vmalloc_buffer as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'snd_pcm_period_elapsed' (function is undefined)
Defining function snd_ctl_boolean_mono_info as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_suspend_late_3 as symbolic
Defining function ldv_restore_early_3 as symbolic
Defining function ldv_resume_early_3 as symbolic
Defining function ldv_thaw_early_3 as symbolic
Defining function ldv_resume_noirq_3 as symbolic
Defining function ldv_freeze_noirq_3 as symbolic
Defining function ldv_prepare_3 as symbolic
Defining function ldv_freeze_late_3 as symbolic
Defining function ldv_thaw_noirq_3 as symbolic
Defining function ldv_poweroff_noirq_3 as symbolic
Defining function ldv_poweroff_late_3 as symbolic
Defining function ldv_restore_noirq_3 as symbolic
Defining function ldv_suspend_noirq_3 as symbolic
Defining function ldv_complete_3 as symbolic
Defining function printk as symbolic
Removed calls to 'platform_driver_unregister' (function is undefined)
Defining function platform_device_register_full as symbolic
Defining function __platform_driver_register as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strcpy
  strlen
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.281404972076
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 160 116 478 3032
INFO: Starting verification
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_f7daaf53-5003-495b-ac04-ce55265d354c/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:5671: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12466 states (over memory cap)
KLEE: WARNING: killing 9488 states (over memory cap)
KLEE: WARNING: killing 8896 states (over memory cap)
KLEE: WARNING: killing 8794 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4869: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8777 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4899: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4443: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8921 states (over memory cap)
KLEE: WARNING: killing 8983 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:5008: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9050 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4556: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8872 states (over memory cap)
KLEE: WARNING: killing 9098 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4911: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9246 states (over memory cap)
KLEE: WARNING: killing 8910 states (over memory cap)
KLEE: WARNING: killing 8817 states (over memory cap)
KLEE: WARNING: killing 8962 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4899: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9107 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:5516: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9413 states (over memory cap)
KLEE: WARNING: killing 9243 states (over memory cap)
KLEE: WARNING: killing 9149 states (over memory cap)
KLEE: WARNING: killing 9774 states (over memory cap)
KLEE: WARNING: killing 9600 states (over memory cap)
KLEE: WARNING: killing 9193 states (over memory cap)
KLEE: WARNING: killing 9257 states (over memory cap)
KLEE: WARNING: killing 9005 states (over memory cap)
KLEE: WARNING: killing 9630 states (over memory cap)
KLEE: WARNING: killing 9455 states (over memory cap)
KLEE: WARNING: killing 9681 states (over memory cap)
KLEE: WARNING: killing 9353 states (over memory cap)
KLEE: WARNING: killing 9262 states (over memory cap)
KLEE: WARNING: killing 9410 states (over memory cap)
KLEE: WARNING: killing 9235 states (over memory cap)
KLEE: WARNING: killing 9379 states (over memory cap)
KLEE: WARNING: killing 8978 states (over memory cap)
KLEE: WARNING: killing 9670 states (over memory cap)
KLEE: WARNING: killing 9421 states (over memory cap)
KLEE: WARNING: killing 9406 states (over memory cap)
KLEE: WARNING: killing 9240 states (over memory cap)
KLEE: WARNING: killing 9152 states (over memory cap)
KLEE: WARNING: killing 9531 states (over memory cap)
KLEE: WARNING: killing 9517 states (over memory cap)
KLEE: WARNING: killing 9271 states (over memory cap)
KLEE: WARNING: killing 8950 states (over memory cap)
KLEE: WARNING: killing 9248 states (over memory cap)
KLEE: WARNING: killing 9388 states (over memory cap)
KLEE: WARNING: killing 8991 states (over memory cap)
KLEE: WARNING: killing 9675 states (over memory cap)
KLEE: WARNING: killing 9281 states (over memory cap)
KLEE: WARNING: killing 9347 states (over memory cap)
KLEE: WARNING: killing 9722 states (over memory cap)
KLEE: WARNING: killing 9560 states (over memory cap)
KLEE: WARNING: killing 9007 states (over memory cap)
KLEE: WARNING: killing 9302 states (over memory cap)
KLEE: WARNING: killing 9290 states (over memory cap)
KLEE: WARNING: killing 9205 states (over memory cap)
KLEE: WARNING: killing 9425 states (over memory cap)
KLEE: WARNING: killing 9260 states (over memory cap)
KLEE: WARNING: killing 9325 states (over memory cap)
KLEE: WARNING: killing 9545 states (over memory cap)
KLEE: WARNING: killing 9230 states (over memory cap)
KLEE: WARNING: killing 9447 states (over memory cap)
KLEE: WARNING: killing 9743 states (over memory cap)
KLEE: WARNING: killing 9577 states (over memory cap)
KLEE: WARNING: killing 9262 states (over memory cap)
KLEE: WARNING: killing 9405 states (over memory cap)
KLEE: WARNING: killing 9470 states (over memory cap)
KLEE: WARNING: killing 9383 states (over memory cap)
KLEE: WARNING: killing 9602 states (over memory cap)
KLEE: WARNING: killing 9439 states (over memory cap)
KLEE: WARNING: killing 9582 states (over memory cap)
KLEE: WARNING: killing 9348 states (over memory cap)
KLEE: WARNING: killing 9563 states (over memory cap)
KLEE: WARNING: killing 9480 states (over memory cap)
KLEE: WARNING: killing 9621 states (over memory cap)
KLEE: WARNING: killing 9461 states (over memory cap)
KLEE: WARNING: killing 9374 states (over memory cap)
KLEE: WARNING: killing 9140 states (over memory cap)
KLEE: WARNING: killing 9429 states (over memory cap)
KLEE: WARNING: killing 9645 states (over memory cap)
KLEE: WARNING: killing 9560 states (over memory cap)
KLEE: WARNING: killing 9399 states (over memory cap)
KLEE: WARNING: killing 9390 states (over memory cap)
KLEE: WARNING: killing 9676 states (over memory cap)
KLEE: WARNING: killing 9220 states (over memory cap)
KLEE: WARNING: killing 9209 states (over memory cap)
KLEE: WARNING: killing 9573 states (over memory cap)
KLEE: WARNING: killing 9634 states (over memory cap)
KLEE: WARNING: killing 9552 states (over memory cap)
KLEE: WARNING: killing 9541 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4912: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9310 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4870: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9894 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4557: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9739 states (over memory cap)
KLEE: WARNING: killing 9434 states (over memory cap)
KLEE: WARNING: killing 9351 states (over memory cap)
KLEE: WARNING: killing 9707 states (over memory cap)
KLEE: WARNING: killing 9842 states (over memory cap)
KLEE: WARNING: killing 9470 states (over memory cap)
KLEE: WARNING: killing 9385 states (over memory cap)
KLEE: WARNING: killing 9668 states (over memory cap)
KLEE: WARNING: killing 9732 states (over memory cap)
KLEE: WARNING: killing 9723 states (over memory cap)
KLEE: WARNING: killing 9638 states (over memory cap)
KLEE: WARNING: killing 9411 states (over memory cap)
KLEE: WARNING: killing 9911 states (over memory cap)
KLEE: WARNING: killing 9908 states (over memory cap)
KLEE: WARNING: killing 9750 states (over memory cap)
KLEE: WARNING: killing 9520 states (over memory cap)
KLEE: WARNING: killing 9584 states (over memory cap)
KLEE: WARNING: killing 9431 states (over memory cap)
KLEE: WARNING: killing 9709 states (over memory cap)
KLEE: WARNING: killing 9626 states (over memory cap)
KLEE: WARNING: killing 9835 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:4444: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9468 states (over memory cap)
KLEE: WARNING: killing 9673 states (over memory cap)
KLEE: WARNING: killing 9373 states (over memory cap)
KLEE: WARNING: killing 9723 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-HyeMQw/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-aloop.ko-entry_point_true-unreach-call.cil.out.c:5591: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9716 states (over memory cap)
KLEE: WARNING: killing 9700 states (over memory cap)
KLEE: WARNING: killing 9619 states (over memory cap)
KLEE: WARNING: killing 9467 states (over memory cap)
KLEE: WARNING: killing 9458 states (over memory cap)
KLEE: WARNING: killing 9735 states (over memory cap)
KLEE: WARNING: killing 9366 states (over memory cap)
KLEE: WARNING: killing 9924 states (over memory cap)
KLEE: WARNING: killing 9559 states (over memory cap)
KLEE: WARNING: killing 9622 states (over memory cap)
KLEE: WARNING: killing 10257 states (over memory cap)
KLEE: WARNING: killing 9817 states (over memory cap)
KLEE: WARNING: killing 9523 states (over memory cap)
KLEE: WARNING: killing 9584 states (over memory cap)
KLEE: WARNING: killing 8938 states (over memory cap)
KLEE: WARNING: killing 9918 states (over memory cap)
KLEE: WARNING: killing 9699 states (over memory cap)
KLEE: WARNING: killing 9834 states (over memory cap)
KLEE: WARNING: killing 9398 states (over memory cap)
KLEE: WARNING: killing 9741 states (over memory cap)
KLEE: WARNING: killing 10154 states (over memory cap)
KLEE: WARNING: killing 9514 states (over memory cap)
KLEE: WARNING: killing 9502 states (over memory cap)
KLEE: WARNING: killing 9636 states (over memory cap)
KLEE: WARNING: killing 9272 states (over memory cap)
KLEE: WARNING: killing 9684 states (over memory cap)
KLEE: WARNING: killing 9955 states (over memory cap)
KLEE: WARNING: killing 9243 states (over memory cap)
KLEE: WARNING: killing 9651 states (over memory cap)
KLEE: WARNING: killing 9432 states (over memory cap)
KLEE: WARNING: killing 9911 states (over memory cap)
KLEE: WARNING: killing 9276 states (over memory cap)
KLEE: WARNING: killing 10105 states (over memory cap)
KLEE: WARNING: killing 9678 states (over memory cap)
KLEE: WARNING: killing 9528 states (over memory cap)
KLEE: WARNING: killing 9796 states (over memory cap)
KLEE: WARNING: killing 9578 states (over memory cap)
KLEE: WARNING: killing 9639 states (over memory cap)
KLEE: WARNING: killing 9352 states (over memory cap)
KLEE: WARNING: killing 9761 states (over memory cap)
KLEE: WARNING: killing 10373 states (over memory cap)
KLEE: WARNING: killing 9675 states (over memory cap)
KLEE: WARNING: killing 9735 states (over memory cap)
KLEE: WARNING: killing 9726 states (over memory cap)
KLEE: WARNING: killing 9440 states (over memory cap)
KLEE: WARNING: killing 9707 states (over memory cap)
KLEE: WARNING: killing 9354 states (over memory cap)
KLEE: WARNING: killing 9345 states (over memory cap)
KLEE: WARNING: killing 9678 states (over memory cap)
KLEE: WARNING: killing 9809 states (over memory cap)
KLEE: WARNING: killing 9729 states (over memory cap)
KLEE: WARNING: killing 9449 states (over memory cap)
KLEE: WARNING: killing 9782 states (over memory cap)
KLEE: WARNING: killing 9771 states (over memory cap)
KLEE: WARNING: killing 9488 states (over memory cap)
KLEE: WARNING: killing 9685 states (over memory cap)
KLEE: WARNING: killing 9877 states (over memory cap)
KLEE: WARNING: killing 9529 states (over memory cap)
KLEE: WARNING: killing 9658 states (over memory cap)
KLEE: WARNING: killing 9307 states (over memory cap)
KLEE: WARNING: killing 9165 states (over memory cap)
KLEE: WARNING: killing 10041 states (over memory cap)
KLEE: WARNING: killing 9967 states (over memory cap)
KLEE: WARNING: killing 9553 states (over memory cap)
KLEE: WARNING: killing 9744 states (over memory cap)
KLEE: WARNING: killing 9874 states (over memory cap)
