./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/if_etherip-fixed-invalid-deref2.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/if_etherip-fixed-invalid-deref2.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/openbsd-6.2/if_etherip-fixed-invalid-deref2.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
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1069: Warning: Ignoring identifier attribute
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2795: Warning: Ignoring identifier attribute
:-1: Warning: Incompatible declaration for clock_gettime (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:427 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i (0)) 
	Failed assumption that struct timespec and struct timespec are isomorphic 
	Failed assumption that time_t and __time_t are isomorphic (different integer types long long  and long )
struct timespec {
   time_t tv_sec ;
   long tv_nsec ;
};

struct timespec {
   __time_t tv_sec ;
   __syscall_slong_t tv_nsec ;
};
 
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1895:3-1897:27 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1930:9-1935:20 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1958:5-1968:5 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1975:5-1980:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1993:5-2000:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2001:5-2002:26 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2049:9-2054:20 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2065:3-2080:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:3-4954:3 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:3-4971:33 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4972:3-4976:1 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4982:3-5013:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5599:3-5600:13 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7549:3-7556:14 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7561:3-7567:14 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7584:5-7586:16 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7705:3-7719:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7836:3-7848:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7978:3-7995:3 with factor 3
[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] 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 ifq_serialize
[Info][Witness] couldn't parse entry: find uuid
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5600:5-5600:13)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (3192) (in bytes) with offset by ((Unknown int([-63,63]),[6,9223372036854775807],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5600:5-5600:13)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 320 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 87 (in bytes). It is offset by 384 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:151:3-151:52)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4971:5-4971:33)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 255 (in bytes). It is offset by 896 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1876:3-1876:51)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 255 (in bytes). It is offset by 256 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1878:3-1879:52)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:867:3-867:35)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:414:5-414:12)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 255 (in bytes). It is offset by 448 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:875:3-875:52)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:876:3-876:31)
[Info][Unsound] Unknown address in {&ref} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2934:3-2934:38)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2934:3-2934:38)
[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/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2925:3-2925:28)
[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/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2926:11-2926:18)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2935:3-2935:16)
[Warning][Unknown] Pointer counters + c has a points-to-set of top. An invalid memory access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2935:3-2935:16)
[Warning][Unknown] Size of lval dereference expression counters + c is top. Out-of-bounds memory access may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2935:3-2935:16)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of pointer counters in expression counters + c is top. Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2935:3-2935:16)
[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/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2929:3-2929:27)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Size of lval dereference expression is 255 (in bytes). It is offset by 448 (in bytes). Memory out-of-bounds access must occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4987:10-4987:46)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5006:7-5006:38)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5009:9-5009:23)
[Warning][Behavior > Undefined > MemoryOutOfBoundsAccess][CWE-823] Could not compare size of pointer (1344) (in bytes) with offset by ((Unknown int([0,16]),[0,28560],not {} ([-63,63]))) (in bytes). Memory out-of-bounds access might occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5009:9-5009:23)
[Warning][Behavior > Undefined > ArrayOutOfBounds > PastEnd] May access array past end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5011:5-5011:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5011:5-5011:46)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5011:5-5011:46)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7971:5-7971:15)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1896:5-1896:18)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1887:3-1887:49)
[Info][Unsound] Unknown value in {&ipsrc} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7976:3-7976:42)
[Warning][Unknown] lval (& ip6)->ip6_src points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5764:74-5764:74)
[Info][Unsound] Unknown value in {&ipdst} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7977:3-7977:42)
[Warning][Unknown] lval (& ip6)->ip6_dst points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5764:74-5764:74)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7997:12-7997:46)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5016:3-5016:15)
[Warning][Behavior > Undefined > ArrayOutOfBounds > Unknown] May access array out of bounds (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:759:10-759:20)
[Warning][Behavior > Undefined > MemoryLeak][CWE-401] Memory leak detected for heap variables (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:877:10-877:11)
[Warning][Deadcode] Function 'imax' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:369:1-369:66)
[Warning][Deadcode] Function 'imin' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:370:1-370:66)
[Warning][Deadcode] Function 'lmax' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:371:1-371:69)
[Warning][Deadcode] Function 'lmin' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:372:1-372:69)
[Warning][Deadcode] Function 'max' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:373:1-373:71)
[Warning][Deadcode] Function 'min' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:374:1-374:71)
[Warning][Deadcode] Function 'ulmax' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:375:1-375:76)
[Warning][Deadcode] Function 'ulmin' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:376:1-376:76)
[Warning][Deadcode] Function 'abs' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:377:1-377:59)
[Warning][Deadcode] Function 'openbsd_clock_gettime' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:428:1-431:1)
[Warning][Deadcode] Function 'satosin6' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:519:1-521:1)
[Warning][Deadcode] Function 'sin6tosa' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:522:1-524:1)
[Warning][Deadcode] Function 'ifatoia6' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:525:1-527:1)
[Warning][Deadcode] Function 'satosin' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:569:1-571:1)
[Warning][Deadcode] Function 'sintosa' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:572:1-574:1)
[Warning][Deadcode] Function 'ifatoia' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:575:1-577:1)
[Warning][Deadcode] Function 'sstosa' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:854:1-856:1)
[Warning][Deadcode] Function '__fd_set' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:891:1-894:1)
[Warning][Deadcode] Function '__fd_clr' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:895:1-898:1)
[Warning][Deadcode] Function '__fd_isset' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:899:1-902:1)
[Warning][Deadcode] Function 'bintime_addx' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:926:1-932:1)
[Warning][Deadcode] Function 'bintime_add' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:933:1-940:1)
[Warning][Deadcode] Function 'bintime_sub' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:941:1-948:1)
[Warning][Deadcode] Function 'bintime2timespec' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:949:1-953:1)
[Warning][Deadcode] Function 'timespec2bintime' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:954:1-957:1)
[Warning][Deadcode] Function 'bintime2timeval' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:958:1-961:1)
[Warning][Deadcode] Function 'timeval2bintime' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:962:1-965:1)
[Warning][Deadcode] Function 'xsave' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1217:1-1222:1)
[Warning][Deadcode] Function 'm_get' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1851:1-1863:1)
[Warning][Deadcode] Function 'm_leadingspace' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1900:1-1909:1)
[Warning][Deadcode] Function 'm_prepend' is uncalled: 27 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1910:1-1949:1)
[Warning][Deadcode] Function 'm_adj' is uncalled: 43 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1950:1-2004:1)
[Warning][Deadcode] Function 'm_pullup' is uncalled: 53 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2005:1-2086:1)
[Warning][Deadcode] Function 'm_trailingspace' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2087:1-2098:1)
[Warning][Deadcode] Function 'm_clget' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2099:1-2101:1)
[Warning][Deadcode] Function 'ifq_set_oactive' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2445:1-2447:1)
[Warning][Deadcode] Function 'ifq_clr_oactive' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2448:1-2450:1)
[Warning][Deadcode] Function 'ifq_is_oactive' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2451:1-2453:1)
[Warning][Deadcode] Function 'ifq_start' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2454:1-2456:1)
[Warning][Deadcode] Function 'ifq_restart' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2457:1-2459:1)
[Warning][Deadcode] Function 'ifq_idx' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2460:1-2463:1)
[Warning][Deadcode] Function '_atomic_cas_uint' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2802:1-2808:1)
[Warning][Deadcode] Function '_atomic_cas_ulong' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2809:1-2815:1)
[Warning][Deadcode] Function '_atomic_cas_ptr' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2816:1-2821:1)
[Warning][Deadcode] Function '_atomic_swap_uint' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2822:1-2826:1)
[Warning][Deadcode] Function '_atomic_swap_ulong' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2827:1-2831:1)
[Warning][Deadcode] Function '_atomic_swap_64' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2832:1-2835:1)
[Warning][Deadcode] Function '_atomic_swap_ptr' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2836:1-2841:1)
[Warning][Deadcode] Function '_atomic_inc_int' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2842:1-2844:1)
[Warning][Deadcode] Function '_atomic_inc_long' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2845:1-2847:1)
[Warning][Deadcode] Function '_atomic_dec_int' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2848:1-2850:1)
[Warning][Deadcode] Function '_atomic_dec_long' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2851:1-2853:1)
[Warning][Deadcode] Function '_atomic_add_int' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2854:1-2856:1)
[Warning][Deadcode] Function '_atomic_add_long' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2857:1-2860:1)
[Warning][Deadcode] Function '_atomic_sub_int' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2861:1-2863:1)
[Warning][Deadcode] Function '_atomic_sub_long' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2864:1-2867:1)
[Warning][Deadcode] Function '_atomic_add_int_nv' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2868:1-2873:1)
[Warning][Deadcode] Function '_atomic_add_long_nv' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2874:1-2879:1)
[Warning][Deadcode] Function '_atomic_sub_int_nv' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2880:1-2885:1)
[Warning][Deadcode] Function '_atomic_sub_long_nv' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2886:1-2891:1)
[Warning][Deadcode] Function 'x86_atomic_setbits_u32' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2892:1-2895:1)
[Warning][Deadcode] Function 'x86_atomic_clearbits_u32' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2896:1-2899:1)
[Warning][Deadcode] Function 'x86_atomic_setbits_u64' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2900:1-2903:1)
[Warning][Deadcode] Function 'x86_atomic_clearbits_u64' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2904:1-2907:1)
[Warning][Deadcode] Function 'counters_add' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2938:1-2944:1)
[Warning][Deadcode] Function 'counters_pkt' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2945:1-2953:1)
[Warning][Deadcode] Function 'rtstat_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:2962:1-2965:1)
[Warning][Deadcode] Function 'tcpstat_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:3617:1-3619:1)
[Warning][Deadcode] Function 'tcpstat_add' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:3620:1-3622:1)
[Warning][Deadcode] Function 'tcpstat_pkt' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:3623:1-3626:1)
[Warning][Deadcode] Function 'udpstat_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:3732:1-3734:1)
[Warning][Deadcode] Function 'icmp6stat_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:3945:1-3947:1)
[Warning][Deadcode] Function '_rb_init' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:3980:1-3982:1)
[Warning][Deadcode] Function '_rb_empty' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:3983:1-3985:1)
[Warning][Deadcode] Function 'ipipstat_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4378:1-4380:1)
[Warning][Deadcode] Function 'ipipstat_add' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4381:1-4383:1)
[Warning][Deadcode] Function 'ifmatoin6m' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4592:1-4594:1)
[Warning][Deadcode] Function 'ip6stat_inc' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4745:1-4747:1)
[Warning][Deadcode] Function 'ip6stat_add' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4748:1-4750:1)
[Warning][Deadcode] Function 'ip_init' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4831:1-4831:21)
[Warning][Deadcode] Function 'in6_domifattach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5019:1-5025:1)
[Warning][Deadcode] Function 'in6_domifdetach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5026:1-5031:1)
[Warning][Deadcode] Function 'ip6_ctloutput' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5032:1-5038:1)
[Warning][Deadcode] Function 'ip6_sysctl' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5039:1-5045:1)
[Warning][Deadcode] Function 'frag6_slowtimo' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5053:1-5058:1)
[Warning][Deadcode] Function 'frag6_drain' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5059:1-5064:1)
[Warning][Deadcode] Function 'udp_attach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5065:1-5071:1)
[Warning][Deadcode] Function 'udp_sysctl' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5079:1-5085:1)
[Warning][Deadcode] Function 'udp_usrreq' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5086:1-5093:1)
[Warning][Deadcode] Function 'udp6_ctlinput' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5094:1-5099:1)
[Warning][Deadcode] Function 'tcp_attach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5100:1-5106:1)
[Warning][Deadcode] Function 'tcp_ctloutput' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5107:1-5113:1)
[Warning][Deadcode] Function 'tcp_sysctl' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5121:1-5127:1)
[Warning][Deadcode] Function 'tcp_usrreq' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5128:1-5135:1)
[Warning][Deadcode] Function 'tcp6_ctlinput' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5136:1-5141:1)
[Warning][Deadcode] Function 'rip6_attach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5142:1-5148:1)
[Warning][Deadcode] Function 'rip6_ctlinput' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5149:1-5154:1)
[Warning][Deadcode] Function 'rip6_ctloutput' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5155:1-5161:1)
[Warning][Deadcode] Function 'rip6_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5162:1-5167:1)
[Warning][Deadcode] Function 'rip6_sysctl' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5175:1-5181:1)
[Warning][Deadcode] Function 'rip6_usrreq' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5182:1-5189:1)
[Warning][Deadcode] Function 'icmp6_fasttimo' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5190:1-5195:1)
[Warning][Deadcode] Function 'icmp6_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5196:1-5201:1)
[Warning][Deadcode] Function 'icmp6_sysctl' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5209:1-5215:1)
[Warning][Deadcode] Function 'splassert_fail' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5608:1-5613:1)
[Warning][Deadcode] Function 'ether_fakeaddr' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5614:1-5619:1)
[Warning][Deadcode] Function 'ifmedia_init' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5620:1-5626:1)
[Warning][Deadcode] Function 'ifmedia_add' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5627:1-5632:1)
[Warning][Deadcode] Function 'ifmedia_set' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5633:1-5638:1)
[Warning][Deadcode] Function 'if_attach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5639:1-5644:1)
[Warning][Deadcode] Function 'ether_ifattach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5645:1-5650:1)
[Warning][Deadcode] Function 'ifmedia_delete_instance' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5651:1-5656:1)
[Warning][Deadcode] Function 'ether_ifdetach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5657:1-5662:1)
[Warning][Deadcode] Function 'if_detach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5663:1-5668:1)
[Warning][Deadcode] Function 'if_clone_attach' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5669:1-5674:1)
[Warning][Deadcode] Function 'ifmedia_ioctl' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5675:1-5682:1)
[Warning][Deadcode] Function 'suser' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5683:1-5689:1)
[Warning][Deadcode] Function 'rtable_exists' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5690:1-5696:1)
[Warning][Deadcode] Function 'ether_ioctl' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5697:1-5703:1)
[Warning][Deadcode] Function 'ifq_dequeue' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5704:1-5711:1)
[Warning][Deadcode] Function 'bpf_mtap' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5712:1-5718:1)
[Warning][Deadcode] Function 'unhandled_af' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5719:1-5726:1)
[Warning][Deadcode] Function 'ip_randomid' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5727:1-5733:1)
[Warning][Deadcode] Function 'pf_pkt_addr_changed' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5734:1-5734:43)
[Warning][Deadcode] Function 'ip_output' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5735:1-5742:1)
[Warning][Deadcode] Function 'in6_embedscope' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5744:1-5751:1)
[Warning][Deadcode] Function 'ip6_output' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5752:1-5759:1)
[Warning][Deadcode] Function 'rtable_l2' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5760:1-5760:74)
[Warning][Deadcode] Function 'ml_enqueue' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5762:1-5762:55)
[Warning][Deadcode] Function 'if_input' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5763:1-5763:54)
[Warning][Deadcode] Function 'sysctl_int' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5765:1-5771:1)
[Warning][Deadcode] Function 'sysctl_struct' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5772:1-5778:1)
[Warning][Deadcode] Function 'satosdl' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:6114:1-6116:1)
[Warning][Deadcode] Function 'sdltosa' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:6117:1-6119:1)
[Warning][Deadcode] Function 'etheripattach' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7527:1-7527:67)
[Warning][Deadcode] Function 'etherip_clone_create' is uncalled: 23 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7528:1-7558:1)
[Warning][Deadcode] Function 'etherip_clone_destroy' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7559:1-7573:1)
[Warning][Deadcode] Function 'etherip_media_change' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7574:1-7574:57)
[Warning][Deadcode] Function 'etherip_media_status' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7575:1-7578:1)
[Warning][Deadcode] Function 'etherip_start' is uncalled: 22 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7579:1-7608:1)
[Warning][Deadcode] Function 'etherip_ioctl' is uncalled: 64 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7609:1-7699:1)
[Warning][Deadcode] Function 'etherip_set_tunnel_addr' is uncalled: 13 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7700:1-7724:1)
[Warning][Deadcode] Function 'ip_etherip_output' is uncalled: 50 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7725:1-7816:1)
[Warning][Deadcode] Function 'ip_etherip_input' is uncalled: 45 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7817:1-7878:1)
[Warning][Deadcode] Function 'ip6_etherip_output' is uncalled: 46 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7879:1-7960:1)
[Warning][Deadcode] Function 'ip_etherip_sysctl' is uncalled: 11 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:8026:1-8042:1)
[Warning][Deadcode] Function 'dest6_input' has dead code:
  on line 5219 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5219-5219)
  on line 5221 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5221-5221)
