./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_valid-memsafety/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/valid-memsafety.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.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
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-free) ) -> enabling soundness analyses "base, useAfterFree"[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-deref) ) -> enabling soundness analyses "base, memOutOfBounds"[0;0;00m
[0;34m[Info] Setting "ana.arrayoob" to true[0;0;00m
[0;34m[Info] Setting "cil.addNestedScopeAttr" to true[0;0;00m
[0;34m[Info] Specification: CHECK( init(main()), LTL(G valid-memtrack) ) -> enabling soundness analyses "memLeak"[0;0;00m
[0;34m[Info] Setting "ana.malloc.unique_address_count" to 5[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] SV-COMP specification: CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )
[Error][Imprecise][Unsound] Function definition missing for __xadd_wrong_size
[Error][Imprecise][Unsound] Function definition missing for __bad_size_call_parameter
[Error][Imprecise][Unsound] Function definition missing for __bad_percpu_size
[Error][Imprecise][Unsound] Function definition missing for ldv_xmalloc
[Info][Witness] couldn't parse entry: find uuid

[Info] runtime: 00:00:10.309
[Info] vars: 8576, evals: 9468

[Info] |called|=45

Memory statistics: total=18398.87MB, max=268.97MB, minor=18395.16MB, major=596.77MB, promoted=593.05MB
    minor collections=8782  major collections=23 compactions=0


[Info] runtime: 00:00:20.418
[Info] vars: 14992, evals: 15996

[Info] |called|=44

Memory statistics: total=35915.40MB, max=470.43MB, minor=35911.27MB, major=1217.96MB, promoted=1213.83MB
    minor collections=17138  major collections=29 compactions=0


[Info] runtime: 00:00:30.474
[Info] vars: 20267, evals: 21614

[Info] |called|=22

Memory statistics: total=52540.36MB, max=622.15MB, minor=52535.26MB, major=1902.40MB, promoted=1897.31MB
    minor collections=25067  major collections=33 compactions=0


[Info] runtime: 00:00:40.541
[Info] vars: 24128, evals: 25711

[Info] |called|=18

Memory statistics: total=67914.41MB, max=715.47MB, minor=67908.92MB, major=2681.67MB, promoted=2676.18MB
    minor collections=32399  major collections=37 compactions=0

[Info][Unsound] Unknown value in {&(alloc@sid:163)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4503:7-4503:70)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3573:3-3573:62)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3574:3-3574:64)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3581:5-3581:39)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3765:7-3765:80)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3765:7-3765:80)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 2944 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3765:7-3765:80)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3765:7-3765:80)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3771:9-3771:75)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3771:9-3771:75)
[Warning][Unknown] Size of lval dereference expression s is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3771:9-3771:75)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3771:9-3771:75)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3771:9-3771:75)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3769:5-3769:17)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3769:5-3769:17)
[Warning][Unknown] Size of lval dereference expression s is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3769:5-3769:17)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3769:5-3769:17)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3769:5-3769:17)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3776:5-3776:23)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3776:5-3776:23)
[Warning][Unknown] Size of lval dereference expression s is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3776:5-3776:23)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3776:5-3776:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3776:5-3776:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3777:5-3777:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3777:5-3777:36)
[Warning][Unknown] Pointer s has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3777:5-3777:36)
[Warning][Unknown] Size of lval dereference expression s is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3777:5-3777:36)
[Warning][Behavior > Undefined > Other] Pointer s contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3777:5-3777:36)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer s is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3777:5-3777:36)
[Warning][Unknown] lval (& s)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4858:3-4858:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3778:5-3778:29)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3711:3-3711:47)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2672:11-2672:44)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3517:3-3517:38)
[Info][Unsound] Unknown value in {&gameport_event_lock.__annonCompField18.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3517:3-3517:38)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3518:3-3518:62)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3524:9-3524:67)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3524:9-3524:67)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3524:9-3524:67)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3524:9-3524:67)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3524:9-3524:67)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3522:7-3522:39)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3522:7-3522:39)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3522:7-3522:39)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3522:7-3522:39)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3531:3-3531:58)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3531:3-3531:58)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3531:3-3531:58)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3531:3-3531:58)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3534:7-3534:81)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3534:7-3534:81)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3534:7-3534:81)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3534:7-3534:81)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3523:5-3523:48)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3523:5-3523:48)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3523:5-3523:48)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3523:5-3523:48)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2692:3-2692:71)
[Info][Unsound] Unknown value in {&gameport_event_lock.__annonCompField18.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2692:3-2692:71)
[Warning][Unknown] lval (& lock)->__annonCompField18.rlock points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4808:3-4808:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3713:5-3713:50)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3481:3-3481:38)
[Info][Unsound] Unknown value in {&gameport_event_lock.__annonCompField18.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3481:3-3481:38)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3482:3-3482:62)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3484:3-3484:58)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3484:3-3484:58)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3484:3-3484:58)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3484:3-3484:58)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3497:7-3497:81)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3497:7-3497:81)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3497:7-3497:81)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3497:7-3497:81)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3488:7-3488:62)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3488:7-3488:62)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3488:7-3488:62)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3488:7-3488:62)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3489:5-3489:33)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3489:5-3489:33)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3489:5-3489:33)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3489:5-3489:33)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3489:5-3489:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2480:3-2480:26)
[Warning][Unknown] lval (& event)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2480:3-2480:26)
[Warning][Unknown] lval (& event)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4779:3-4779:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2481:3-2481:24)
[Warning][Unknown] lval (& event)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2481:3-2481:24)
[Warning][Unknown] Pointer list has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2463:3-2463:20)
[Warning][Unknown] Size of lval dereference expression list is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2463:3-2463:20)
[Warning][Behavior > Undefined > Other] Pointer list contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2463:3-2463:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer list is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2463:3-2463:20)
[Warning][Unknown] Pointer list has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2464:3-2464:20)
[Warning][Unknown] Size of lval dereference expression list is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2464:3-2464:20)
[Warning][Behavior > Undefined > Other] Pointer list contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2464:3-2464:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer list is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2464:3-2464:20)
[Warning][Unknown] lval (& event)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2465:3-2465:9)
[Warning][Unknown] lval (& event)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2482:3-2482:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3490:5-3490:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3332:3-3332:34)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3332:3-3332:34)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3332:3-3332:34)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3332:3-3332:34)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3332:3-3332:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4617:3-4617:32)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:163(#4)), (alloc@sid:163(#2)), (alloc@sid:163(#3)), (alloc@sid:163(#1)), (alloc@sid:163(#0)), (alloc@sid:163) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:12:83-12:230)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:12:83-12:230)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3333:3-3333:29)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)p in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4926:3-4926:18)
[Warning][Unknown] Pointer next has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3494:3-3494:57)
[Warning][Unknown] Size of lval dereference expression next is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3494:3-3494:57)
[Warning][Behavior > Undefined > Other] Pointer next contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3494:3-3494:57)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer next is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3494:3-3494:57)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3714:5-3714:29)
[Warning][Unknown] Pointer child has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3714:5-3714:29)
[Warning][Unknown] Size of lval dereference expression child is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3714:5-3714:29)
[Warning][Behavior > Undefined > Other] Pointer child contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3714:5-3714:29)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer child is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3714:5-3714:29)
[Warning][Unknown] lval (& child)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4908:3-4908:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3717:7-3717:81)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3717:7-3717:81)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3717:7-3717:81)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3717:7-3717:81)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3717:7-3717:81)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3718:6-3718:53)
[Warning][Unknown] Pointer gameport->parent has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3718:6-3718:53)
[Warning][Unknown] Size of lval dereference expression gameport->parent is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3718:6-3718:53)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3718:6-3718:53)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3718:6-3718:53)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3718:6-3718:53)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3718:6-3718:53)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3719:5-3719:44)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3719:5-3719:44)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3719:5-3719:44)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3719:5-3719:44)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3719:5-3719:44)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3719:5-3719:44)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3722:3-3722:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3722:3-3722:46)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3722:3-3722:46)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3722:3-3722:46)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3722:3-3722:46)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3722:3-3722:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2911:11-2911:42)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2911:11-2911:42)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2911:11-2911:42)
[Warning][Unknown] Pointer dev has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2911:11-2911:42)
[Warning][Unknown] Size of lval dereference expression dev is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2911:11-2911:42)
[Warning][Behavior > Undefined > Other] Pointer dev contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2911:11-2911:42)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer dev is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2911:11-2911:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3724:5-3724:32)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3724:5-3724:32)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3724:5-3724:32)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3724:5-3724:32)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3724:5-3724:32)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3724:5-3724:32)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4852:3-4852:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3727:3-3727:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3727:3-3727:34)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3727:3-3727:34)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3727:3-3727:34)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3727:3-3727:34)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3727:3-3727:34)
[Warning][Unknown] lval (& gameport)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2480:3-2480:26)
[Warning][Unknown] lval (& gameport)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4779:3-4779:9)
[Warning][Unknown] lval (& gameport)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2481:3-2481:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2463:3-2463:20)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2463:3-2463:20)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2463:3-2463:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2464:3-2464:20)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2464:3-2464:20)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2464:3-2464:20)
[Warning][Unknown] lval (& gameport)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2465:3-2465:9)
[Warning][Unknown] lval (& gameport)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2482:3-2482:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3728:3-3728:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3729:3-3729:30)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3729:3-3729:30)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3729:3-3729:30)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3729:3-3729:30)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3729:3-3729:30)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3729:3-3729:30)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4908:3-4908:9)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 4352 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4858:3-4858:9)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3585:7-3585:40)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Unknown] Pointer gameport->drv has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Unknown] Size of lval dereference expression gameport->drv is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3738:7-3738:183)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3743:5-3743:52)
[Warning][Imprecise][Call] Function pointer *((gameport->drv)->reconnect) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3743:5-3743:52)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3743:5-3743:52)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3751:3-3751:29)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3751:3-3751:29)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3751:3-3751:29)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3751:3-3751:29)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3739:5-3739:39)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3765:7-3765:80)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3765:7-3765:80)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3765:7-3765:80)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3765:7-3765:80)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3786:3-3786:41)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3740:5-3740:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Warning][Unknown] lval (& gameport)->dev 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 (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4845:10-4845:33)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4845:10-4845:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4837:3-4837:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3745:7-3745:41)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3746:7-3746:37)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3589:9-3589:43)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3590:9-3590:39)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 4352 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3295:3-3295:41)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].name} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].phys} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 4352 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3297:5-3298:76)
[Info][Unsound] Unknown value in {&(alloc@sid:163)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3592:9-3592:47)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3592:9-3592:47)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3594:11-3594:45)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:163(#4)), (alloc@sid:163(#2)), (alloc@sid:1519(#0)), (alloc@sid:163(#3)), (alloc@sid:163(#1)), (alloc@sid:163(#0)), (alloc@sid:163) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:12:83-12:230)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3596:11-3596:110)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3596:11-3596:110)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3271:3-3271:39)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 8320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3271:3-3271:39)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3271:3-3271:39)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 256 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3271:3-3271:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3272:3-3272:41)
[Warning][Imprecise][Call] Function pointer *(drv->connect) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3272:3-3272:41)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3272:3-3272:41)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3274:5-3274:53)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 8320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3274:5-3274:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3274:5-3274:53)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3278:3-3278:46)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3278:3-3278:46)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 4352 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3278:3-3278:46)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3278:3-3278:46)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4849:10-4849:33)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4849:10-4849:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3280:5-3282:20)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3280:5-3282:20)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].dev} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3280:5-3282:20)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].name} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3280:5-3282:20)
[Info][Unsound] Unknown value in {&(alloc@sid:163)[-544].phys} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3280:5-3282:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 4352 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3280:5-3282:20)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3280:5-3282:20)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3280:5-3282:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3283:6-3283:35)
[Warning][Imprecise][Call] Function pointer *(drv->disconnect) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3283:6-3283:35)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3283:6-3283:35)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3284:5-3284:53)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 119 (in bytes). It is offset by 8320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3284:5-3284:53)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3284:5-3284:53)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3603:3-3603:33)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3604:11-3604:59)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3604:11-3604:59)

