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-43_2a-drivers--input--mouse--psmouse.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.: 607 578 6284 44222
Removed infinite loop in alps_command_mode_send_nibble
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.65062880516
Removed calls to 'dev_warn' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'input_set_abs_params' (function is undefined)
Removed calls to 'input_alloc_absinfo' (function is undefined)
Removed calls to 'input_set_capability' (function is undefined)
Removed calls to 'input_free_device' (function is undefined)
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)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'sysfs_remove_group' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Defining function __request_region as symbolic
Defining function input_allocate_device as symbolic
Defining function snprintf as symbolic
Defining function input_register_device as symbolic
Removed calls to 'input_event' (function is undefined)
Removed calls to 'input_unregister_device' (function is undefined)
Defining function ps2_command as symbolic
Removed calls to 'input_mt_report_slot_state' (function is undefined)
Removed calls to 'input_mt_report_pointer_emulation' (function is undefined)
Defining function input_mt_init_slots as symbolic
Defining function kstrndup as symbolic
Defining function strsep as symbolic
Defining function strcasecmp as symbolic
Defining function sysfs_create_group as symbolic
Removed calls to 'ps2_begin_command' (function is undefined)
Removed calls to 'ps2_end_command' (function is undefined)
Defining function ps2_sendbyte as symbolic
Defining function __ps2_command as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to 'dev_printk' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Defining function printk as symbolic
Defining function dmi_check_system as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'input_mt_report_finger_count' (function is undefined)
Removed calls to 'input_mt_sync_frame' (function is undefined)
Defining function input_mt_assign_slots as symbolic
Removed calls to 'ps2_drain' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function del_timer as symbolic
Defining function mod_timer as symbolic
Defining function __msecs_to_jiffies as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to '__serio_register_port' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Defining function dmi_get_system_info as symbolic
Defining function device_create_file as symbolic
Defining function strlcpy as symbolic
Removed calls to 'input_mt_drop_unused' (function is undefined)
Defining function serio_interrupt as symbolic
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Defining function prepare_to_wait_event as symbolic
Defining function schedule_timeout as symbolic
Removed calls to 'serio_unregister_child_port' (function is undefined)
Defining function sprintf as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function kstrtouint as symbolic
Removed calls to 'ps2_cmd_aborted' (function is undefined)
Removed calls to 'serio_reconnect' (function is undefined)
Removed calls to 'ps2_init' (function is undefined)
Removed calls to 'serio_close' (function is undefined)
Removed calls to 'flush_workqueue' (function is undefined)
Defining function serio_open as symbolic
Defining function ps2_handle_ack as symbolic
Defining function ps2_handle_response as symbolic
Removed calls to 'dev_notice' (function is undefined)
Defining function kstrtou8 as symbolic
Defining function simple_strtoul as symbolic
Defining function kstrtoint as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'serio_unregister_driver' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Defining function __serio_register_driver as symbolic
Defining function queue_work_on as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcmp
  strlen
  strncmp
  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.627161026
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 682 477 3340 25055
INFO: Starting verification
KLEE: WARNING ONCE: function "ps2bare_detect" has inline asm
KLEE: WARNING ONCE: function "ps2pp_init" has inline asm
KLEE: WARNING ONCE: function "thinking_detect" has inline asm
KLEE: WARNING ONCE: function "cypress_init" has inline asm
KLEE: WARNING ONCE: function "genius_detect" has inline asm
KLEE: WARNING ONCE: function "intellimouse_detect" has inline asm
KLEE: WARNING ONCE: function "im_explorer_detect" has inline asm
KLEE: WARNING ONCE: function "alps_init" has inline asm
KLEE: WARNING ONCE: function "trackpoint_detect" has inline asm
KLEE: WARNING ONCE: function "elantech_init" has inline asm
KLEE: WARNING ONCE: function "fsp_init" has inline asm
KLEE: WARNING ONCE: function "cortron_detect" has inline asm
KLEE: WARNING ONCE: function "focaltech_init" has inline asm
KLEE: WARNING ONCE: function "vmmouse_detect" has inline asm
KLEE: WARNING ONCE: function "vmmouse_enable" has inline asm
KLEE: WARNING ONCE: function "vmmouse_process_byte" has inline asm
KLEE: WARNING ONCE: function "vmmouse_disable" has inline asm
KLEE: WARNING ONCE: function "vmmouse_report_button" has inline asm
KLEE: WARNING ONCE: function "alps_register_bare_ps2_mouse" has inline asm
KLEE: WARNING ONCE: function "alps_set_abs_params_v7" has inline asm
KLEE: WARNING ONCE: function "alps_set_abs_params_ss4_v2" has inline asm
KLEE: WARNING ONCE: function "alps_set_abs_params_mt_common" has inline asm
KLEE: WARNING ONCE: function "alps_command_mode_send_nibble" has inline asm
KLEE: WARNING ONCE: function "__synaptics_init" has inline asm
KLEE: WARNING ONCE: function "psmouse_apply_defaults" has inline asm
KLEE: WARNING ONCE: function "psmouse_extensions" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
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_2e37eb30-0a5c-490b-8e25-593aff7c09fd/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 8836 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 45668 states (over memory cap)
KLEE: WARNING: killing 37271 states (over memory cap)
KLEE: WARNING: killing 39052 states (over memory cap)
KLEE: WARNING: killing 36467 states (over memory cap)
KLEE: WARNING: killing 35908 states (over memory cap)
KLEE: WARNING: killing 39119 states (over memory cap)
KLEE: WARNING: killing 39205 states (over memory cap)
KLEE: WARNING: killing 42742 states (over memory cap)
KLEE: WARNING: killing 40915 states (over memory cap)
KLEE: WARNING: killing 45471 states (over memory cap)
KLEE: WARNING: killing 44678 states (over memory cap)
KLEE: WARNING: killing 46248 states (over memory cap)
KLEE: WARNING: killing 39304 states (over memory cap)
KLEE: WARNING: killing 39988 states (over memory cap)
KLEE: WARNING: killing 40887 states (over memory cap)
KLEE: WARNING: killing 40146 states (over memory cap)
KLEE: WARNING: killing 45260 states (over memory cap)
KLEE: WARNING: killing 42619 states (over memory cap)
KLEE: WARNING: killing 41122 states (over memory cap)
KLEE: WARNING: killing 43793 states (over memory cap)
KLEE: WARNING: killing 40733 states (over memory cap)
KLEE: WARNING: killing 40161 states (over memory cap)
KLEE: WARNING: killing 41599 states (over memory cap)
KLEE: WARNING: killing 40502 states (over memory cap)
KLEE: WARNING: killing 45804 states (over memory cap)
KLEE: WARNING: killing 39580 states (over memory cap)
KLEE: WARNING: killing 40593 states (over memory cap)
KLEE: WARNING: killing 43751 states (over memory cap)
KLEE: WARNING: killing 42125 states (over memory cap)
KLEE: WARNING: killing 41819 states (over memory cap)
KLEE: WARNING: killing 41139 states (over memory cap)
KLEE: WARNING: killing 42936 states (over memory cap)
KLEE: WARNING: killing 42217 states (over memory cap)
KLEE: WARNING: killing 41807 states (over memory cap)
KLEE: WARNING: killing 40663 states (over memory cap)
KLEE: WARNING: killing 43285 states (over memory cap)
KLEE: WARNING: killing 41738 states (over memory cap)
KLEE: WARNING: killing 40800 states (over memory cap)
KLEE: WARNING: killing 43638 states (over memory cap)
KLEE: WARNING: killing 40157 states (over memory cap)
KLEE: WARNING: killing 41632 states (over memory cap)
KLEE: WARNING: killing 41311 states (over memory cap)
KLEE: WARNING: killing 43045 states (over memory cap)
KLEE: WARNING: killing 41483 states (over memory cap)
KLEE: WARNING: killing 41897 states (over memory cap)
KLEE: WARNING: killing 42339 states (over memory cap)
KLEE: WARNING: killing 40946 states (over memory cap)
KLEE: WARNING: killing 42242 states (over memory cap)
KLEE: WARNING: killing 41896 states (over memory cap)
KLEE: WARNING: killing 42783 states (over memory cap)
KLEE: WARNING: killing 41905 states (over memory cap)
KLEE: WARNING: killing 38829 states (over memory cap)
KLEE: WARNING: killing 40984 states (over memory cap)
KLEE: WARNING: killing 42015 states (over memory cap)
KLEE: WARNING: killing 43961 states (over memory cap)
KLEE: WARNING: killing 41981 states (over memory cap)
KLEE: WARNING: killing 40445 states (over memory cap)
KLEE: WARNING: killing 43990 states (over memory cap)
KLEE: WARNING: killing 42107 states (over memory cap)
KLEE: WARNING: killing 40390 states (over memory cap)
KLEE: WARNING: killing 41412 states (over memory cap)
KLEE: WARNING: killing 40810 states (over memory cap)
KLEE: WARNING: killing 42967 states (over memory cap)
KLEE: WARNING: killing 41598 states (over memory cap)
KLEE: WARNING: killing 41457 states (over memory cap)
KLEE: WARNING: killing 40005 states (over memory cap)
KLEE: WARNING: killing 41483 states (over memory cap)
KLEE: WARNING: killing 41148 states (over memory cap)
KLEE: WARNING: killing 41874 states (over memory cap)
KLEE: WARNING: killing 38992 states (over memory cap)
KLEE: WARNING: killing 41471 states (over memory cap)
KLEE: WARNING: killing 44024 states (over memory cap)
KLEE: WARNING: killing 42217 states (over memory cap)
KLEE: WARNING: killing 43988 states (over memory cap)
KLEE: WARNING: killing 41999 states (over memory cap)
KLEE: WARNING: killing 44636 states (over memory cap)
KLEE: WARNING: killing 39910 states (over memory cap)
KLEE: WARNING: killing 38058 states (over memory cap)
KLEE: WARNING: killing 44247 states (over memory cap)
KLEE: WARNING: killing 41954 states (over memory cap)
KLEE: WARNING: killing 38595 states (over memory cap)
KLEE: WARNING: killing 44787 states (over memory cap)
KLEE: WARNING: killing 40931 states (over memory cap)
KLEE: WARNING: killing 42211 states (over memory cap)
KLEE: WARNING: killing 42140 states (over memory cap)
KLEE: WARNING: killing 38752 states (over memory cap)
KLEE: WARNING: killing 42605 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-B3v0bk/linux-4.2-rc1.tar.xz-43_2a-drivers--input--mouse--psmouse.ko-entry_point_true-unreach-call.cil.out.c:6108: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-B3v0bk/linux-4.2-rc1.tar.xz-43_2a-drivers--input--mouse--psmouse.ko-entry_point_true-unreach-call.cil.out.c:6330: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-B3v0bk/linux-4.2-rc1.tar.xz-43_2a-drivers--input--mouse--psmouse.ko-entry_point_true-unreach-call.cil.out.c:6380: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 42155 states (over memory cap)
KLEE: WARNING: killing 40231 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-B3v0bk/linux-4.2-rc1.tar.xz-43_2a-drivers--input--mouse--psmouse.ko-entry_point_true-unreach-call.cil.out.c:6157: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-B3v0bk/linux-4.2-rc1.tar.xz-43_2a-drivers--input--mouse--psmouse.ko-entry_point_true-unreach-call.cil.out.c:6176: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 42877 states (over memory cap)
KLEE: WARNING: killing 45546 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-B3v0bk/linux-4.2-rc1.tar.xz-43_2a-drivers--input--mouse--psmouse.ko-entry_point_true-unreach-call.cil.out.c:6157: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 40136 states (over memory cap)