[Warning][Deadcode] Function 'frag6_input' has dead code:
  on line 5049 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5049-5049)
  on line 5051 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5051-5051)
[Warning][Deadcode] Function 'icmp6_input' has dead code:
  on line 5205 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5205-5205)
  on line 5207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5207-5207)
[Warning][Deadcode] Function 'ip6_etherip_input' has dead code:
  on line 7980 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7980-7980)
  on lines 7982..7984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7982-7984)
  on line 7992 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7992-7992)
  on lines 7999..8003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7999-8003)
  on lines 8005..8009 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:8005-8009)
  on lines 8011..8012 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:8011-8012)
  on lines 8014..8018 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:8014-8018)
  on lines 8020..8024 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:8020-8024)
[Warning][Deadcode] Function 'ip_deliver' has dead code:
  on line 4984 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4984-4984)
  on lines 4993..4994 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4993-4994)
  on lines 4997..4998 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4997-4998)
  on line 5003 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5003-5003)
[Warning][Deadcode] Function 'ipip_input' has dead code:
  on line 5233 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5233-5233)
  on line 5235 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5235-5235)
[Warning][Deadcode] Function 'm_free' has dead code:
  on line 1885 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1885-1885)
[Warning][Deadcode] Function 'm_freem' has dead code:
  on line 1893 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1893-1893)
