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-drivers--acpi--processor.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.: 218 157 2006 10759
Removed infinite loop in paravirt_read_msr
Removed infinite loop in wbinvd
Removed infinite loop in arch_safe_halt
Removed infinite loop in arch_local_irq_disable
Removed infinite loop in paravirt_write_msr
Removed infinite loop in arch_local_irq_enable
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.431197881699
Removed calls to 'acpi_debug_print' (function is undefined)
Defining function cpufreq_update_policy as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function find_next_bit as symbolic
Defining function cpufreq_get_policy as symbolic
Defining function cpumask_next_and as symbolic
Defining function work_on_cpu as symbolic
Defining function printk as symbolic
Removed calls to 'acpi_exception' (function is undefined)
Defining function acpi_has_method as symbolic
Defining function acpi_evaluate_integer as symbolic
Defining function acpi_evaluate_object as symbolic
Defining function acpi_extract_package as symbolic
Removed calls to 'module_put' (function is undefined)
Defining function try_module_get as symbolic
Defining function acpi_os_write_port as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'free_cpumask_var' (function is undefined)
Defining function zalloc_cpumask_var as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function acpi_bus_get_device as symbolic
Removed calls to 'sysfs_remove_link' (function is undefined)
Removed calls to 'thermal_cooling_device_unregister' (function is undefined)
Removed calls to 'cpuidle_pause_and_lock' (function is undefined)
Removed calls to 'cpuidle_disable_device' (function is undefined)
Removed calls to 'cpuidle_resume_and_unlock' (function is undefined)
Defining function alloc_cpumask_var as symbolic
Defining function set_cpus_allowed_ptr as symbolic
Removed calls to 'acpi_processor_power_init_bm_check' (function is undefined)
Removed calls to 'mark_tsc_unstable' (function is undefined)
Defining function cpuidle_enable_device as symbolic
Defining function smp_call_function_single as symbolic
Defining function clockevents_notify as symbolic
Defining function acpi_processor_ffh_cstate_probe as symbolic
Defining function snprintf as symbolic
Defining function acpi_evaluate_ost as symbolic
Defining function cpuidle_get_driver as symbolic
Defining function thermal_cooling_device_register as symbolic
Defining function sysfs_create_link as symbolic
Defining function dev_err as symbolic
Defining function acpi_install_notify_handler as symbolic
Removed calls to 'cpuidle_unregister_device' (function is undefined)
Removed calls to 'cpuidle_unregister_driver' (function is undefined)
Defining function acpi_bus_generate_netlink_event as symbolic
Removed calls to 'get_online_cpus' (function is undefined)
Removed calls to 'put_online_cpus' (function is undefined)
Removed calls to 'trace_hardirqs_on' (function is undefined)
Removed calls to 'sched_clock_idle_sleep_event' (function is undefined)
Removed calls to 'sched_clock_idle_wakeup_event' (function is undefined)
Removed calls to 'leave_mm' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'trace_hardirqs_off' (function is undefined)
Removed calls to 'stop_critical_timings' (function is undefined)
Removed calls to 'acpi_processor_ffh_cstate_enter' (function is undefined)
Removed calls to 'start_critical_timings' (function is undefined)
Defining function __bitmap_weight as symbolic
Defining function dmi_check_system as symbolic
Defining function cpuidle_register_driver as symbolic
Defining function acpi_remove_notify_handler as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'unregister_cpu_notifier' (function is undefined)
Removed calls to 'unregister_syscore_ops' (function is undefined)
Removed calls to 'driver_unregister' (function is undefined)
Removed calls to 'register_syscore_ops' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function driver_register as symbolic
Defining function register_cpu_notifier as symbolic
Defining function cpufreq_register_notifier as symbolic
Defining function cpufreq_unregister_notifier as symbolic
Defining function ldv_release_4 as symbolic
Defining function ldv_probe_4 as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  strncpy
  __kmalloc
  __memcpy
  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.433627128601
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 262 141 1002 5927
INFO: Starting verification
KLEE: WARNING ONCE: function "processor_get_cur_state" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_set_throttling" has inline asm
KLEE: WARNING ONCE: function "cpufreq_set_cur_state" has inline asm
KLEE: WARNING ONCE: function "phys_package_first_cpu" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_throttling_notifier" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_get_bios_limit" has inline asm
KLEE: WARNING ONCE: function "paravirt_read_msr" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_preregister_performance" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_register_performance" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_unregister_performance" has inline asm
KLEE: WARNING ONCE: function "acpi_cpu_soft_notify" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_hotplug" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_get_throttling" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_get_power_info" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_setup_cpuidle_cx" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_get_throttling_info" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_power_exit" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_cst_has_changed" has inline asm
KLEE: WARNING ONCE: function "acpi_idle_enter_c1" has inline asm
KLEE: WARNING ONCE: function "acpi_idle_play_dead" has inline asm
KLEE: WARNING ONCE: function "acpi_idle_enter_simple" has inline asm
KLEE: WARNING ONCE: function "acpi_idle_enter_bm" has inline asm
KLEE: WARNING ONCE: function "acpi_safe_halt" has inline asm
KLEE: WARNING ONCE: function "wbinvd" has inline asm
KLEE: WARNING ONCE: function "acpi_idle_do_entry" has inline asm
KLEE: WARNING ONCE: function "arch_safe_halt" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_disable" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_get_throttling_fadt" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_set_throttling_fadt" has inline asm
KLEE: WARNING ONCE: function "arch_local_irq_enable" has inline asm
KLEE: WARNING ONCE: function "acpi_thermal_cpufreq_notifier" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_ppc_notifier" has inline asm
KLEE: WARNING ONCE: function "acpi_processor_throttling_init" 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_8174eb93-465b-4669-a983-4b60e5036e5b/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-SvkmFt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--acpi--processor.ko-entry_point_true-unreach-call.cil.out.c:5087: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-SvkmFt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--acpi--processor.ko-entry_point_true-unreach-call.cil.out.c:4212: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-SvkmFt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--acpi--processor.ko-entry_point_true-unreach-call.cil.out.c:4364: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-SvkmFt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--acpi--processor.ko-entry_point_true-unreach-call.cil.out.c:9263: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-SvkmFt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--acpi--processor.ko-entry_point_true-unreach-call.cil.out.c:9466: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-SvkmFt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--acpi--processor.ko-entry_point_true-unreach-call.cil.out.c:9433: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-SvkmFt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--acpi--processor.ko-entry_point_true-unreach-call.cil.out.c:9407: 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 13962 states (over memory cap)
KLEE: WARNING: killing 9790 states (over memory cap)
KLEE: WARNING: killing 9696 states (over memory cap)
KLEE: WARNING: killing 9253 states (over memory cap)
KLEE: WARNING: killing 9578 states (over memory cap)
KLEE: WARNING: killing 9420 states (over memory cap)
KLEE: WARNING: killing 9327 states (over memory cap)
KLEE: WARNING: killing 9307 states (over memory cap)
KLEE: WARNING: killing 9149 states (over memory cap)
KLEE: WARNING: killing 9476 states (over memory cap)
KLEE: WARNING: killing 9459 states (over memory cap)
KLEE: WARNING: killing 10473 states (over memory cap)
KLEE: WARNING: killing 10113 states (over memory cap)
KLEE: WARNING: killing 10231 states (over memory cap)
KLEE: WARNING: killing 10629 states (over memory cap)
KLEE: WARNING: killing 10548 states (over memory cap)
KLEE: WARNING: killing 10738 states (over memory cap)
KLEE: WARNING: killing 10519 states (over memory cap)
KLEE: WARNING: killing 10982 states (over memory cap)
KLEE: WARNING: killing 10766 states (over memory cap)
KLEE: WARNING: killing 10478 states (over memory cap)
KLEE: WARNING: killing 10260 states (over memory cap)
KLEE: WARNING: killing 10649 states (over memory cap)
KLEE: WARNING: killing 10702 states (over memory cap)
KLEE: WARNING: killing 10216 states (over memory cap)
KLEE: WARNING: killing 10338 states (over memory cap)
KLEE: WARNING: killing 9920 states (over memory cap)
KLEE: WARNING: killing 10444 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 10550 states (over memory cap)
KLEE: WARNING: killing 9935 states (over memory cap)
KLEE: WARNING: killing 10187 states (over memory cap)
KLEE: WARNING: killing 10373 states (over memory cap)
KLEE: WARNING: killing 10223 states (over memory cap)
KLEE: WARNING: killing 10011 states (over memory cap)
KLEE: WARNING: killing 10261 states (over memory cap)
KLEE: WARNING: killing 10380 states (over memory cap)
KLEE: WARNING: killing 10702 states (over memory cap)
KLEE: WARNING: killing 9957 states (over memory cap)
KLEE: WARNING: killing 10340 states (over memory cap)
KLEE: WARNING: killing 10463 states (over memory cap)
KLEE: WARNING: killing 10578 states (over memory cap)
KLEE: WARNING: killing 10436 states (over memory cap)
KLEE: WARNING: killing 10749 states (over memory cap)
KLEE: WARNING: killing 9944 states (over memory cap)
KLEE: WARNING: killing 10330 states (over memory cap)
KLEE: WARNING: killing 10777 states (over memory cap)
KLEE: WARNING: killing 10696 states (over memory cap)
KLEE: WARNING: killing 10491 states (over memory cap)
KLEE: WARNING: killing 10478 states (over memory cap)
KLEE: WARNING: killing 10725 states (over memory cap)
KLEE: WARNING: killing 10583 states (over memory cap)
KLEE: WARNING: killing 10570 states (over memory cap)
KLEE: WARNING: killing 10166 states (over memory cap)
KLEE: WARNING: killing 10937 states (over memory cap)
KLEE: WARNING: killing 10536 states (over memory cap)
KLEE: WARNING: killing 10453 states (over memory cap)
KLEE: WARNING: killing 10444 states (over memory cap)
KLEE: WARNING: killing 10694 states (over memory cap)
KLEE: WARNING: killing 10094 states (over memory cap)
KLEE: WARNING: killing 10599 states (over memory cap)
KLEE: WARNING: killing 10460 states (over memory cap)
KLEE: WARNING: killing 10381 states (over memory cap)
KLEE: WARNING: killing 10563 states (over memory cap)
KLEE: WARNING: killing 10229 states (over memory cap)
KLEE: WARNING: killing 10471 states (over memory cap)
KLEE: WARNING: killing 10525 states (over memory cap)
KLEE: WARNING: killing 10511 states (over memory cap)
KLEE: WARNING: killing 10823 states (over memory cap)
KLEE: WARNING: killing 10302 states (over memory cap)
KLEE: WARNING: killing 10352 states (over memory cap)
KLEE: WARNING: killing 10597 states (over memory cap)
KLEE: WARNING: killing 10327 states (over memory cap)
KLEE: WARNING: killing 10831 states (over memory cap)
KLEE: WARNING: killing 10052 states (over memory cap)
KLEE: WARNING: killing 10485 states (over memory cap)
KLEE: WARNING: killing 10470 states (over memory cap)
KLEE: WARNING: killing 10779 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10377 states (over memory cap)
KLEE: WARNING: killing 10244 states (over memory cap)
KLEE: WARNING: killing 10483 states (over memory cap)
KLEE: WARNING: killing 10534 states (over memory cap)
KLEE: WARNING: killing 10525 states (over memory cap)
KLEE: WARNING: killing 9945 states (over memory cap)
KLEE: WARNING: killing 10625 states (over memory cap)
KLEE: WARNING: killing 10617 states (over memory cap)
KLEE: WARNING: killing 10669 states (over memory cap)
KLEE: WARNING: killing 10470 states (over memory cap)
KLEE: WARNING: killing 10525 states (over memory cap)
KLEE: WARNING: killing 10511 states (over memory cap)
KLEE: WARNING: killing 10004 states (over memory cap)
KLEE: WARNING: killing 10490 states (over memory cap)
KLEE: WARNING: killing 10607 states (over memory cap)
KLEE: WARNING: killing 10346 states (over memory cap)
KLEE: WARNING: killing 10645 states (over memory cap)
KLEE: WARNING: killing 10262 states (over memory cap)
KLEE: WARNING: killing 10562 states (over memory cap)
KLEE: WARNING: killing 10494 states (over memory cap)
KLEE: WARNING: killing 10356 states (over memory cap)
KLEE: WARNING: killing 10656 states (over memory cap)
KLEE: WARNING: killing 10150 states (over memory cap)
KLEE: WARNING: killing 10446 states (over memory cap)
KLEE: WARNING: killing 10498 states (over memory cap)
KLEE: WARNING: killing 10677 states (over memory cap)
KLEE: WARNING: killing 10544 states (over memory cap)
KLEE: WARNING: killing 10347 states (over memory cap)
KLEE: WARNING: killing 10336 states (over memory cap)
KLEE: WARNING: killing 10947 states (over memory cap)
KLEE: WARNING: killing 10505 states (over memory cap)
KLEE: WARNING: killing 10745 states (over memory cap)
KLEE: WARNING: killing 10858 states (over memory cap)
KLEE: WARNING: killing 10786 states (over memory cap)
KLEE: WARNING: killing 10101 states (over memory cap)
KLEE: WARNING: killing 10641 states (over memory cap)
KLEE: WARNING: killing 10630 states (over memory cap)
KLEE: WARNING: killing 10373 states (over memory cap)
KLEE: WARNING: killing 10552 states (over memory cap)
KLEE: WARNING: killing 10417 states (over memory cap)
KLEE: WARNING: killing 9735 states (over memory cap)
KLEE: WARNING: killing 10888 states (over memory cap)
KLEE: WARNING: killing 10638 states (over memory cap)
KLEE: WARNING: killing 10506 states (over memory cap)
KLEE: WARNING: killing 10553 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-SvkmFt/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--acpi--processor.ko-entry_point_true-unreach-call.cil.out.c:9666: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 10481 states (over memory cap)
KLEE: WARNING: killing 10595 states (over memory cap)
KLEE: WARNING: killing 10281 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10682 states (over memory cap)
KLEE: WARNING: killing 10251 states (over memory cap)
KLEE: WARNING: killing 10666 states (over memory cap)
KLEE: WARNING: killing 10530 states (over memory cap)
KLEE: WARNING: killing 10157 states (over memory cap)
KLEE: WARNING: killing 10873 states (over memory cap)
KLEE: WARNING: killing 10324 states (over memory cap)
KLEE: WARNING: killing 10673 states (over memory cap)
KLEE: WARNING: killing 10298 states (over memory cap)
KLEE: WARNING: killing 10711 states (over memory cap)
KLEE: WARNING: killing 10099 states (over memory cap)
KLEE: WARNING: killing 10389 states (over memory cap)
KLEE: WARNING: killing 10855 states (over memory cap)
KLEE: WARNING: killing 10670 states (over memory cap)
KLEE: WARNING: killing 10663 states (over memory cap)
KLEE: WARNING: killing 10775 states (over memory cap)
KLEE: WARNING: killing 10230 states (over memory cap)
KLEE: WARNING: killing 10759 states (over memory cap)
KLEE: WARNING: killing 10513 states (over memory cap)
KLEE: WARNING: killing 10442 states (over memory cap)
KLEE: WARNING: killing 10373 states (over memory cap)
KLEE: WARNING: killing 10483 states (over memory cap)
KLEE: WARNING: killing 10655 states (over memory cap)
KLEE: WARNING: killing 10700 states (over memory cap)
KLEE: WARNING: killing 10749 states (over memory cap)
KLEE: WARNING: killing 10144 states (over memory cap)
KLEE: WARNING: killing 10608 states (over memory cap)
KLEE: WARNING: killing 10425 states (over memory cap)
KLEE: WARNING: killing 10531 states (over memory cap)
KLEE: WARNING: killing 10522 states (over memory cap)
KLEE: WARNING: killing 10691 states (over memory cap)
KLEE: WARNING: killing 10263 states (over memory cap)
KLEE: WARNING: killing 10493 states (over memory cap)
KLEE: WARNING: killing 10481 states (over memory cap)
KLEE: WARNING: killing 10647 states (over memory cap)
KLEE: WARNING: killing 10814 states (over memory cap)
KLEE: WARNING: killing 10691 states (over memory cap)
KLEE: WARNING: killing 10507 states (over memory cap)
KLEE: WARNING: killing 10439 states (over memory cap)
KLEE: WARNING: killing 10663 states (over memory cap)
KLEE: WARNING: killing 10536 states (over memory cap)
KLEE: WARNING: killing 10409 states (over memory cap)
KLEE: WARNING: killing 10691 states (over memory cap)
KLEE: WARNING: killing 10623 states (over memory cap)
KLEE: WARNING: killing 10500 states (over memory cap)
KLEE: WARNING: killing 10431 states (over memory cap)
KLEE: WARNING: killing 10654 states (over memory cap)
KLEE: WARNING: killing 10880 states (over memory cap)
KLEE: WARNING: killing 10460 states (over memory cap)
KLEE: WARNING: killing 10394 states (over memory cap)
KLEE: WARNING: killing 10381 states (over memory cap)
KLEE: WARNING: killing 10428 states (over memory cap)
KLEE: WARNING: killing 10304 states (over memory cap)
KLEE: WARNING: killing 10760 states (over memory cap)
KLEE: WARNING: killing 11044 states (over memory cap)
KLEE: WARNING: killing 10689 states (over memory cap)
KLEE: WARNING: killing 10503 states (over memory cap)
KLEE: WARNING: killing 10436 states (over memory cap)
KLEE: WARNING: killing 10549 states (over memory cap)
KLEE: WARNING: killing 10939 states (over memory cap)
KLEE: WARNING: killing 10699 states (over memory cap)
KLEE: WARNING: killing 10747 states (over memory cap)
KLEE: WARNING: killing 10222 states (over memory cap)
KLEE: WARNING: killing 10497 states (over memory cap)
KLEE: WARNING: killing 10487 states (over memory cap)
KLEE: WARNING: killing 10531 states (over memory cap)
KLEE: WARNING: killing 10177 states (over memory cap)
KLEE: WARNING: killing 10571 states (over memory cap)
KLEE: WARNING: killing 10857 states (over memory cap)
KLEE: WARNING: killing 10791 states (over memory cap)
KLEE: WARNING: killing 10436 states (over memory cap)
KLEE: WARNING: killing 10314 states (over memory cap)
KLEE: WARNING: killing 10532 states (over memory cap)
KLEE: WARNING: killing 10690 states (over memory cap)
KLEE: WARNING: killing 10739 states (over memory cap)
KLEE: WARNING: killing 10845 states (over memory cap)
KLEE: WARNING: killing 10383 states (over memory cap)
KLEE: WARNING: killing 10204 states (over memory cap)
KLEE: WARNING: killing 10536 states (over memory cap)
KLEE: WARNING: killing 10523 states (over memory cap)
