bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--platform--x86--thinkpad_acpi.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.: 976 588 6853 30003
Removed infinite loop in hotkey_init
Removed infinite loop in volume_create_alsa_mixer
Removed infinite loop in tpacpi_new_rfkill
Removed infinite loop in tpacpi_destroy_rfkill
Removed infinite loop in hotkey_inputdev_open
Removed infinite loop in ldv_stop
Removed infinite loop in thinkpad_acpi_init_banner
Removed infinite loop in ibm_init
Removed infinite loop in register_tpacpi_subdriver
Removed infinite loop in setup_acpi_notify
Removed infinite loop in ibm_exit
Removed infinite loop in tpacpi_acpi_handle_locate
INFO: Compilation, preparation and instrumentation time: 1.08401489258
Defining function acpi_get_handle as symbolic
Defining function printk as symbolic
Removed calls to 'ldv__builtin_va_start' (function is undefined)
Removed calls to 'ldv__builtin_va_arg' (function is undefined)
Removed calls to 'ldv__builtin_va_end' (function is undefined)
Defining function acpi_evaluate_object as symbolic
Defining function acpi_format_exception as symbolic
Defining function cancel_delayed_work as symbolic
Defining function mod_delayed_work_on as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function ec_write as symbolic
Defining function ec_read as symbolic
Defining function mutex_lock_killable as symbolic
Defining function queue_work_on as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'input_set_capability' (function is undefined)
Removed calls to 'input_event' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Defining function sysfs_create_group as symbolic
Defining function driver_create_file as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Defining function kthread_create_on_node as symbolic
Defining function wake_up_process as symbolic
Defining function kthread_stop as symbolic
Defining function set_freezable as symbolic
Defining function msleep_interruptible as symbolic
Defining function kthread_freezable_should_stop as symbolic
Defining function kthread_should_stop as symbolic
Removed calls to 'backlight_force_update' (function is undefined)
Removed calls to 'snd_ctl_notify' (function is undefined)
Defining function nvram_read_byte as symbolic
Defining function snd_card_new as symbolic
Defining function strlcpy as symbolic
Defining function snprintf as symbolic
Defining function snd_ctl_new1 as symbolic
Defining function snd_ctl_add as symbolic
Defining function snd_card_register as symbolic
Defining function snd_card_free as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function pid_vnr as symbolic
Defining function acpi_video_get_backlight_type as symbolic
Defining function backlight_device_register as symbolic
Removed calls to 'led_classdev_unregister' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Defining function led_classdev_register as symbolic
Defining function device_create_file as symbolic
Removed calls to 'rfkill_init_sw_state' (function is undefined)
Removed calls to 'rfkill_destroy' (function is undefined)
Defining function rfkill_alloc as symbolic
Defining function rfkill_set_hw_state as symbolic
Defining function rfkill_register as symbolic
Removed calls to 'rfkill_unregister' (function is undefined)
Defining function seq_printf as symbolic
Defining function skip_spaces as symbolic
Defining function simple_strtoul as symbolic
Defining function sprintf as symbolic
Removed calls to 'sysfs_notify' (function is undefined)
Defining function rfkill_set_sw_state as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function sscanf as symbolic
Defining function acpi_bus_generate_netlink_event as symbolic
Defining function capable as symbolic
Removed calls to 'device_remove_file' (function is undefined)
Defining function strstr as symbolic
Removed calls to 'backlight_device_unregister' (function is undefined)
Removed calls to 'nvram_write_byte' (function is undefined)
Defining function snd_ctl_boolean_mono_info as symbolic
Removed calls to 'driver_remove_file' (function is undefined)
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function single_release as symbolic
Defining function PDE_DATA as symbolic
Defining function single_open as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'delayed_work_timer_fn' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function ldv_release_29 as symbolic
Defining function ldv_probe_29 as symbolic
Defining function ldv_resume_68 as symbolic
Defining function ldv_suspend_68 as symbolic
Defining function ldv_remove_68 as symbolic
Defining function ldv_probe_68 as symbolic
Defining function ldv_suspend_late_69 as symbolic
Defining function ldv_restore_early_69 as symbolic
Defining function ldv_resume_early_69 as symbolic
Defining function ldv_thaw_early_69 as symbolic
Defining function ldv_resume_noirq_69 as symbolic
Defining function ldv_freeze_noirq_69 as symbolic
Defining function ldv_prepare_69 as symbolic
Defining function ldv_freeze_late_69 as symbolic
Defining function ldv_thaw_noirq_69 as symbolic
Defining function ldv_poweroff_noirq_69 as symbolic
Defining function ldv_poweroff_late_69 as symbolic
Defining function ldv_restore_noirq_69 as symbolic
Defining function ldv_suspend_noirq_69 as symbolic
Defining function ldv_complete_69 as symbolic
Defining function ldv_release_59 as symbolic
Defining function ldv_probe_59 as symbolic
Removed calls to 'input_unregister_device' (function is undefined)
Removed calls to 'input_free_device' (function is undefined)
Removed calls to 'hwmon_device_unregister' (function is undefined)
Removed calls to 'platform_device_unregister' (function is undefined)
Removed calls to 'platform_driver_unregister' (function is undefined)
Removed calls to 'remove_proc_entry' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function proc_mkdir as symbolic
Defining function hwmon_device_register as symbolic
Defining function input_allocate_device as symbolic
Defining function input_register_device as symbolic
Defining function proc_create_data as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'acpi_bus_unregister_driver' (function is undefined)
Defining function acpi_remove_notify_handler as symbolic
Defining function acpi_bus_get_device as symbolic
Defining function acpi_install_notify_handler as symbolic
Defining function acpi_bus_register_driver as symbolic
Defining function acpi_get_devices as symbolic
Defining function acpi_device_hid as symbolic
Defining function platform_device_register_full as symbolic
Defining function __platform_driver_register as symbolic
Defining function dmi_name_in_vendors as symbolic
Defining function dmi_get_system_info as symbolic
Defining function kstrdup as symbolic
Defining function dmi_find_device as symbolic
Defining function strncasecmp as symbolic
Defining function queue_delayed_work_on as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  strchr
  strcmp
  strcpy
  strcspn
  strlen
  strncmp
  __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: 1.3125679493
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1073 577 3977 19232
INFO: Starting verification
KLEE: WARNING ONCE: function "hotkey_init" has inline asm
KLEE: WARNING ONCE: function "led_init" has inline asm
KLEE: WARNING ONCE: function "volume_init" has inline asm
KLEE: WARNING ONCE: function "tpacpi_new_rfkill" has inline asm
KLEE: WARNING ONCE: function "tpacpi_destroy_rfkill" has inline asm
KLEE: WARNING ONCE: function "hotkey_inputdev_open" has inline asm
KLEE: WARNING ONCE: function "hotkey_enable_show" has inline asm
KLEE: WARNING ONCE: function "hotkey_enable_store" has inline asm
KLEE: WARNING ONCE: function "hotkey_bios_mask_show" has inline asm
KLEE: WARNING ONCE: function "hotkey_mask_store" has inline asm
KLEE: WARNING ONCE: function "hotkey_source_mask_store" has inline asm
KLEE: WARNING ONCE: function "hotkey_poll_freq_store" has inline asm
KLEE: WARNING ONCE: function "hotkey_write" has inline asm
KLEE: WARNING ONCE: function "hotkey_enabledisable_warn" has inline asm
KLEE: WARNING ONCE: function "tpacpi_rfk_sysfs_enable_store" has inline asm
KLEE: WARNING ONCE: function "printk_deprecated_rfkill_attribute" has inline asm
KLEE: WARNING ONCE: function "tpacpi_rfk_procfs_write" has inline asm
KLEE: WARNING ONCE: function "brightness_write" has inline asm
KLEE: WARNING ONCE: function "volume_write" has inline asm
KLEE: WARNING ONCE: function "fan_pwm1_enable_store" has inline asm
KLEE: WARNING ONCE: function "fan_pwm1_store" has inline asm
KLEE: WARNING ONCE: function "fan_write" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "tpacpi_acpi_handle_locate" has inline asm
KLEE: WARNING ONCE: function "ibm_exit" has inline asm
KLEE: WARNING: undefined reference to variable: acpi_root_dir
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: ERROR: unable to load symbol(acpi_root_dir) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-QqgMgL/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "hotkey_init" has inline asm
KLEE: WARNING ONCE: function "led_init" has inline asm
KLEE: WARNING ONCE: function "volume_init" has inline asm
KLEE: WARNING ONCE: function "tpacpi_new_rfkill" has inline asm
KLEE: WARNING ONCE: function "tpacpi_destroy_rfkill" has inline asm
KLEE: WARNING ONCE: function "hotkey_inputdev_open" has inline asm
KLEE: WARNING ONCE: function "hotkey_enable_show" has inline asm
KLEE: WARNING ONCE: function "hotkey_enable_store" has inline asm
KLEE: WARNING ONCE: function "hotkey_bios_mask_show" has inline asm
KLEE: WARNING ONCE: function "hotkey_mask_store" has inline asm
KLEE: WARNING ONCE: function "hotkey_source_mask_store" has inline asm
KLEE: WARNING ONCE: function "hotkey_poll_freq_store" has inline asm
KLEE: WARNING ONCE: function "hotkey_write" has inline asm
KLEE: WARNING ONCE: function "hotkey_enabledisable_warn" has inline asm
KLEE: WARNING ONCE: function "tpacpi_rfk_sysfs_enable_store" has inline asm
KLEE: WARNING ONCE: function "printk_deprecated_rfkill_attribute" has inline asm
KLEE: WARNING ONCE: function "tpacpi_rfk_procfs_write" has inline asm
KLEE: WARNING ONCE: function "brightness_write" has inline asm
KLEE: WARNING ONCE: function "volume_write" has inline asm
KLEE: WARNING ONCE: function "fan_pwm1_enable_store" has inline asm
KLEE: WARNING ONCE: function "fan_pwm1_store" has inline asm
KLEE: WARNING ONCE: function "fan_write" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "tpacpi_acpi_handle_locate" has inline asm
KLEE: WARNING ONCE: function "ibm_exit" has inline asm
KLEE: WARNING: undefined reference to variable: acpi_root_dir
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: ERROR: unable to load symbol(acpi_root_dir) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 2.7139840126
