./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 64bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i


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


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2850:3-2861:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2889:3-2902:3 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2909:3-2918:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2939:3-2946:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3073:3-3081:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:3-3092:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3232:3-3238:18 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3264:3-3270:18 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3326:3-3327:39 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3394:3-3395:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3396:3-3397:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3448:3-3449:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3455:3-3461:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:3-3476:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:5-3491:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3485:3-3492:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3494:3-3495:23 with factor 12
[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] longjmp -> enabling longjmp analyses "activeLongjmp, activeSetjmp, taintPartialContexts, modifiedSinceSetjmp, poisonVariables, expsplit, vla"
[Info] Setting "ana.int.interval" to true
[Info] function aexpr is recursive, disable interval and interval_set contexts
[Info] function nexpr is recursive, disable interval and interval_set contexts
[Info] function oexpr is recursive, disable interval and interval_set contexts
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )

[Info] runtime: 00:00:10.187
[Info] vars: 17460, evals: 39041

[Info] |called|=107

Memory statistics: total=24020.35MB, max=132.00MB, minor=24014.22MB, major=256.00MB, promoted=249.88MB
    minor collections=11459  major collections=17 compactions=0

[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3482:8-3482:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3482:8-3482:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3482:8-3482:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3483:8-3483:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3483:8-3483:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3483:8-3483:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3491:7-3491:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3491:7-3491:42)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3145:3-3145:45)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2573:3-2573:23)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3152:6-3152:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3154:5-3154:20)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3157:10-3157:59)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2582:3-2582:49)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2605:3-2605:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2605:3-2605:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2605:3-2605:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2610:3-2610:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2610:3-2610:74)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)msg in function realloc is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2625:3-2625:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2625:3-2625:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2625:3-2625:116)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2625:3-2625:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2641:5-2641:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2643:5-2643:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2644:5-2644:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2660:5-2660:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2766:3-2766:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2766:3-2766:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2665:5-2665:62)
[Info][Unsound] Unknown value in {&(alloc@sid:77)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2665:5-2665:62)
[Info][Unsound] Unknown value in {&(alloc@sid:77)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2852:5-2852:32)
[Info][Unsound] Unknown value in {&(alloc@sid:77)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2850:6-2850:58)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2852:5-2852:32)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([0,63]); intervals:[0,9223372036854775807]; enums:not {} ([0,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2859:5-2859:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2850:6-2850:58)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2852:5-2852:32)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3075:5-3075:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2859:5-2859:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2850:6-2850:58)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2852:5-2852:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2859:5-2859:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2850:6-2850:58)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2852:5-2852:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2859:5-2859:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2850:6-2850:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2859:5-2859:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2850:6-2850:58)
[Info][Unsound] Unknown value in {&(alloc@sid:77)[def_exc:Unknown int([-63,63]); intervals:[0,9223372036854775807]; enums:not {} ([-63,63])]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2852:5-2852:32)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3191:9-3191:111)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(argv + (long )argc) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3229:5-3229:38)
[Info][Unsound] Unknown value in {&(alloc@sid:1472)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3236:5-3236:100)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3239:3-3239:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3239:3-3239:44)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3249:7-3249:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3250:7-3250:79)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3250:7-3250:79)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2746:3-2746:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2749:3-2749:35)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2900:5-2900:88)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2901:5-2901:18)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2752:3-2752:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2955:5-2955:63)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2956:5-2956:49)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2956:5-2956:49)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2959:7-2959:65)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3007:5-3007:63)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3009:5-3009:77)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3009:5-3009:77)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2979:3-2979:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2981:3-2981:75)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2981:3-2981:75)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2985:5-2985:63)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2987:5-2987:77)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2987:5-2987:77)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2994:3-2994:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3011:5-3011:63)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3013:5-3013:77)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3013:5-3013:77)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3106:5-3106:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2582:3-2582:49)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2605:3-2605:29)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3449:73-3449:84)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3107:3-3107:43)
[Warning][Imprecise] Jump buffer (struct __jmp_buf_tag *)(test_ptr_to_statics->leaving) may contain unknown pointers. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3107:3-3107:43)
[Warning][Imprecise] Longjmp to potentially invalid target, as contents of buffer (struct __jmp_buf_tag *)(test_ptr_to_statics->leaving) may be unknown! (imprecision due to heap?) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3107:3-3107:43)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3019:3-3019:48)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3021:3-3021:94)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3021:3-3021:94)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3025:8-3025:69)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3027:10-3027:70)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2678:3-2678:37)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2679:3-2679:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2680:3-2680:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2680:3-2680:45)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2681:3-2681:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2682:3-2682:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2683:3-2683:37)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2686:5-2686:80)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2686:5-2686:80)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3104:5-3104:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2688:6-2688:66)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2705:6-2705:66)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2724:3-2724:39)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3365:3-3365:51)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3367:3-3367:49)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3368:3-3368:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3370:3-3370:50)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3371:3-3371:57)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3372:3-3372:55)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3373:3-3373:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3374:3-3374:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3375:3-3375:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2731:5-2731:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2736:6-2736:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2738:6-2738:34)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3036:6-3036:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3038:8-3038:66)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3040:5-3040:63)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3043:14-3043:115)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3047:14-3047:115)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3051:7-3051:59)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3051:7-3051:59)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )(& p) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2869:3-2869:23)
[Info][Imprecise] Invalidating expressions: & r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2869:3-2869:23)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2878:5-2878:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3087:8-3087:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2879:5-2879:122)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2882:5-2882:28)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3052:7-3052:68)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3056:5-3056:66)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3056:5-3056:66)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2776:5-2776:39)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3386:10-3386:25)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2785:3-2785:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3059:6-3059:66)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3067:10-3067:111)

