./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/yes-2.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/yes-2.i:2349:3-2360:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2367:3-2375:35 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2401:5-2408:5 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2425:3-2426:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2427:3-2428:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2479:3-2480:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2486:3-2492:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2506:3-2507:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2521:5-2522:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2516:3-2523:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2525:3-2526: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] 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) )
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2513:8-2513:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2513:8-2513:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2513:8-2513:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2514:8-2514:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2514:8-2514:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2514:8-2514:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2522:7-2522:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2522:7-2522:42)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stdout (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown address in (FILE * __restrict  )stdout has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2403:7-2403:25)
[Info][Imprecise] Invalidating expressions: & return_value_putchar_unlocked$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2409:5-2409:48)
[Info][Imprecise] Invalidating expressions: & return_value_strerror$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2248:5-2248:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2253:3-2253:37)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2253:3-2253:37)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2273:3-2273:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2273:3-2273:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2273:3-2273:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2278:3-2278:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2278:3-2278:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2288:3-2288:41)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2288:3-2288:41)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2293:3-2293:116)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2293:3-2293:116)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2311:5-2311:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2312:5-2312:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2318:9-2318:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2321:9-2321:24)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2325:7-2325:31)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2325:7-2325:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2325:7-2325:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2328:5-2328:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2342:3-2342:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2342:3-2342:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2333:5-2333:62)
[Info][Unsound] Unknown value in {&(alloc@sid:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2333:5-2333:62)
[Info][Unsound] Unknown value in {&(alloc@sid:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2351:5-2351:32)
[Info][Unsound] Unknown value in {&(alloc@sid:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2369:5-2369:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2349:6-2349:58)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2351:5-2351:32)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2358:5-2358:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2349:6-2349:58)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2351:5-2351:32)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2369:5-2369:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2358:5-2358:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2349:6-2349:58)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2351:5-2351:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2358:5-2358:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2349:6-2349:58)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2351:5-2351:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2358:5-2358:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2349:6-2349:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2358:5-2358:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2349:6-2349:58)
[Info][Unsound] Unknown value in {&(alloc@sid:51)[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/yes-2.i:2351:5-2351:32)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:22:1-22:169)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.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/yes-2.i:81:1-85:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2378:1-2387:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2388:1-2390:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2414:1-2418:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2420:1-2430:1)
[Warning][Deadcode] Function 'getopt' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2431:1-2457:1)
[Warning][Deadcode] Function 'getopt_long' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2458:1-2464:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2465:1-2473:1)
[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function '__main' has dead code:
  on line 2413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2413-2413)
[Warning][Deadcode] Function 'bb_perror_nomsg_and_die' has dead code:
  on line 2260 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2260-2260)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2270-2270)
  on line 2275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2275-2275)
  on lines 2300..2303 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2300-2303)
  on line 2336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2336-2336)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 2525..2530 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2525-2530)
[Warning][Deadcode] Function 'vasprintf' has dead code:
  on lines 2481..2486 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2481-2486)
  on lines 2488..2489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2488-2489)
  on line 2491 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2491-2491)
  on lines 2493..2494 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2493-2494)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 121
  dead: 71 (45 in uncalled functions)
  total lines: 192
[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/yes-2.i:2506:6-2506:25)
[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/yes-2.i:2521:8-2521: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/yes-2.i:2401:11-2401:19)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2330:6-2330:39)
[Warning][Deadcode][CWE-570] condition 's < tmp' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2479:6-2479:41)
[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/yes-2.i:2521:8-2521:27)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2335:6-2335:39)
[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/yes-2.i:2401:11-2401:19)
[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/yes-2.i:2521:8-2521: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/yes-2.i:2521:8-2521: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/yes-2.i:2401:11-2401:19)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2354:10-2354: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/yes-2.i:2521:8-2521: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/yes-2.i:2521:8-2521: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/yes-2.i:2401:11-2401:19)
[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/yes-2.i:2521:8-2521: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/yes-2.i:2521:8-2521: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/yes-2.i:2521:8-2521: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/yes-2.i:2521:8-2521: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/yes-2.i:2521:8-2521: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/yes-2.i:2521:8-2521:27)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2269:6-2269: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/yes-2.i:2521:8-2521: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/yes-2.i:2401:11-2401:19)
[Warning][Deadcode][CWE-571] condition '(unsigned long )s == (unsigned long )((char const   *)((void *)0))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2271:6-2271:38)
[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/yes-2.i:2506:6-2506:25)
[Warning][Deadcode][CWE-571] condition 'no_format' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2480:6-2480:15)
[Warning][Deadcode][CWE-570] condition 'used < 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/yes-2.i:2274:6-2274:14)
[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/yes-2.i:2521:8-2521:27)
[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/yes-2.i:2506:6-2506: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/yes-2.i:2401:11-2401:19)
[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/yes-2.i:2506:6-2506: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/yes-2.i:2401:11-2401:19)
[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/yes-2.i:2506:6-2506:25)
[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/yes-2.i:2298:6-2298:35)
[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/yes-2.i:2506:6-2506: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/yes-2.i:2401:11-2401:19)
[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/yes-2.i:2506:6-2506:25)
[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/yes-2.i:2521:8-2521:27)
[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/yes-2.i:2506:6-2506: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/yes-2.i:2401:11-2401:19)
[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/yes-2.i:2521:8-2521:27)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
