bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-commit-tester/main4_true-unreach-call_arch-x86-oprofile-oprofile-ko--131_1a--79db8ef-1.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.: 189 278 2060 12679
Removed infinite loop in paravirt_read_msr
Removed infinite loop in paravirt_write_msr
Removed infinite loop in __cpuid
INFO: Compilation, preparation and instrumentation time: 0.474613189697
Defining function no_llseek as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'dcookie_unregister' (function is undefined)
Removed calls to 'ring_buffer_free' (function is undefined)
Removed calls to 'flush_scheduled_work' (function is undefined)
Removed calls to 'free_cpumask_var' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Defining function unregister_module_notifier as symbolic
Defining function profile_event_unregister as symbolic
Defining function task_handoff_unregister as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Removed calls to 'free_task' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function find_next_bit as symbolic
Defining function del_timer_sync as symbolic
Removed calls to '__wake_up' (function is undefined)
Defining function cancel_delayed_work_sync as symbolic
Removed calls to 'pci_dev_put' (function is undefined)
Removed calls to 'release_perfctr_nmi' (function is undefined)
Removed calls to 'release_evntsel_nmi' (function is undefined)
Defining function ring_buffer_unlock_commit as symbolic
Defining function ring_buffer_lock_reserve as symbolic
Defining function ring_buffer_event_data as symbolic
Defining function profile_pc as symbolic
Defining function setup_APIC_eilvt_ibs as symbolic
Defining function printk as symbolic
Defining function reserve_perfctr_nmi as symbolic
Defining function reserve_evntsel_nmi as symbolic
Removed calls to 'dput' (function is undefined)
Removed calls to 'd_instantiate' (function is undefined)
Removed calls to 'd_rehash' (function is undefined)
Defining function d_alloc_name as symbolic
Defining function new_inode as symbolic
Defining function current_kernel_time as symbolic
Defining function pci_get_device as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function find_first_bit as symbolic
Defining function schedule_delayed_work as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Removed calls to 'mmput' (function is undefined)
Defining function find_vma as symbolic
Defining function get_dcookie as symbolic
Defining function get_task_mm as symbolic
Defining function ring_buffer_consume as symbolic
Defining function ring_buffer_event_length as symbolic
Defining function ring_buffer_entries_cpu as symbolic
Defining function simple_strtoul as symbolic
Defining function _copy_from_user as symbolic
Defining function snprintf as symbolic
Defining function simple_read_from_buffer as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function jiffies_to_msecs as symbolic
Removed calls to 'iput' (function is undefined)
Defining function get_sb_single as symbolic
Defining function d_alloc_root as symbolic
Defining function generic_delete_inode as symbolic
Defining function simple_statfs as symbolic
Removed calls to 'hrtimer_init' (function is undefined)
Defining function smp_call_function_single as symbolic
Defining function hrtimer_cancel as symbolic
Defining function hrtimer_start as symbolic
Defining function hrtimer_forward as symbolic
Defining function print_context_stack as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function capable as symbolic
Defining function dcookie_register as symbolic
Defining function nonseekable_open as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Defining function zalloc_cpumask_var as symbolic
Defining function task_handoff_register as symbolic
Defining function profile_event_register as symbolic
Defining function register_module_notifier as symbolic
Defining function schedule_delayed_work_on as symbolic
Defining function vmalloc as symbolic
Defining function __ring_buffer_alloc as symbolic
Defining function autoremove_wake_function as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_handler_precall' (function is undefined)
Removed calls to 'unregister_cpu_notifier' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Removed calls to 'sysdev_unregister' (function is undefined)
Removed calls to 'sysdev_class_unregister' (function is undefined)
Defining function unregister_filesystem as symbolic
Defining function register_filesystem as symbolic
Defining function register_cpu_notifier as symbolic
Defining function on_each_cpu as symbolic
Removed calls to 'dump_trace' (function is undefined)
Defining function copy_user_generic_unrolled as symbolic
Defining function copy_user_generic_string as symbolic
Removed calls to 'synchronize_sched' (function is undefined)
Defining function unregister_die_notifier as symbolic
Defining function register_die_notifier as symbolic
Removed calls to 'get_online_cpus' (function is undefined)
Removed calls to 'put_online_cpus' (function is undefined)
Defining function sysdev_class_register as symbolic
Defining function sysdev_register as symbolic
Defining function avail_to_resrv_perfctr_nmi_bit as symbolic
Removed calls to 'ldv_check_return_value' (function is undefined)
Linked our definitions to these undefined functions:
  strlen
  __kmalloc
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.466413021088
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 331 244 1241 7589
INFO: Starting verification
KLEE: WARNING ONCE: function "event_buffer_read" has inline asm
KLEE: WARNING ONCE: function "event_buffer_open" has inline asm
KLEE: WARNING ONCE: function "event_buffer_release" has inline asm
KLEE: WARNING ONCE: function "end_cpu_work" has inline asm
KLEE: WARNING ONCE: function "op_amd_setup_ctrs" has inline asm
KLEE: WARNING ONCE: function "op_amd_check_ctrs" has inline asm
KLEE: WARNING ONCE: function "op_amd_start" has inline asm
KLEE: WARNING ONCE: function "op_amd_stop" has inline asm
KLEE: WARNING ONCE: function "op_mux_switch_ctrl" has inline asm
KLEE: WARNING ONCE: function "paravirt_read_msr" has inline asm
KLEE: WARNING ONCE: function "paravirt_write_msr" has inline asm
KLEE: WARNING ONCE: function "oprofile_write_reserve" has inline asm
KLEE: WARNING ONCE: function "__oprofile_add_ext_sample" has inline asm
KLEE: WARNING ONCE: function "log_sample" has inline asm
KLEE: WARNING ONCE: function "cpuid_eax" has inline asm
KLEE: WARNING ONCE: function "ppro_setup_ctrs" has inline asm
KLEE: WARNING ONCE: function "arch_perfmon_init" has inline asm
KLEE: WARNING ONCE: function "p4_fill_in_addresses" has inline asm
KLEE: WARNING ONCE: function "p4_setup_ctrs" has inline asm
KLEE: WARNING ONCE: function "p4_check_ctrs" has inline asm
KLEE: WARNING ONCE: function "p4_start" has inline asm
KLEE: WARNING ONCE: function "p4_stop" has inline asm
KLEE: WARNING ONCE: function "switch_worker" has inline asm
KLEE: WARNING ONCE: function "task_exit_notify" has inline asm
KLEE: WARNING ONCE: function "sync_buffer" has inline asm
KLEE: WARNING ONCE: function "add_event_entry" has inline asm
KLEE: WARNING ONCE: function "munmap_notify" has inline asm
KLEE: WARNING ONCE: function "oprofile_reset_stats" has inline asm
KLEE: WARNING ONCE: function "oprofile_create_stats_files" has inline asm
KLEE: WARNING ONCE: function "oprofile_cpu_notify" has inline asm
KLEE: WARNING ONCE: function "__oprofile_hrtimer_start" has inline asm
KLEE: WARNING ONCE: function "oprofile_hrtimer_notify" has inline asm
KLEE: WARNING ONCE: function "oprofile_add_trace" has inline asm
KLEE: WARNING ONCE: function "profile_exceptions_notify" has inline asm
KLEE: WARNING ONCE: function "nmi_cpu_stop" has inline asm
KLEE: WARNING ONCE: function "nmi_cpu_shutdown" has inline asm
KLEE: WARNING ONCE: function "nmi_cpu_setup" has inline asm
KLEE: WARNING ONCE: function "nmi_cpu_start" has inline asm
KLEE: WARNING ONCE: function "alloc_cpu_buffers" has inline asm
KLEE: WARNING ONCE: function "start_cpu_work" has inline asm
KLEE: WARNING ONCE: function "wq_sync_buffer" has inline asm
KLEE: WARNING ONCE: function "op_x86_phys_to_virt" has inline asm
KLEE: WARNING ONCE: function "oprofile_hrtimer_stop" has inline asm
KLEE: WARNING ONCE: function "x86_backtrace" has inline asm
KLEE: WARNING ONCE: function "nmi_setup" has inline asm
KLEE: WARNING ONCE: function "nmi_shutdown" has inline asm
KLEE: WARNING ONCE: function "nmi_cpu_switch" has inline asm
KLEE: WARNING ONCE: function "free_msrs" has inline asm
KLEE: WARNING ONCE: function "oprofile_cpu_buffer_inc_smpl_lost" has inline asm
KLEE: WARNING ONCE: function "oprofile_add_pc" has inline asm
KLEE: WARNING ONCE: function "ldv_main2_sequence_infinite_withcheck_stateful" has inline asm
KLEE: WARNING: undefined reference to variable: boot_tvec_bases
KLEE: WARNING: undefined reference to function: kill_litter_super
KLEE: WARNING: Type for boot_tvec_bases is not sized
KLEE: WARNING: Unable to find size for global variable: boot_tvec_bases (use will result in out of bounds access)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_08690d18-5bf1-4356-b85a-1fca24125c6c/symbiotic/lib/libc/strlen.c:6: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 32768 bytes on read, may be slow and/or crash: MO99[32768] allocated at global:__per_cpu_offset
KLEE: ERROR: /tmp/symbiotic-hw1SPr/main4_true-unreach-call_arch-x86-oprofile-oprofile-ko--131_1a--79db8ef-1.c:5888: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hw1SPr/main4_true-unreach-call_arch-x86-oprofile-oprofile-ko--131_1a--79db8ef-1.c:5991: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-hw1SPr/main4_true-unreach-call_arch-x86-oprofile-oprofile-ko--131_1a--79db8ef-1.c:5927: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