[Info] runtime: 00:00:20.241
[Info] vars: 25545, evals: 67256

[Info] |called|=0

Memory statistics: total=47371.17MB, max=200.75MB, minor=47363.60MB, major=443.61MB, promoted=436.04MB
    minor collections=22595  major collections=21 compactions=0

[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2551:3-2551:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2553:3-2553:75)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2553:3-2553:75)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2557:5-2557:63)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2559:5-2559:77)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2559:5-2559:77)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2566:3-2566:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3253:10-3253:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3255:9-3255:67)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3256:12-3256:66)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3258:11-3258:74)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3258:11-3258:74)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)test_ptr_to_statics in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3268:5-3268:38)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)*(mem_track + i___1) in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3495:5-3495:23)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:76:1-80:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:81:1-85:1)
[Warning][Deadcode] Function 'bb_error_msg_and_die' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2585:1-2592:1)
[Warning][Deadcode] Function 'initialize_group_array' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2905:1-2919:1)
[Warning][Deadcode] Function 'is_a_group_member' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2920:1-2948:1)
[Warning][Deadcode] Function 'test_eaccess' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3109:1-3137:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3138:1-3140:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3273:1-3282:1)
[Warning][Deadcode] Function 'xrealloc' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3294:1-3303:1)
[Warning][Deadcode] Function 'getgroups' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3315:1-3329:1)
[Warning][Deadcode] Function 'getuid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3330:1-3333:1)
[Warning][Deadcode] Function 'getgid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3338:1-3341:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3350:1-3354:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3389:1-3399:1)
[Warning][Deadcode] Function 'getopt' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3400:1-3426:1)
[Warning][Deadcode] Function 'getopt_long' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3427:1-3433:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3434:1-3442:1)
[Warning][Deadcode] Function '__main' has dead code:
  on line 3207 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3207-3207)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2602 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2602-2602)
  on line 2604 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2604-2604)
  on lines 2615..2616 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2615-2616)
  on lines 2632..2635 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2632-2635)
  on line 2647 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2647-2647)
  on lines 2649..2654 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2649-2654)
  on lines 2656..2657 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2656-2657)
  on line 2668 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2668-2668)
[Warning][Deadcode] Function 'binop' has dead code:
  on lines 2690..2702 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2690-2702)
  on lines 2710..2719 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2710-2719)
[Warning][Deadcode] Function 'check_operator' has dead code:
  on line 2756 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2756-2756)
[Warning][Deadcode] Function 'filstat' has dead code:
  on lines 2792..2797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2792-2797)
  on lines 2799..2800 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2799-2800)
  on lines 2804..2815 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2804-2815)
  on lines 2822..2828 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2822-2828)
[Warning][Deadcode] Function 'getn' has dead code:
  on line 2871 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2871-2871)
[Warning][Deadcode] Function 'xmalloc' has dead code:
  on lines 3289..3290 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3289-3290)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 381
  dead: 181 (108 in uncalled functions)
  total lines: 562
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-570] condition '255 + (int )((unsigned char )mode) <= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2790:6-2790:48)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-570] condition '(_Bool)0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3238:9-3238:18)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-570] condition '251 + (int )((unsigned char )mode) <= 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2802:6-2802:48)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:6-3475:25)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-570] condition '242 + (int )((unsigned char )mode) <= 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2820:6-2820:48)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:6-3475:25)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:6-3475:25)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:22:73-22:74)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:6-3475:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:6-3475:25)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:6-3475:25)
[Warning][Deadcode][CWE-571] condition 'res == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3242:6-3242:14)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2855:10-2855:24)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:6-3475:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3475:6-3475:25)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-570] condition '(_Bool)0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3270:9-3270:18)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2601:6-2601:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-570] condition '(unsigned long )s == (unsigned long )((char const   *)((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2603:6-2603:38)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )strerr == (unsigned long )((char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2613:6-2613:46)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-570] condition '(unsigned long )msg1 == (unsigned long )((char *)((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2630:6-2630:35)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )strerr == (unsigned long )((char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2645:8-2645:48)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-570] condition '! (*bb_errno == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2870:6-2870:23)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2662:6-2662:39)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2667:6-2667:39)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-570] condition '228 + (int )((unsigned char )((int )op->op_num)) <= 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2688:6-2688:66)
[Warning][Deadcode][CWE-571] condition 'i < result_buffer_size' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3455:9-3455:29)
[Warning][Deadcode][CWE-570] condition '234 + (int )((unsigned char )((int )op->op_num)) <= 5' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2705:6-2705:66)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3173:10-3173:18)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '__s2_len < 4UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3178:9-3178:109)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
[Warning][Deadcode][CWE-571] condition '2l * (long )n >= 0l' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:2753:6-2753:35)
[Warning][Deadcode][CWE-570] condition '(unsigned long )ptr == (unsigned long )((void *)0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3287:6-3287:24)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3490:8-3490:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3086:6-3086:30)
[Warning][Deadcode][CWE-571] condition '! (247 + (int )((unsigned char )((int )*s)) <= 4)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/test-incomplete-1.i:3089:10-3089:65)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
[Error][Unsound][Imprecise][Call] Longjmp to unknown target ignored