[Warning][Deadcode] Function 'm_gethdr' has dead code:
  on line 1867 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1867-1867)
[Warning][Deadcode] Function 'panic' has dead code:
  on line 5605 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5605-5605)
  on line 5607 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5607-5607)
[Warning][Deadcode] Function 'pffindproto' has dead code:
  on line 4947 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4947-4947)
[Warning][Deadcode] Function 'reach_error' has dead code:
  on line 410 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:410-410)
[Warning][Deadcode] Function 'rip6_input' has dead code:
  on line 5171 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5171-5171)
  on line 5173 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5173-5173)
[Warning][Deadcode] Function 'route6_input' has dead code:
  on line 5226 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5226-5226)
  on line 5228 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5228-5228)
[Warning][Deadcode] Function 'tcp_input' has dead code:
  on line 5117 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5117-5117)
  on line 5119 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5119-5119)
[Warning][Deadcode] Function 'udp_input' has dead code:
  on line 5075 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5075-5075)
  on line 5077 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5077-5077)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 148
  dead: 785 (729 in uncalled functions)
  total lines: 933
[Warning][Deadcode][CWE-570] condition '(unsigned long )m___0 != (unsigned long )((void *)0)' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1897:10-1897:27)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-570] condition '(unsigned long )pr < (unsigned long )dp->dom_protoswNPROTOSW' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4948:7-4948:64)
[Warning][Deadcode][CWE-571] condition 'i < len' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5599:7-5599:27)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-570] condition 'family == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4946:7-4946:18)
[Warning][Deadcode][CWE-571] condition 'i < len' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5599:7-5599:27)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'i < len' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5599:7-5599:27)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition '(unsigned long )ifp == (unsigned long )((void *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7996:7-7996:25)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition '(unsigned long )maybe == (unsigned long )((void *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition '((int )m___0->m_hdr.mh_flags & 3072) == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7970:7-7970:69)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-570] condition '(unsigned long )sc != (unsigned long )((void *)0)' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:7978:7-7979:39)
[Warning][Deadcode][CWE-570] condition 'nxt != 257' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4982:10-4982:20)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-570] condition '(unsigned long )pr < (unsigned long )inet6domain.dom_protoswNPROTOSW' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4972:7-4972:80)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'nxt != 257' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4982:10-4982:20)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition 'af == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4983:9-4983:68)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'ip6_hdrnestlimit' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4983:9-4983:68)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-570] condition 'nest > ip6_hdrnestlimit' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4983:9-4983:68)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-570] condition 'nxt == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4992:5-4992:11)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-570] condition 'nxt == 41' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4996:5-4996:12)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-570] condition 'nowait == 0x0002' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1866:7-1866:51)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'i < 256' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4970:7-4970:27)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-570] condition 'af == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5002:5-5002:11)
[Warning][Deadcode][CWE-571] condition 'af == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5005:5-5005:12)
[Warning][Deadcode][CWE-571] condition 'i < len' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5599:7-5599:27)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:409:5-409:73)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition 'i < len' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5599:7-5599:27)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-570] condition '(unsigned long )m___0 == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1884:7-1884:23)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-570] condition '(unsigned long )m___0 == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:1892:7-1892:23)
[Warning][Deadcode][CWE-571] condition '(pr->pr_domain)->dom_family == 24' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Warning][Deadcode][CWE-571] condition 'type == 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4951:9-4952:29)
[Warning][Deadcode][CWE-571] condition 'i < len' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:5599:7-5599:27)
[Warning][Deadcode][CWE-571] condition '(int )pr->pr_protocol < 256' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/openbsd-6.2/if_etherip-fixed-invalid-deref2.i:4973:9-4974:56)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
[Error][Imprecise][Unsound] Function definition missing
