./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain ONLY for:
[Info] usb_urb, usb_dev, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, tmp, tmp, tmp, tmp, tmp, tmp, tmp, res, tmp, res, tmp, data, data, tmp, result, tmp, res, urb, tmp, urb, complete_fn, urb, complete_fn, urb, value, tmp___0, data, arg, urb, tmp, data, urb, complete_fn, tmp, ldv_func_arg1, tmp, ldv_func_arg1, tmp, ldv_func_arg1, ldv_func_arg2, ldv_func_arg3, ldv_func_res, tmp, tmp, tmp___0, tmp___1, tmp___2, result, tmp, intf, input_dev, acecad, dev, maxp, err, tmp___0, tmp___5, tmp___6, dev, tmp___0, dev, dev, prox, status, urb, x, y, pressure, touch, id, dev, dev, code, value, value, dev, code, data, tmp, exp, tmp, tmp, s, c, n, tmp, p, size, tmp, p, tmp___0, size, tmp, p, tmp___0, size, tmp, cond, size, tmp, size, flags, tmp___1, size, tmp, is_out, tmp, tmp___0, ep, driver, tmp, actual, size, buf, tmp, tmp, tmp___0, epd, tmp___1
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3360:3-3360:69)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3360:3-3360:69)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3360:3-3360:69)
[Info][Unsound] Unknown address in {&__this_module} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3980:3-3980:73)
[Info][Unsound] Unknown value in {&__this_module} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3980:3-3980:73)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3980:3-3980:73)
[Info][Unsound] Unknown value in {&(alloc@sid:87)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3871:3-3871:57)
[Info][Unsound] Unknown value in {&(alloc@sid:87)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3909:7-3909:54)
[Info][Unsound] Unknown value in {&(alloc@sid:87)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3819:3-3819:37)
[Info][Unsound] Unknown value in {&(alloc@sid:87)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3821:3-3821:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3822:3-3822:41)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3822:3-3822:41)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3822:3-3822:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3823:3-3823:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3824:3-3824:81)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3825:3-3825:30)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3825:3-3825:30)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3911:7-3911:28)
[Info][Unsound] Unknown value in {&(alloc@sid:87)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3898:7-3898:103)
[Info][Unsound] Unknown value in {&(alloc@sid:87)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3707:3-3707:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3709:3-3709:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3710:7-3710:57)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3714:3-3714:43)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3715:3-3715:85)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3715:3-3715:85)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3317:3-3317:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3308:12-3308:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3319:5-3319:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3302:11-3302:59)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3302:11-3302:59)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3717:13-3717:17)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3720:3-3720:74)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3380:11-3380:64)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3380:11-3380:64)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3721:3-3721:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3721:3-3721:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3722:3-3722:56)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3392:3-3392:44)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3392:3-3392:44)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3723:3-3723:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3724:3-3724:33)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3725:3-3725:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3726:3-3726:38)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3732:3-3732:67)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4339:10-4339:25)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3464:3-3464:36)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3466:13-3466:23)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3468:5-3468:23)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3469:5-3469:12)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3470:5-3470:74)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3457:1-3457:1)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3471:13-3471:15)
[Warning][Unknown] lval (& acecad)->data_dma points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4339:10-4339:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3733:3-3733:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3739:3-3739:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3745:3-3745:23)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3746:3-3746:28)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3746:3-3746:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3746:3-3746:28)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3748:5-3748:78)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3748:5-3748:78)
[Warning][Unknown] lval (& acecad)->name points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:44:170-44:173)
[Warning][Unknown] lval (& acecad)->name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4336:10-4336:35)
[Warning][Unknown] lval (& acecad)->name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4336:10-4336:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3753:7-3753:52)
[Warning][Unknown] lval (& acecad)->name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4332:10-4332:35)
[Warning][Unknown] lval (& acecad)->name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4332:10-4332:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3756:5-3756:73)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3756:5-3756:73)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3759:3-3759:53)
[Info][Imprecise] Invalidating expressions: buf (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3349:3-3349:92)
[Info][Imprecise] Invalidating expressions: & actual (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3349:3-3349:92)
[Warning][Unknown] lval (& acecad)->phys points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3349:3-3349:92)
[Warning][Unknown] lval (& acecad)->phys points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3350:11-3350:45)
[Warning][Unknown] lval (& acecad)->phys points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3350:11-3350:45)
[Warning][Unknown] lval (& acecad)->phys points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3350:11-3350:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3760:3-3760:53)
[Warning][Unknown] lval (& acecad)->phys points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:44:170-44:173)
[Warning][Unknown] lval (& acecad)->phys points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4332:10-4332:35)
[Warning][Unknown] lval (& acecad)->phys points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4332:10-4332:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3761:3-3761:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3762:3-3762:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3763:3-3763:67)
[Warning][Unknown] lval (& input_dev)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3597:3-3597:19)
[Warning][Unknown] lval (& input_dev)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3598:3-3598:40)
[Warning][Unknown] lval (& input_dev)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3599:3-3599:42)
[Warning][Unknown] lval (& input_dev)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3600:3-3600:42)
[Warning][Unknown] lval (& input_dev)->id points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3601:3-3601:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3764:3-3764:38)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3764:3-3764:38)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3764:3-3764:38)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3765:3-3765:47)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3765:3-3765:47)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3765:3-3765:47)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3562:3-3562:36)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3562:3-3562:36)
[Warning][Unknown] lval (& dev)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4305:3-4305:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3766:3-3766:38)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3767:3-3767:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3768:3-3768:29)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3769:3-3769:32)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3771:3-3771:11)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3782:3-3782:11)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3772:3-3772:53)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3772:3-3772:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3772:3-3772:53)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3773:3-3773:53)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3773:3-3773:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3773:3-3773:53)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3774:3-3774:53)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3774:3-3774:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3774:3-3774:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3775:3-3775:51)
[Info][Imprecise] Invalidating expressions: (char *)(& acecad->name) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3777:5-3778:78)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3783:3-3783:54)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3783:3-3783:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3783:3-3783:54)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3784:3-3784:53)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3784:3-3784:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3784:3-3784:53)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3785:3-3785:54)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3785:3-3785:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3785:3-3785:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3786:3-3786:51)
[Info][Imprecise] Invalidating expressions: (char *)(& acecad->name) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3788:5-3789:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3795:3-3796:107)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3795:3-3796:107)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3795:3-3796:107)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3795:3-3796:107)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3795:3-3796:107)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3795:3-3796:107)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4123:5-4123:52)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3797:4-3797:49)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3798:4-3798:69)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3799:3-3799:45)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3799:3-3799:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3799:3-3799:45)
[Info][Unsound] Unknown value in {&(alloc@sid:87)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3804:3-3804:47)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3804:3-3804:47)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3804:3-3804:47)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3804:3-3804:47)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4025:3-4025:29)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4025:3-4025:29)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4078:3-4078:22)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4078:3-4078:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3805:11-3805:13)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3728:5-3728:14)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3735:5-3735:14)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3741:5-3741:14)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3807:3-3807:70)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3809:3-3809:31)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3809:3-3809:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3809:3-3809:31)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3810:3-3810:30)
[Info][Unsound] Unknown value in {&(alloc@sid:87).dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3810:3-3810:30)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3810:3-3810:30)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3811:11-3811:15)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3901:9-3901:30)
[Warning][Deadcode] Function 'ldv_zalloc' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3475:1-3491:1)
[Warning][Deadcode] Function 'ldv_memset' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3503:1-3510:1)
[Warning][Deadcode] Function 'ldv_undef_ulong' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3519:1-3526:1)
[Warning][Deadcode] Function 'input_get_drvdata' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3551:1-3558:1)
[Warning][Deadcode] Function 'input_report_key' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3569:1-3576:1)
[Warning][Deadcode] Function 'input_report_abs' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3577:1-3584:1)
[Warning][Deadcode] Function 'input_sync' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3585:1-3591:1)
[Warning][Deadcode] Function 'usb_acecad_irq' is uncalled: 31 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3604:1-3659:1)
[Warning][Deadcode] Function 'usb_acecad_open' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3660:1-3676:1)
[Warning][Deadcode] Function 'usb_acecad_close' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3677:1-3687:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_3' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3988:1-3995:1)
[Warning][Deadcode] Function 'ldv_usb_submit_urb_4' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3996:1-4003:1)
[Warning][Deadcode] Function 'ldv_usb_put_intf' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4082:1-4088:1)
[Warning][Deadcode] Function 'ldv_fill_bulk_urb' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4129:1-4139:1)
[Warning][Deadcode] Function 'ldv_submit_urb' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4140:1-4169:1)
[Warning][Deadcode] Function 'ldv_get_dev' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4184:1-4202:1)
[Warning][Deadcode] Function 'ldv_put_dev' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4203:1-4216:1)
[Warning][Deadcode] Function 'ldv_get_interface' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4217:1-4234:1)
[Warning][Deadcode] Function 'ldv_put_interface' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4235:1-4245:1)
[Warning][Deadcode] Function 'ldv_serial_register' is uncalled: 7 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4246:1-4263:1)
[Warning][Deadcode] Function 'ldv_serial_deregister' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4264:1-4274:1)
[Warning][Deadcode] Function 'dev_get_drvdata' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4301:1-4303:1)
[Warning][Deadcode] Function 'input_event' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4307:1-4309:1)
[Warning][Deadcode] Function 'usb_kill_urb' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4347:1-4349:1)
[Warning][Deadcode] Function 'ldv_check_final_state' has dead code:
  on line 4283 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4283-4283)
  on line 4287 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4287-4287)
  on line 4291 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4291-4291)
  on line 4295 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4295-4295)
[Warning][Deadcode] Function 'ldv_error' has dead code:
  on line 4058 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4058-4058)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 315
  dead: 127 (122 in uncalled functions)
  total lines: 442
[Warning][Deadcode][CWE-571] condition 'usb_counter == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3908:9-3908:54)
[Warning][Deadcode][CWE-571] condition 'ldv_state_variable_0 != 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3923:7-3923:32)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:12:73-12:74)
[Warning][Deadcode][CWE-570] condition '(unsigned long )usb_dev != (unsigned long )((struct usb_device *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4282:7-4282:74)
[Warning][Deadcode][CWE-570] condition 'dev_counter != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4286:7-4286:23)
[Warning][Deadcode][CWE-570] condition 'INTERF_STATE != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4290:7-4290:24)
[Warning][Deadcode][CWE-570] condition 'SERIAL_STATE != 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:4294:7-4294:24)
[Warning][Deadcode][CWE-570] condition '! cond' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-validator-v0.8/linux-stable-a450319-1-144_2a-drivers--input--tablet--acecad.ko-entry_point_ldv-val-v0.8.cil.out.i:3456:6-3456:11)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
