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--hid--hid-roccat-kovaplus.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.: 99 129 862 4913
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.270148992538
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'hid_disconnect' (function is undefined)
Removed calls to 'roccat_disconnect' (function is undefined)
Defining function roccat_report_event as symbolic
Defining function roccat_connect as symbolic
Defining function roccat_common2_receive as symbolic
Defining function roccat_common2_send as symbolic
Defining function hid_connect as symbolic
Defining function hid_open_report as symbolic
Defining function snprintf as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function roccat_common2_send_with_status as symbolic
Defining function kstrtoull as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'hid_unregister_driver' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Defining function ldv_release_11 as symbolic
Defining function ldv_probe_11 as symbolic
Defining function ldv_release_7 as symbolic
Defining function ldv_probe_7 as symbolic
Defining function ldv_release_17 as symbolic
Defining function ldv_probe_17 as symbolic
Defining function ldv_release_18 as symbolic
Defining function ldv_probe_18 as symbolic
Defining function ldv_release_16 as symbolic
Defining function ldv_probe_16 as symbolic
Defining function ldv_release_13 as symbolic
Defining function ldv_probe_13 as symbolic
Defining function ldv_release_9 as symbolic
Defining function ldv_probe_9 as symbolic
Defining function ldv_release_12 as symbolic
Defining function ldv_probe_12 as symbolic
Defining function ldv_release_20 as symbolic
Defining function ldv_probe_20 as symbolic
Defining function ldv_release_14 as symbolic
Defining function ldv_probe_14 as symbolic
Defining function ldv_release_15 as symbolic
Defining function ldv_probe_15 as symbolic
Defining function ldv_release_8 as symbolic
Defining function ldv_probe_8 as symbolic
Defining function ldv_release_19 as symbolic
Defining function ldv_probe_19 as symbolic
Defining function ldv_release_10 as symbolic
Defining function ldv_probe_10 as symbolic
Defining function __class_create as symbolic
Defining function __hid_register_driver as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  __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: 0.292201042175
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 163 152 575 3347
INFO: Starting verification
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_d7a65cc0-5a76-4042-8430-da2ee2cb4e48/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:5086: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11334 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 25341 states (over memory cap)
KLEE: WARNING: killing 24374 states (over memory cap)
KLEE: WARNING: killing 20909 states (over memory cap)
KLEE: WARNING: killing 21388 states (over memory cap)
KLEE: WARNING: killing 23395 states (over memory cap)
KLEE: WARNING: killing 23713 states (over memory cap)
KLEE: WARNING: killing 24509 states (over memory cap)
KLEE: WARNING: killing 23792 states (over memory cap)
KLEE: WARNING: killing 26276 states (over memory cap)
KLEE: WARNING: killing 25035 states (over memory cap)
KLEE: WARNING: killing 26627 states (over memory cap)
KLEE: WARNING: killing 27917 states (over memory cap)
KLEE: WARNING: killing 26110 states (over memory cap)
KLEE: WARNING: killing 24456 states (over memory cap)
KLEE: WARNING: killing 24690 states (over memory cap)
KLEE: WARNING: killing 26265 states (over memory cap)
KLEE: WARNING: killing 25050 states (over memory cap)
KLEE: WARNING: killing 24858 states (over memory cap)
KLEE: WARNING: killing 23416 states (over memory cap)
KLEE: WARNING: killing 25002 states (over memory cap)
KLEE: WARNING: killing 24457 states (over memory cap)
KLEE: WARNING: killing 24634 states (over memory cap)
KLEE: WARNING: killing 26000 states (over memory cap)
KLEE: WARNING: killing 25093 states (over memory cap)
KLEE: WARNING: killing 24921 states (over memory cap)
KLEE: WARNING: killing 25921 states (over memory cap)
KLEE: WARNING: killing 26923 states (over memory cap)
KLEE: WARNING: killing 24527 states (over memory cap)
KLEE: WARNING: killing 25634 states (over memory cap)
KLEE: WARNING: killing 25147 states (over memory cap)
KLEE: WARNING: killing 25218 states (over memory cap)
KLEE: WARNING: killing 24733 states (over memory cap)
KLEE: WARNING: killing 25165 states (over memory cap)
KLEE: WARNING: killing 23912 states (over memory cap)
KLEE: WARNING: killing 25067 states (over memory cap)
KLEE: WARNING: killing 25809 states (over memory cap)
KLEE: WARNING: killing 25890 states (over memory cap)
KLEE: WARNING: killing 25354 states (over memory cap)
KLEE: WARNING: killing 24922 states (over memory cap)
KLEE: WARNING: killing 25254 states (over memory cap)
KLEE: WARNING: killing 24716 states (over memory cap)
KLEE: WARNING: killing 25343 states (over memory cap)
KLEE: WARNING: killing 25323 states (over memory cap)
KLEE: WARNING: killing 24994 states (over memory cap)
KLEE: WARNING: killing 25012 states (over memory cap)
KLEE: WARNING: killing 26208 states (over memory cap)
KLEE: WARNING: killing 23093 states (over memory cap)
KLEE: WARNING: killing 25747 states (over memory cap)
KLEE: WARNING: killing 25314 states (over memory cap)
KLEE: WARNING: killing 25291 states (over memory cap)
KLEE: WARNING: killing 25721 states (over memory cap)
KLEE: WARNING: killing 26506 states (over memory cap)
KLEE: WARNING: killing 25430 states (over memory cap)
KLEE: WARNING: killing 25403 states (over memory cap)
KLEE: WARNING: killing 25018 states (over memory cap)
KLEE: WARNING: killing 24842 states (over memory cap)
KLEE: WARNING: killing 24971 states (over memory cap)
KLEE: WARNING: killing 25555 states (over memory cap)
KLEE: WARNING: killing 24529 states (over memory cap)
KLEE: WARNING: killing 25299 states (over memory cap)
KLEE: WARNING: killing 24230 states (over memory cap)
KLEE: WARNING: killing 26047 states (over memory cap)
KLEE: WARNING: killing 25877 states (over memory cap)
KLEE: WARNING: killing 24363 states (over memory cap)
KLEE: WARNING: killing 25334 states (over memory cap)
KLEE: WARNING: killing 25165 states (over memory cap)
KLEE: WARNING: killing 25638 states (over memory cap)
KLEE: WARNING: killing 25022 states (over memory cap)
KLEE: WARNING: killing 25692 states (over memory cap)
KLEE: WARNING: killing 24284 states (over memory cap)
KLEE: WARNING: killing 26539 states (over memory cap)
KLEE: WARNING: killing 25086 states (over memory cap)
KLEE: WARNING: killing 24914 states (over memory cap)
KLEE: WARNING: killing 25793 states (over memory cap)
KLEE: WARNING: killing 25523 states (over memory cap)
KLEE: WARNING: killing 24854 states (over memory cap)
KLEE: WARNING: killing 25074 states (over memory cap)
KLEE: WARNING: killing 24319 states (over memory cap)
KLEE: WARNING: killing 24740 states (over memory cap)
KLEE: WARNING: killing 24957 states (over memory cap)
KLEE: WARNING: killing 26310 states (over memory cap)
KLEE: WARNING: killing 25753 states (over memory cap)
KLEE: WARNING: killing 26131 states (over memory cap)
KLEE: WARNING: killing 25717 states (over memory cap)
KLEE: WARNING: killing 23630 states (over memory cap)
KLEE: WARNING: killing 24634 states (over memory cap)
KLEE: WARNING: killing 26034 states (over memory cap)
KLEE: WARNING: killing 25291 states (over memory cap)
KLEE: WARNING: killing 25024 states (over memory cap)
KLEE: WARNING: killing 25250 states (over memory cap)
KLEE: WARNING: killing 24148 states (over memory cap)
KLEE: WARNING: killing 26329 states (over memory cap)
KLEE: WARNING: killing 24796 states (over memory cap)
KLEE: WARNING: killing 25949 states (over memory cap)
KLEE: WARNING: killing 24469 states (over memory cap)
KLEE: WARNING: killing 25227 states (over memory cap)
KLEE: WARNING: killing 25112 states (over memory cap)
KLEE: WARNING: killing 25862 states (over memory cap)
KLEE: WARNING: killing 24823 states (over memory cap)
KLEE: WARNING: killing 24856 states (over memory cap)
KLEE: WARNING: killing 25179 states (over memory cap)
KLEE: WARNING: killing 24867 states (over memory cap)
KLEE: WARNING: killing 24990 states (over memory cap)
KLEE: WARNING: killing 25789 states (over memory cap)
KLEE: WARNING: killing 26204 states (over memory cap)
KLEE: WARNING: killing 24259 states (over memory cap)
KLEE: WARNING: killing 26024 states (over memory cap)
KLEE: WARNING: killing 23931 states (over memory cap)
KLEE: WARNING: killing 25161 states (over memory cap)
KLEE: WARNING: killing 24946 states (over memory cap)
KLEE: WARNING: killing 25129 states (over memory cap)
KLEE: WARNING: killing 24485 states (over memory cap)
KLEE: WARNING: killing 24889 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:4771: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25637 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:4728: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25758 states (over memory cap)
KLEE: WARNING: killing 24879 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:5040: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25669 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:4208: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25744 states (over memory cap)
KLEE: WARNING: killing 25098 states (over memory cap)
KLEE: WARNING: killing 26799 states (over memory cap)
KLEE: WARNING: killing 25063 states (over memory cap)
KLEE: WARNING: killing 24654 states (over memory cap)
KLEE: WARNING: killing 25205 states (over memory cap)
KLEE: WARNING: killing 25663 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:4748: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:4660: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25355 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:4576: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24565 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:4640: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 26222 states (over memory cap)
KLEE: WARNING: killing 25627 states (over memory cap)
KLEE: WARNING: killing 24942 states (over memory cap)
KLEE: WARNING: killing 24914 states (over memory cap)
KLEE: WARNING: killing 25745 states (over memory cap)
KLEE: WARNING: killing 25150 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-FZGmg6/linux-4.2-rc1.tar.xz-32_7a-drivers--hid--hid-roccat-kovaplus.ko-entry_point_true-unreach-call.cil.out.c:4708: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25313 states (over memory cap)
KLEE: WARNING: killing 25726 states (over memory cap)
