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-drivers--platform--x86--ideapad-laptop.ko-main.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.: 143 99 972 3826
INFO: Compilation, preparation and instrumentation time: 0.233469963074
Removed calls to 'acpi_bus_unregister_driver' (function is undefined)
Defining function single_release as symbolic
Defining function seq_read as symbolic
Defining function seq_lseek as symbolic
Defining function ldv_ideapad_pm_suspend_late_2 as symbolic
Defining function ldv_ideapad_pm_restore_early_2 as symbolic
Defining function ldv_ideapad_pm_resume_early_2 as symbolic
Defining function ldv_ideapad_pm_thaw_early_2 as symbolic
Defining function ldv_ideapad_pm_resume_noirq_2 as symbolic
Defining function ldv_ideapad_pm_freeze_noirq_2 as symbolic
Defining function ldv_ideapad_pm_prepare_2 as symbolic
Defining function ldv_ideapad_pm_freeze_2 as symbolic
Defining function ldv_ideapad_pm_freeze_late_2 as symbolic
Defining function ldv_ideapad_pm_thaw_noirq_2 as symbolic
Defining function ldv_ideapad_pm_poweroff_2 as symbolic
Defining function ldv_ideapad_pm_poweroff_noirq_2 as symbolic
Defining function ldv_ideapad_pm_poweroff_late_2 as symbolic
Defining function ldv_ideapad_pm_restore_noirq_2 as symbolic
Defining function ldv_ideapad_pm_suspend_2 as symbolic
Defining function ldv_ideapad_pm_suspend_noirq_2 as symbolic
Defining function ldv_ideapad_pm_complete_2 as symbolic
Removed calls to 'backlight_force_update' (function is undefined)
Removed calls to 'platform_device_del' (function is undefined)
Removed calls to 'platform_device_put' (function is undefined)
Removed calls to 'sparse_keymap_free' (function is undefined)
Removed calls to 'input_free_device' (function is undefined)
Removed calls to 'rfkill_init_sw_state' (function is undefined)
Removed calls to 'rfkill_destroy' (function is undefined)
Removed calls to 'input_unregister_device' (function is undefined)
Removed calls to 'debugfs_remove_recursive' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to 'backlight_device_unregister' (function is undefined)
Defining function dev_get_drvdata as symbolic
Removed calls to 'schedule' (function is undefined)
Defining function printk as symbolic
Defining function acpi_evaluate_integer as symbolic
Defining function acpi_evaluate_object as symbolic
Defining function acpi_bus_register_driver as symbolic
Removed calls to 'rfkill_unregister' (function is undefined)
Defining function dev_set_drvdata as symbolic
Defining function acpi_video_backlight_support as symbolic
Defining function backlight_device_register as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function i8042_command as symbolic
Defining function sparse_keymap_report_event as symbolic
Defining function rfkill_set_hw_state as symbolic
Defining function rfkill_alloc as symbolic
Defining function rfkill_register as symbolic
Defining function input_allocate_device as symbolic
Defining function sparse_keymap_setup as symbolic
Defining function input_register_device as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Defining function platform_device_alloc as symbolic
Defining function platform_device_add as symbolic
Defining function sysfs_create_group as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Defining function sprintf as symbolic
Defining function sscanf as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.197660923004
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 222 126 567 2439
INFO: Starting verification
KLEE: WARNING ONCE: function "ideapad_acpi_notify" has inline asm
KLEE: WARNING ONCE: function "ideapad_acpi_add" has inline asm
KLEE: ERROR: /tmp/symbiotic-_8h4GW/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--platform--x86--ideapad-laptop.ko-main.cil.out.c:4546: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_8h4GW/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--platform--x86--ideapad-laptop.ko-main.cil.out.c:4843: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_8h4GW/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--platform--x86--ideapad-laptop.ko-main.cil.out.c:5150: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_8h4GW/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--platform--x86--ideapad-laptop.ko-main.cil.out.c:5018: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_8h4GW/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--platform--x86--ideapad-laptop.ko-main.cil.out.c:4424: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-_8h4GW/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--platform--x86--ideapad-laptop.ko-main.cil.out.c:4473: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 14815 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 16772 states (over memory cap)
KLEE: WARNING: killing 15781 states (over memory cap)
KLEE: WARNING: killing 15731 states (over memory cap)
KLEE: WARNING: killing 15101 states (over memory cap)
KLEE: WARNING: killing 14363 states (over memory cap)
KLEE: WARNING: killing 15483 states (over memory cap)
KLEE: WARNING: killing 15788 states (over memory cap)
KLEE: WARNING: killing 16320 states (over memory cap)
KLEE: WARNING: killing 15476 states (over memory cap)
KLEE: WARNING: killing 15893 states (over memory cap)
KLEE: WARNING: killing 15515 states (over memory cap)
KLEE: WARNING: killing 15820 states (over memory cap)
KLEE: WARNING: killing 16465 states (over memory cap)
KLEE: WARNING: killing 16090 states (over memory cap)
KLEE: WARNING: killing 16283 states (over memory cap)
KLEE: WARNING: killing 16142 states (over memory cap)
KLEE: WARNING: killing 16791 states (over memory cap)
KLEE: WARNING: killing 17440 states (over memory cap)
KLEE: WARNING: killing 17192 states (over memory cap)
KLEE: WARNING: killing 16938 states (over memory cap)
KLEE: WARNING: killing 16803 states (over memory cap)
KLEE: WARNING: killing 17339 states (over memory cap)
KLEE: WARNING: killing 17311 states (over memory cap)
KLEE: WARNING: killing 17517 states (over memory cap)
KLEE: WARNING: killing 17155 states (over memory cap)
KLEE: WARNING: killing 17917 states (over memory cap)
KLEE: WARNING: killing 17329 states (over memory cap)
KLEE: WARNING: killing 16967 states (over memory cap)
KLEE: WARNING: killing 16727 states (over memory cap)
KLEE: WARNING: killing 16704 states (over memory cap)
KLEE: WARNING: killing 16453 states (over memory cap)
KLEE: WARNING: killing 17540 states (over memory cap)
KLEE: WARNING: killing 16177 states (over memory cap)
KLEE: WARNING: killing 16151 states (over memory cap)
KLEE: WARNING: killing 15795 states (over memory cap)
KLEE: WARNING: killing 15990 states (over memory cap)
KLEE: WARNING: killing 16405 states (over memory cap)
KLEE: WARNING: killing 16598 states (over memory cap)
KLEE: WARNING: killing 15911 states (over memory cap)
KLEE: WARNING: killing 16982 states (over memory cap)
KLEE: WARNING: killing 16519 states (over memory cap)
KLEE: WARNING: killing 16269 states (over memory cap)
KLEE: WARNING: killing 15592 states (over memory cap)
KLEE: WARNING: killing 16005 states (over memory cap)
KLEE: WARNING: killing 16737 states (over memory cap)
KLEE: WARNING: killing 16823 states (over memory cap)
KLEE: WARNING: killing 16150 states (over memory cap)
KLEE: WARNING: killing 16228 states (over memory cap)
KLEE: WARNING: killing 16420 states (over memory cap)
KLEE: WARNING: killing 16399 states (over memory cap)
KLEE: WARNING: killing 16595 states (over memory cap)
KLEE: WARNING: killing 17005 states (over memory cap)
KLEE: WARNING: killing 16551 states (over memory cap)
KLEE: WARNING: killing 16535 states (over memory cap)
KLEE: WARNING: killing 17040 states (over memory cap)
KLEE: WARNING: killing 16056 states (over memory cap)
KLEE: WARNING: killing 16464 states (over memory cap)
KLEE: WARNING: killing 16443 states (over memory cap)
KLEE: WARNING: killing 15988 states (over memory cap)
KLEE: WARNING: killing 16603 states (over memory cap)
KLEE: WARNING: killing 17225 states (over memory cap)
KLEE: WARNING: killing 17210 states (over memory cap)
KLEE: WARNING: killing 16332 states (over memory cap)
KLEE: WARNING: killing 16418 states (over memory cap)
KLEE: WARNING: killing 17038 states (over memory cap)
KLEE: WARNING: killing 16163 states (over memory cap)
KLEE: WARNING: killing 16248 states (over memory cap)
KLEE: WARNING: killing 16756 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 17032 states (over memory cap)
KLEE: WARNING: killing 15961 states (over memory cap)
KLEE: WARNING: killing 16458 states (over memory cap)
KLEE: WARNING: killing 16126 states (over memory cap)
KLEE: WARNING: killing 16528 states (over memory cap)
KLEE: WARNING: killing 16194 states (over memory cap)
KLEE: WARNING: killing 16177 states (over memory cap)
KLEE: WARNING: killing 16364 states (over memory cap)
KLEE: WARNING: killing 16758 states (over memory cap)
KLEE: WARNING: killing 16117 states (over memory cap)
KLEE: WARNING: killing 16098 states (over memory cap)
KLEE: WARNING: killing 16280 states (over memory cap)
KLEE: WARNING: killing 16161 states (over memory cap)
KLEE: WARNING: killing 16034 states (over memory cap)
KLEE: WARNING: killing 16119 states (over memory cap)
KLEE: WARNING: killing 16205 states (over memory cap)
KLEE: WARNING: killing 16286 states (over memory cap)
KLEE: WARNING: killing 16475 states (over memory cap)
KLEE: WARNING: killing 16666 states (over memory cap)
KLEE: WARNING: killing 16438 states (over memory cap)
KLEE: WARNING: killing 16933 states (over memory cap)
KLEE: WARNING: killing 16193 states (over memory cap)
KLEE: WARNING: killing 15861 states (over memory cap)
KLEE: WARNING: killing 16878 states (over memory cap)
KLEE: WARNING: killing 16858 states (over memory cap)
KLEE: WARNING: killing 16531 states (over memory cap)
KLEE: WARNING: killing 16508 states (over memory cap)
KLEE: WARNING: killing 16802 states (over memory cap)
KLEE: WARNING: killing 16890 states (over memory cap)
KLEE: WARNING: killing 16458 states (over memory cap)
KLEE: WARNING: killing 15726 states (over memory cap)
KLEE: WARNING: killing 16115 states (over memory cap)
KLEE: WARNING: killing 16190 states (over memory cap)
KLEE: WARNING: killing 16175 states (over memory cap)
KLEE: WARNING: killing 16255 states (over memory cap)
KLEE: WARNING: killing 16236 states (over memory cap)
KLEE: WARNING: killing 16725 states (over memory cap)
KLEE: WARNING: killing 16096 states (over memory cap)
KLEE: WARNING: killing 16079 states (over memory cap)
KLEE: WARNING: killing 16366 states (over memory cap)
KLEE: WARNING: killing 15436 states (over memory cap)
KLEE: WARNING: killing 15920 states (over memory cap)
KLEE: WARNING: killing 16605 states (over memory cap)
KLEE: WARNING: killing 16788 states (over memory cap)
KLEE: WARNING: killing 16675 states (over memory cap)
KLEE: WARNING: killing 16454 states (over memory cap)
KLEE: WARNING: killing 16843 states (over memory cap)
KLEE: WARNING: killing 16421 states (over memory cap)
KLEE: WARNING: killing 17108 states (over memory cap)
KLEE: WARNING: killing 16483 states (over memory cap)
KLEE: WARNING: killing 16570 states (over memory cap)
KLEE: WARNING: killing 16450 states (over memory cap)
KLEE: WARNING: killing 16332 states (over memory cap)
KLEE: WARNING: killing 15922 states (over memory cap)
KLEE: WARNING: killing 16603 states (over memory cap)
KLEE: WARNING: killing 16283 states (over memory cap)
KLEE: WARNING: killing 16461 states (over memory cap)
KLEE: WARNING: killing 16244 states (over memory cap)
KLEE: WARNING: killing 16323 states (over memory cap)
KLEE: WARNING: killing 16502 states (over memory cap)
KLEE: WARNING: killing 15987 states (over memory cap)
KLEE: WARNING: killing 15774 states (over memory cap)
KLEE: WARNING: killing 16055 states (over memory cap)
KLEE: WARNING: killing 16226 states (over memory cap)
KLEE: WARNING: killing 16803 states (over memory cap)
KLEE: WARNING: killing 16586 states (over memory cap)
KLEE: WARNING: killing 16277 states (over memory cap)
KLEE: WARNING: killing 16550 states (over memory cap)
KLEE: WARNING: killing 16342 states (over memory cap)
KLEE: WARNING: killing 16317 states (over memory cap)
KLEE: WARNING: killing 16504 states (over memory cap)
KLEE: WARNING: killing 16878 states (over memory cap)
KLEE: WARNING: killing 16858 states (over memory cap)
KLEE: WARNING: killing 16357 states (over memory cap)
KLEE: WARNING: killing 16247 states (over memory cap)
KLEE: WARNING: killing 16517 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 16191 states (over memory cap)
KLEE: WARNING: killing 16170 states (over memory cap)
KLEE: WARNING: killing 16928 states (over memory cap)
KLEE: WARNING: killing 16426 states (over memory cap)
KLEE: WARNING: killing 16215 states (over memory cap)
KLEE: WARNING: killing 16587 states (over memory cap)
KLEE: WARNING: killing 15888 states (over memory cap)
KLEE: WARNING: killing 16350 states (over memory cap)
KLEE: WARNING: killing 15951 states (over memory cap)
KLEE: WARNING: killing 16316 states (over memory cap)
KLEE: WARNING: killing 16393 states (over memory cap)
KLEE: WARNING: killing 15797 states (over memory cap)
KLEE: WARNING: killing 16641 states (over memory cap)
KLEE: WARNING: killing 16334 states (over memory cap)
KLEE: WARNING: killing 16220 states (over memory cap)
KLEE: WARNING: killing 15921 states (over memory cap)
KLEE: WARNING: killing 17048 states (over memory cap)
KLEE: WARNING: killing 16834 states (over memory cap)
KLEE: WARNING: killing 16630 states (over memory cap)
KLEE: WARNING: killing 16706 states (over memory cap)
KLEE: WARNING: killing 16601 states (over memory cap)
KLEE: WARNING: killing 16485 states (over memory cap)
KLEE: WARNING: killing 15993 states (over memory cap)
KLEE: WARNING: killing 16347 states (over memory cap)
KLEE: WARNING: killing 16047 states (over memory cap)
KLEE: WARNING: killing 16502 states (over memory cap)
KLEE: WARNING: killing 16392 states (over memory cap)