[Info] runtime: 00:00:50.648
[Info] vars: 26999, evals: 28878

[Info] |called|=0

Memory statistics: total=84043.48MB, max=946.22MB, minor=84037.20MB, major=3373.28MB, promoted=3367.01MB
    minor collections=40091  major collections=39 compactions=0

[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:163(#4)), (alloc@sid:163(#2)), (alloc@sid:1519(#0)), (alloc@sid:163(#3)), (alloc@sid:163(#1)), (alloc@sid:1519(#1)), (alloc@sid:163(#0)), (alloc@sid:163) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:12:83-12:230)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:163(#4)), (alloc@sid:163(#2)), (alloc@sid:1519(#2)), (alloc@sid:1519(#0)), (alloc@sid:163(#3)), (alloc@sid:163(#1)), (alloc@sid:1519(#1)), (alloc@sid:163(#0)), (alloc@sid:163) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:12:83-12:230)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:163(#4)), (alloc@sid:163(#2)), (alloc@sid:1519(#3)), (alloc@sid:1519(#2)), (alloc@sid:1519(#0)), (alloc@sid:163(#3)), (alloc@sid:163(#1)), (alloc@sid:1519(#1)), (alloc@sid:163(#0)), (alloc@sid:163) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:12:83-12:230)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:1519(#4)), (alloc@sid:163(#4)), (alloc@sid:163(#2)), (alloc@sid:1519(#3)), (alloc@sid:1519(#2)), (alloc@sid:1519(#0)), (alloc@sid:163(#3)), (alloc@sid:163(#1)), (alloc@sid:1519(#1)), (alloc@sid:163(#0)), (alloc@sid:163) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:12:83-12:230)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] There is unreachable allocated heap memory at program exit. A memory leak might occur for the alloc vars (alloc@sid:1519(#4)), (alloc@sid:163(#4)), (alloc@sid:163(#2)), (alloc@sid:1519(#3)), (alloc@sid:1519(#2)), (alloc@sid:1519(#0)), (alloc@sid:163(#3)), (alloc@sid:1519), (alloc@sid:163(#1)), (alloc@sid:1519(#1)), (alloc@sid:163(#0)), (alloc@sid:163) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:12:83-12:230)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4044:3-4044:39)
[Info][Unsound] Unknown value in {&(alloc@sid:163)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4070:3-4070:45)
[Info][Unsound] Unknown value in {&(alloc@sid:163)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4445:7-4445:41)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3835:3-3835:67)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Warning][Imprecise] Trying to update a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Info][Imprecise] Invalidating expressions: buf (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Warning][Behavior > Undefined > Other] Pointer tmp___0 contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Warning][Unknown] Pointer tmp___0 has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer tmp___0 is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3836:3-3836:136)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4217:5-4217:48)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3381:3-3381:42)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3317:3-3317:38)
[Info][Unsound] Unknown value in {&gameport_event_lock.__annonCompField18.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3317:3-3317:38)
[Info][Unsound] Unknown value in {&gameport_event_list} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3318:3-3318:74)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3320:5-3320:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3322:5-3322:33)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3322:5-3322:33)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3322:5-3322:33)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3322:5-3322:33)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3322:5-3322:33)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3385:5-3385:12)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3385:5-3385:12)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3385:5-3385:12)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3385:5-3385:12)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3388:5-3388:12)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3388:5-3388:12)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3388:5-3388:12)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3388:5-3388:12)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3386:5-3386:56)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3386:5-3386:56)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3386:5-3386:56)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3386:5-3386:56)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3386:5-3386:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3677:7-3677:81)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3677:7-3677:81)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3677:7-3677:81)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3677:7-3677:81)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3677:7-3677:81)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3678:6-3678:41)
[Warning][Unknown] Pointer gameport->parent has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3678:6-3678:41)
[Warning][Unknown] Size of lval dereference expression gameport->parent is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3678:6-3678:41)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3678:6-3678:41)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3678:6-3678:41)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3678:6-3678:41)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3678:6-3678:41)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3682:5-3682:43)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2973:3-2973:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3996:7-3997:75)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3996:7-3997:75)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3996:7-3997:75)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3996:7-3997:75)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3996:7-3997:75)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3998:5-3998:46)
[Warning][Imprecise][Call] Function pointer *(gameport->open) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3998:5-3998:46)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3998:5-3998:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4008:3-4008:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3986:3-3986:47)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3986:3-3986:47)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3986:3-3986:47)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3986:3-3986:47)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3986:3-3986:47)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3986:3-3986:47)
[Warning][Unknown] lval (& gameport)->drv_mutex points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4898:3-4898:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3987:3-3987:22)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3987:3-3987:22)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3987:3-3987:22)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3987:3-3987:22)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3987:3-3987:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3988:3-3988:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3988:3-3988:38)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3988:3-3988:38)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3988:3-3988:38)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3988:3-3988:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3988:3-3988:38)
[Warning][Unknown] lval (& gameport)->drv_mutex points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4901:3-4901:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2988:3-2988:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2938:7-2938:99)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2938:7-2938:99)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2938:7-2938:99)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2938:7-2938:99)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2938:7-2938:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2939:5-2939:40)
[Warning][Imprecise][Call] Function pointer *(gameport->read) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2939:5-2939:40)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2939:5-2939:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2942:5-2942:32)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2942:5-2942:32)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2942:5-2942:32)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2942:5-2942:32)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2942:5-2942:32)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2754:3-2754:63)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2551:3-2553:29)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2545:5-2546:48)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2610:3-2612:29)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2604:5-2605:48)
[Error][Imprecise][Unsound] Function definition missing for ldv_xmalloc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Imprecise] INVALIDATING ALL GLOBALS! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Imprecise] Invalidating expressions: & ldv_module_refcounter, & ldv_retval_1, & ldv_retval_0, & __ksymtab_gameport_close, & __ksymtab_gameport_open, & __ksymtab_gameport_unregister_driver, & __ksymtab___gameport_register_driver, & __ksymtab_gameport_unregister_port, & __ksymtab___gameport_register_port, & __ksymtab_gameport_set_phys, & __ksymtab_gameport_stop_polling, & __ksymtab_gameport_start_polling, & ldv_state_variable_4, & ldv_state_variable_7, & ldv_state_variable_1, & ldv_work_1_0, & ref_cnt, & ldv_timer_list_2, & ldv_state_variable_3, & ldv_timer_state_2, & ldv_work_struct_1_2, & LDV_IN_INTERRUPT, & ldv_work_1_2, & gameport_bus_group0, & ldv_work_1_1, & ldv_state_variable_2, & ldv_state_variable_5, & ldv_state_variable_0, & ldv_state_variable_6, & ldv_work_1_3, & ldv_work_struct_1_3, & ldv_work_struct_1_1, & ldv_work_struct_1_0, sizeof(union ktime ) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab_gameport_close} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab_gameport_open} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab_gameport_unregister_driver} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab___gameport_register_driver} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab_gameport_unregister_port} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab___gameport_register_port} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab_gameport_set_phys} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab_gameport_stop_polling} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&__ksymtab_gameport_start_polling} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&ldv_timer_list_2} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&ldv_work_struct_1_2} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&gameport_bus_group0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown value in {&(alloc@sid:163)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&ldv_work_struct_1_3} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&ldv_work_struct_1_1} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Unsound] Unknown address in {&ldv_work_struct_1_0} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4878:10-4878:58)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2716:11-2716:26)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2581:3-2583:48)
[Info][Unsound] ASM statement ignored. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2575:5-2576:48)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3006:3-3006:88)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3006:3-3006:88)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3017:3-3017:27)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4022:3-4022:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4022:3-4022:48)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4022:3-4022:48)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4022:3-4022:48)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4022:3-4022:48)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4022:3-4022:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4648:3-4648:38)
[Warning][Unknown] lval (& gameport)->poll_timer points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4648:3-4648:38)
[Warning][Unknown] lval (& gameport)->poll_timer 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 (& gameport)->poll_timer points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4827:10-4827:33)
[Warning][Unknown] lval (& gameport)->poll_timer points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4827:10-4827:33)
[Warning][Unknown] lval (& gameport)->poll_timer points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4649:3-4649:21)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4650:3-4650:42)
[Warning][Unknown] lval (& gameport)->poll_timer points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4650:3-4650:42)
[Warning][Unknown] lval (& gameport)->poll_timer points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4180:5-4180:11)
[Warning][Unknown] lval (& gameport)->poll_timer points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4183:3-4183:9)
[Warning][Unknown] lval (& gameport)->poll_timer points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4651:11-4651:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4023:3-4023:59)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4023:3-4023:59)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4023:3-4023:59)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4023:3-4023:59)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4023:3-4023:59)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4024:3-4024:31)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4024:3-4024:31)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4024:3-4024:31)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4024:3-4024:31)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4024:3-4024:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4025:3-4025:58)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4026:7-4026:91)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4026:7-4026:91)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4026:7-4026:91)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4026:7-4026:91)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4026:7-4026:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4027:6-4027:35)
[Warning][Imprecise][Call] Function pointer *(gameport->close) may contain unknown functions. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4027:6-4027:35)
[Warning][Unsound][Call] No suitable function to be called at call site. Continuing with state before call. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4027:6-4027:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3683:5-3683:26)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3683:5-3683:26)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3683:5-3683:26)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3683:5-3683:26)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3683:5-3683:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3688:3-3688:51)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3688:3-3688:51)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3688:3-3688:51)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3688:3-3688:51)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3688:3-3688:51)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3688:3-3688:51)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2472:3-2472:36)
[Warning][Unknown] lval (& gameport)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2472:3-2472:36)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 15 (in bytes). It is offset by 64 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2472:3-2472:36)
[Warning][Unknown] lval (& gameport)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4776:3-4776:9)
[Warning][Unknown] lval (& gameport)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2473:3-2473:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3689:7-3689:24)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3689:7-3689:24)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3689:7-3689:24)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3689:7-3689:24)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3689:7-3689:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3690:5-3692:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3690:5-3692:31)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3690:5-3692:31)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3690:5-3692:31)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3690:5-3692:31)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3690:5-3692:31)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4795:3-4795:9)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3694:5-3695:87)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3694:5-3695:87)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3694:5-3695:87)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3694:5-3695:87)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3694:5-3695:87)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3694:5-3695:87)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3697:3-3697:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3697:3-3697:38)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3697:3-3697:38)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3697:3-3697:38)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3697:3-3697:38)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3697:3-3697:38)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4841:10-4841:33)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4841:10-4841:33)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3699:5-3700:75)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3699:5-3700:75)
[Warning][Unknown] Pointer gameport has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3699:5-3700:75)
[Warning][Unknown] Size of lval dereference expression gameport is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3699:5-3700:75)
[Warning][Behavior > Undefined > Other] Pointer gameport contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3699:5-3700:75)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer gameport is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3699:5-3700:75)
[Warning][Unknown] lval (& gameport)->dev points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4830:3-4830:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3389:5-3389:68)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3389:5-3389:68)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3389:5-3389:68)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3389:5-3389:68)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3389:5-3389:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3880:3-3880:39)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3880:3-3880:39)
[Warning][Unknown] Pointer drv has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3880:3-3880:39)
[Warning][Unknown] Size of lval dereference expression drv is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3880:3-3880:39)
[Warning][Behavior > Undefined > Other] Pointer drv contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3880:3-3880:39)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer drv is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3880:3-3880:39)
[Warning][Unknown] lval (& drv)->driver 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 (& drv)->driver points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4862:10-4862:33)
[Warning][Unknown] lval (& drv)->driver points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4862:10-4862:33)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3882:5-3883:18)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3882:5-3883:18)
[Warning][Unknown] Pointer drv has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3882:5-3883:18)
[Warning][Unknown] Size of lval dereference expression drv is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3882:5-3883:18)
[Warning][Behavior > Undefined > Other] Pointer drv contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3882:5-3883:18)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer drv is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3882:5-3883:18)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3393:5-3393:44)
[Warning][Imprecise][Program] Trying to read a field, but was not given a struct (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3348:3-3348:38)
[Info][Unsound] Unknown value in {&gameport_event_lock.__annonCompField18.rlock} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3348:3-3348:38)
[Info][Imprecise] Trying to read a field, but the struct is unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3349:3-3349:62)
[Warning][Unknown] Pointer e has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3351:3-3351:54)
[Warning][Unknown] Size of lval dereference expression e is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3351:3-3351:54)
[Warning][Behavior > Undefined > Other] Pointer e contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3351:3-3351:54)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer e is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3351:3-3351:54)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3356:9-3356:61)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3356:9-3356:61)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3356:9-3356:61)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3356:9-3356:61)
[Warning][Unknown] Pointer e has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3356:9-3356:61)
[Warning][Unknown] Size of lval dereference expression e is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3356:9-3356:61)
[Warning][Behavior > Undefined > Other] Pointer e contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3356:9-3356:61)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer e is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3356:9-3356:61)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3360:5-3360:29)
[Warning][Unknown] Pointer e has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3360:5-3360:29)
[Warning][Unknown] Size of lval dereference expression e is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3360:5-3360:29)
[Warning][Behavior > Undefined > Other] Pointer e contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3360:5-3360:29)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer e is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3360:5-3360:29)
[Warning][Unknown] lval (& e)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2480:3-2480:26)
[Warning][Unknown] lval (& e)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4779:3-4779:9)
[Warning][Unknown] lval (& e)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2481:3-2481:24)
[Warning][Unknown] lval (& e)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2465:3-2465:9)
[Warning][Unknown] lval (& e)->node points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:2482:3-2482:9)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3361:5-3361:27)
[Warning][Unknown] Pointer event has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3355:7-3355:65)
[Warning][Unknown] Size of lval dereference expression event is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3355:7-3355:65)
[Warning][Behavior > Undefined > Other] Pointer event contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3355:7-3355:65)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer event is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3355:7-3355:65)
[Warning][Unknown] Pointer e has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3355:7-3355:65)
[Warning][Unknown] Size of lval dereference expression e is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3355:7-3355:65)
[Warning][Behavior > Undefined > Other] Pointer e contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3355:7-3355:65)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer e is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3355:7-3355:65)
[Warning][Unknown] Pointer next has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3365:3-3365:57)
[Warning][Unknown] Size of lval dereference expression next is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3365:3-3365:57)
[Warning][Behavior > Undefined > Other] Pointer next contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3365:3-3365:57)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer next is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3365:3-3365:57)
[Warning][Unknown] Pointer e has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3368:7-3368:77)
[Warning][Unknown] Size of lval dereference expression e is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3368:7-3368:77)
[Warning][Behavior > Undefined > Other] Pointer e contains an unknown address. Invalid dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3368:7-3368:77)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer e is top. Memory out-of-bounds access might occur due to pointer arithmetic (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3368:7-3368:77)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3394:5-3394:31)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:3397:3-3397:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4225:5-4225:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4233:5-4233:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--input--gameport--gameport.ko-entry_point.cil.out.i:4241:5-4241:48)

[Info] runtime: 00:01:00.691
[Info] vars: 26999, evals: 28878

[Info] |called|=0

Memory statistics: total=102488.96MB, max=946.22MB, minor=102482.14MB, major=3783.64MB, promoted=3776.83MB
    minor collections=48887  major collections=41 compactions=0

