./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/chroot-incomplete-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/chroot-incomplete-2.i:2435:3-2446:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2476:3-2484:35 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2552:2-2553:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2592:3-2593:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2594:3-2595:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2646:3-2647:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2653:3-2659:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2673:3-2674:34 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2688:5-2689:42 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2683:3-2690:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2692:3-2693:23 with factor 2
[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/chroot-incomplete-2.i:2680:8-2680:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2680:8-2680:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2680:8-2680:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2681:8-2681:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2681:8-2681:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2681:8-2681:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2689:7-2689:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2689:7-2689:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2689:7-2689:42)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2413:3-2413:17)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2498:3-2498:37)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2500:5-2500:71)
[Info][Imprecise] Invalidating expressions: & return_value_strerror$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2314:5-2314:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2319:3-2319:37)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2319:3-2319:37)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2339:3-2339:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2339:3-2339:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2339:3-2339:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2344:3-2344:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2344:3-2344:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2354:3-2354:41)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2354:3-2354:41)
[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/chroot-incomplete-2.i:2359:3-2359:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2359:3-2359:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2359:3-2359:116)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2359:3-2359:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2375:5-2375:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2377:5-2377:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2378:5-2378:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2384:9-2384:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2387:9-2387:24)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2391:7-2391:31)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2391:7-2391:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2391:7-2391:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2394:5-2394:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2428:3-2428:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2428:3-2428:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2399:5-2399:62)
[Info][Unsound] Unknown value in {&(alloc@sid:71)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2399:5-2399:62)
[Info][Unsound] Unknown value in {&(alloc@sid:71)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2437:5-2437:32)
[Info][Unsound] Unknown value in {&(alloc@sid:71)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2478:5-2478:28)
[Info][Unsound] Unknown value in {&(alloc@sid:71)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2478:5-2478:28)
[Info][Unsound] Unknown value in {&(alloc@sid:71)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2478:5-2478:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2435:6-2435:58)
[Info][Unsound] Unknown value in {&(alloc@sid:71)[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/chroot-incomplete-2.i:2437:5-2437:32)
[Info][Unsound] Unknown value in {&(alloc@sid:71)[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/chroot-incomplete-2.i:2478:5-2478:28)
[Info][Unsound] Unknown value in {&(alloc@sid:71)[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/chroot-incomplete-2.i:2478:5-2478:28)
[Info][Unsound] Unknown value in {&(alloc@sid:71)[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/chroot-incomplete-2.i:2478:5-2478:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2444:5-2444:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2435:6-2435:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2444:5-2444:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2435:6-2435:58)
[Info][Unsound] Unknown value in {&(alloc@sid:71)[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/chroot-incomplete-2.i:2437:5-2437:32)
[Info][Unsound] Unknown value in {&(alloc@sid:71)[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/chroot-incomplete-2.i:2478:5-2478:28)
[Info][Unsound] Unknown value in {&(alloc@sid:71)[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/chroot-incomplete-2.i:2478:5-2478:28)
[Info][Unsound] Unknown value in {&(alloc@sid:71)[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/chroot-incomplete-2.i:2478:5-2478:28)
[Info][Imprecise] Invalidating expressions: & shell (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2453:3-2453:24)
[Info][Unsound] Unknown address in {&(alloc@sid:671)[def_exc:Unknown int([0,7]); intervals:[0,2]; enums:{0, 2}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2423:3-2423:25)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2423:3-2423:25)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2302:3-2302:44)
[Info][Unsound] Unknown address in {&(alloc@sid:671)[def_exc:Unknown int([0,7]); intervals:[0,2]; enums:{0, 2}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2302:3-2302:44)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2302:3-2302:44)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2293:3-2293:63)
[Info][Unsound] Unknown address in {&(alloc@sid:671)[def_exc:Unknown int([0,7]); intervals:[0,2]; enums:{0, 2}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2295:5-2295:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2295:5-2295:39)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2552:6-2552:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2297:3-2297:43)
[Info][Unsound] Unknown address in {&(alloc@sid:671)[def_exc:Unknown int([0,7]); intervals:[0,2]; enums:{0, 2}]} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2297:3-2297:43)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2297:3-2297:43)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2304:3-2304:72)
[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/chroot-incomplete-2.i:2693:5-2693: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/chroot-incomplete-2.i:2693:5-2693: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/chroot-incomplete-2.i:2693:5-2693:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-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/chroot-incomplete-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/chroot-incomplete-2.i:81:1-85:1)
[Warning][Deadcode] Function 'bb_show_usage' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2323:1-2326:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2405:1-2407:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2503:1-2512:1)
[Warning][Deadcode] Function 'geteuid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2537:1-2540:1)
[Warning][Deadcode] Function 'getgid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2541:1-2544:1)
[Warning][Deadcode] Function 'getegid' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2545:1-2548:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2581:1-2585:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2587:1-2597:1)
[Warning][Deadcode] Function 'getopt' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2598:1-2624:1)
[Warning][Deadcode] Function 'getopt_long' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2625:1-2631:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2632:1-2640:1)
[Warning][Deadcode] Function 'BB_EXECVP_or_die' has dead code:
  on line 2305 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2305-2305)
[Warning][Deadcode] Function '__main' has dead code:
  on line 2424 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2424-2424)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2336 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2336-2336)
  on line 2338 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2338-2338)
  on lines 2366..2369 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2366-2369)
  on line 2402 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2402-2402)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 205
  dead: 58 (49 in uncalled functions)
  total lines: 263
[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/chroot-incomplete-2.i:2673:6-2673: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673:25)
[Warning][Deadcode][CWE-571] condition 's < tmp' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2646:6-2646: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673:25)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2396:6-2396: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673:25)
[Warning][Deadcode][CWE-571] condition 's < tmp' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2646:6-2646:41)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2401:6-2401: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/chroot-incomplete-2.i:2688:8-2688:27)
[Warning][Deadcode][CWE-570] condition 'j < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2673:6-2673: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688:27)
[Warning][Deadcode][CWE-570] condition 'i < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2673:6-2673:25)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2440:10-2440: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688:27)
[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/chroot-incomplete-2.i:2653:9-2653:29)
[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/chroot-incomplete-2.i:2688:8-2688:27)
[Warning][Deadcode][CWE-570] condition 'j < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688:27)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2335:6-2335: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/chroot-incomplete-2.i:2688:8-2688:27)
[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/chroot-incomplete-2.i:2337:6-2337:38)
[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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688:27)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )pw->pw_shell == (unsigned long )((char *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2464:8-2464: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/chroot-incomplete-2.i:2688:8-2688:27)
[Warning][Deadcode][CWE-570] condition 'j < 10' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688: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/chroot-incomplete-2.i:2688:8-2688:27)
[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/chroot-incomplete-2.i:2364:6-2364:35)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
