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-dummy.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.: 124 117 892 4810
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.261945962906
Defining function snd_pcm_hw_constraint_integer as symbolic
Defining function snd_pcm_hw_constraint_minmax as symbolic
Defining function snd_pcm_lib_ioctl as symbolic
Defining function __phys_addr as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function snd_ctl_boolean_stereo_info as symbolic
Removed calls to 'snd_ctl_notify' (function is undefined)
Defining function snd_ctl_enum_info as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function del_timer as symbolic
Removed calls to 'tasklet_kill' (function is undefined)
Defining function ns_to_timeval as symbolic
Defining function hrtimer_cancel as symbolic
Defining function hrtimer_start as symbolic
Removed calls to 'snd_pcm_set_ops' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function snd_card_free as symbolic
Defining function snd_card_new as symbolic
Defining function printk as symbolic
Defining function sprintf as symbolic
Defining function snd_card_register as symbolic
Defining function snd_card_proc_new as symbolic
Defining function snd_info_get_str as symbolic
Defining function kstrtoull as symbolic
Defining function snd_info_get_line as symbolic
Defining function snd_iprintf as symbolic
Defining function snd_pcm_format_name 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
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'platform_driver_unregister' (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
Removed calls to 'free_pages' (function is undefined)
Defining function platform_device_register_full as symbolic
Defining function get_zeroed_page 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:
  strcmp
  strcpy
  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.286139011383
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 197 123 495 2913
INFO: Starting verification
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:5819: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_c65ff9ae-2305-41e1-9f19-e3ecbe623c84/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10217 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12706 states (over memory cap)
KLEE: WARNING: killing 12427 states (over memory cap)
KLEE: WARNING: killing 11640 states (over memory cap)
KLEE: WARNING: killing 11424 states (over memory cap)
KLEE: WARNING: killing 11966 states (over memory cap)
KLEE: WARNING: killing 11813 states (over memory cap)
KLEE: WARNING: killing 12666 states (over memory cap)
KLEE: WARNING: killing 12643 states (over memory cap)
KLEE: WARNING: killing 13364 states (over memory cap)
KLEE: WARNING: killing 13409 states (over memory cap)
KLEE: WARNING: killing 13015 states (over memory cap)
KLEE: WARNING: killing 13429 states (over memory cap)
KLEE: WARNING: killing 13469 states (over memory cap)
KLEE: WARNING: killing 13759 states (over memory cap)
KLEE: WARNING: killing 13312 states (over memory cap)
KLEE: WARNING: killing 13595 states (over memory cap)
KLEE: WARNING: killing 14010 states (over memory cap)
KLEE: WARNING: killing 13875 states (over memory cap)
KLEE: WARNING: killing 13492 states (over memory cap)
KLEE: WARNING: killing 13224 states (over memory cap)
KLEE: WARNING: killing 12474 states (over memory cap)
KLEE: WARNING: killing 13188 states (over memory cap)
KLEE: WARNING: killing 12804 states (over memory cap)
KLEE: WARNING: killing 13453 states (over memory cap)
KLEE: WARNING: killing 13072 states (over memory cap)
KLEE: WARNING: killing 13181 states (over memory cap)
KLEE: WARNING: killing 12860 states (over memory cap)
KLEE: WARNING: killing 13146 states (over memory cap)
KLEE: WARNING: killing 12947 states (over memory cap)
KLEE: WARNING: killing 13477 states (over memory cap)
KLEE: WARNING: killing 13703 states (over memory cap)
KLEE: WARNING: killing 13020 states (over memory cap)
KLEE: WARNING: killing 13067 states (over memory cap)
KLEE: WARNING: killing 13536 states (over memory cap)
KLEE: WARNING: killing 13584 states (over memory cap)
KLEE: WARNING: killing 13445 states (over memory cap)
KLEE: WARNING: killing 13311 states (over memory cap)
KLEE: WARNING: killing 12995 states (over memory cap)
KLEE: WARNING: killing 12981 states (over memory cap)
KLEE: WARNING: killing 12548 states (over memory cap)
KLEE: WARNING: killing 13431 states (over memory cap)
KLEE: WARNING: killing 13115 states (over memory cap)
KLEE: WARNING: killing 13342 states (over memory cap)
KLEE: WARNING: killing 13444 states (over memory cap)
KLEE: WARNING: killing 13374 states (over memory cap)
KLEE: WARNING: killing 13599 states (over memory cap)
KLEE: WARNING: killing 13113 states (over memory cap)
KLEE: WARNING: killing 13339 states (over memory cap)
KLEE: WARNING: killing 13266 states (over memory cap)
KLEE: WARNING: killing 13194 states (over memory cap)
KLEE: WARNING: killing 13301 states (over memory cap)
KLEE: WARNING: killing 13526 states (over memory cap)
KLEE: WARNING: killing 13154 states (over memory cap)
KLEE: WARNING: killing 12904 states (over memory cap)
KLEE: WARNING: killing 13484 states (over memory cap)
KLEE: WARNING: killing 13177 states (over memory cap)
KLEE: WARNING: killing 13164 states (over memory cap)
KLEE: WARNING: killing 13445 states (over memory cap)
KLEE: WARNING: killing 13197 states (over memory cap)
KLEE: WARNING: killing 13597 states (over memory cap)
KLEE: WARNING: killing 13410 states (over memory cap)
KLEE: WARNING: killing 12866 states (over memory cap)
KLEE: WARNING: killing 13557 states (over memory cap)
KLEE: WARNING: killing 12138 states (over memory cap)
KLEE: WARNING: killing 13124 states (over memory cap)
KLEE: WARNING: killing 13399 states (over memory cap)
KLEE: WARNING: killing 13444 states (over memory cap)
KLEE: WARNING: killing 13377 states (over memory cap)
KLEE: WARNING: killing 13364 states (over memory cap)
KLEE: WARNING: killing 12710 states (over memory cap)
KLEE: WARNING: killing 12756 states (over memory cap)
KLEE: WARNING: killing 13732 states (over memory cap)
KLEE: WARNING: killing 13485 states (over memory cap)
KLEE: WARNING: killing 13415 states (over memory cap)
KLEE: WARNING: killing 13805 states (over memory cap)
KLEE: WARNING: killing 12868 states (over memory cap)
KLEE: WARNING: killing 13554 states (over memory cap)
KLEE: WARNING: killing 13081 states (over memory cap)
KLEE: WARNING: killing 13362 states (over memory cap)
KLEE: WARNING: killing 12709 states (over memory cap)
KLEE: WARNING: killing 13157 states (over memory cap)
KLEE: WARNING: killing 13547 states (over memory cap)
KLEE: WARNING: killing 13364 states (over memory cap)
KLEE: WARNING: killing 12951 states (over memory cap)
KLEE: WARNING: killing 12936 states (over memory cap)
KLEE: WARNING: killing 13379 states (over memory cap)
KLEE: WARNING: killing 12966 states (over memory cap)
KLEE: WARNING: killing 13584 states (over memory cap)
KLEE: WARNING: killing 13743 states (over memory cap)
KLEE: WARNING: killing 13733 states (over memory cap)
KLEE: WARNING: killing 13034 states (over memory cap)
KLEE: WARNING: killing 13138 states (over memory cap)
KLEE: WARNING: killing 12608 states (over memory cap)
KLEE: WARNING: killing 13225 states (over memory cap)
KLEE: WARNING: killing 13608 states (over memory cap)
KLEE: WARNING: killing 13539 states (over memory cap)
KLEE: WARNING: killing 13074 states (over memory cap)
KLEE: WARNING: killing 13064 states (over memory cap)
KLEE: WARNING: killing 12992 states (over memory cap)
KLEE: WARNING: killing 13829 states (over memory cap)
KLEE: WARNING: killing 13305 states (over memory cap)
KLEE: WARNING: killing 13406 states (over memory cap)
KLEE: WARNING: killing 12878 states (over memory cap)
KLEE: WARNING: killing 13264 states (over memory cap)
KLEE: WARNING: killing 13590 states (over memory cap)
KLEE: WARNING: killing 13411 states (over memory cap)
KLEE: WARNING: killing 13063 states (over memory cap)
KLEE: WARNING: killing 13161 states (over memory cap)
KLEE: WARNING: killing 12925 states (over memory cap)
KLEE: WARNING: killing 13141 states (over memory cap)
KLEE: WARNING: killing 13523 states (over memory cap)
KLEE: WARNING: killing 13343 states (over memory cap)
KLEE: WARNING: killing 13388 states (over memory cap)
KLEE: WARNING: killing 13263 states (over memory cap)
KLEE: WARNING: killing 13026 states (over memory cap)
KLEE: WARNING: killing 13347 states (over memory cap)
KLEE: WARNING: killing 12777 states (over memory cap)
KLEE: WARNING: killing 13040 states (over memory cap)
KLEE: WARNING: killing 13475 states (over memory cap)
KLEE: WARNING: killing 13356 states (over memory cap)
KLEE: WARNING: killing 13621 states (over memory cap)
KLEE: WARNING: killing 13387 states (over memory cap)
KLEE: WARNING: killing 13155 states (over memory cap)
KLEE: WARNING: killing 13144 states (over memory cap)
KLEE: WARNING: killing 13135 states (over memory cap)
KLEE: WARNING: killing 13067 states (over memory cap)
KLEE: WARNING: killing 13003 states (over memory cap)
KLEE: WARNING: killing 13658 states (over memory cap)
KLEE: WARNING: killing 13425 states (over memory cap)
KLEE: WARNING: killing 13527 states (over memory cap)
KLEE: WARNING: killing 13022 states (over memory cap)
KLEE: WARNING: killing 13614 states (over memory cap)
KLEE: WARNING: killing 13107 states (over memory cap)
KLEE: WARNING: killing 13152 states (over memory cap)
KLEE: WARNING: killing 13087 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4758: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:5467: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13072 states (over memory cap)
KLEE: WARNING: killing 13617 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4474: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4786: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4818: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12889 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4738: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4786: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4769: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4540: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4500: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13431 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4770: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4577: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4487: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13693 states (over memory cap)
KLEE: WARNING: killing 12974 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4819: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4759: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13348 states (over memory cap)
KLEE: WARNING: killing 13501 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4742: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13767 states (over memory cap)
KLEE: WARNING: killing 13267 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4746: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13858 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-_Xmcvk/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-sound--drivers--snd-dummy.ko-entry_point_true-unreach-call.cil.out.c:4683: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12646 states (over memory cap)
