./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/echo-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/echo-1.i:2283:3-2306:25 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2311:5-2321:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2430:5-2447:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2417:3-2451:18 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2456:3-2465:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2482:7-2508:22 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2473:3-2515:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2545:3-2556:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2563:3-2571:35 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2602:3-2602:26 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2611:3-2612:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2613:3-2614:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2665:3-2666:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2672:3-2678:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2692:3-2693:34 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2707:5-2708:42 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2702:3-2709:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2711:3-2712: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/echo-1.i:2699:8-2699:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2699:8-2699:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2699:8-2699:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2700:8-2700:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2700:8-2700:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2700:8-2700:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2708:7-2708:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2708:7-2708:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2708:7-2708:42)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2463:5-2463:83)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2463:5-2463:83)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2463:5-2463:83)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2467:3-2467:80)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2286:18-2286:109)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2286:18-2286:109)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2288:7-2288:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2293:9-2293:37)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2286:18-2286:109)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2286:18-2286:109)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2288:7-2288:45)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2286:18-2286:109)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2286:18-2286:109)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2288:7-2288:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2318:7-2318:17)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2318:7-2318:17)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2325:10-2325:17)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2480:7-2480:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2480:7-2480:27)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Info][Unsound] Unknown address in {&z} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2500:11-2500:83)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2480:7-2480:27)
[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/echo-1.i:2712:5-2712: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/echo-1.i:2712:5-2712: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/echo-1.i:2712:5-2712:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.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/echo-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/echo-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/echo-1.i:2243:1-2250:1)
[Warning][Deadcode] Function 'bb_perror_msg' is uncalled: 8 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2251:1-2266:1)
[Warning][Deadcode] Function 'bb_verror_msg' is uncalled: 48 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2327:1-2404:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2405:1-2407:1)
[Warning][Deadcode] Function 'fflush_all' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2535:1-2540:1)
[Warning][Deadcode] Function 'safe_write' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2559:1-2573:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2574:1-2583:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2595:1-2599:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2606:1-2616:1)
[Warning][Deadcode] Function 'getopt' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2617:1-2643:1)
[Warning][Deadcode] Function 'getopt_long' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2644:1-2650:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2651:1-2659:1)
[Warning][Deadcode] Function 'vasprintf' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2660:1-2681:1)
[Warning][Deadcode] Function 'write' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2682:1-2687:1)
[Warning][Deadcode] Function '__main' has dead code:
  on line 2496 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2496-2496)
  on lines 2530..2531 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2530-2531)
[Warning][Deadcode] Function 'full_write' has dead code:
  on lines 2547..2548 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2547-2548)
  on lines 2550..2552 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2550-2552)
  on lines 2554..2555 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2554-2555)
[Warning][Deadcode] Function 'xmalloc' has dead code:
  on lines 2590..2591 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2590-2591)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 142
  dead: 143 (131 in uncalled functions)
  total lines: 285
[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/echo-1.i:2707:8-2707: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/echo-1.i:2707:8-2707: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/echo-1.i:2692:6-2692: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/echo-1.i:2456:9-2456:17)
[Warning][Deadcode][CWE-570] condition 'r > 255u' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2300:8-2300:16)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2692:6-2692:25)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[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/echo-1.i:2430:11-2430:19)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2692:6-2692: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/echo-1.i:2707:8-2707: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/echo-1.i:2692:6-2692: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/echo-1.i:2707:8-2707: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/echo-1.i:2473:9-2473:17)
[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/echo-1.i:2508:13-2508:22)
[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/echo-1.i:2508:13-2508:22)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2707:8-2707:27)
[Warning][Deadcode][CWE-570] condition 'num_digits == 0u' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2294:12-2294:28)
[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/echo-1.i:2692:6-2692: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/echo-1.i:2451:9-2451:18)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2707:8-2707:27)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[Warning][Deadcode][CWE-570] condition 'num_digits < 3u' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2306:9-2306:25)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2430:11-2430:19)
[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/echo-1.i:2707:8-2707:27)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2311:11-2311:19)
[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/echo-1.i:2430:11-2430:19)
[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/echo-1.i:2508:13-2508:22)
[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/echo-1.i:2508:13-2508:22)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2508:13-2508:22)
[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/echo-1.i:2430:11-2430: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/echo-1.i:2707:8-2707: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/echo-1.i:2311:11-2311: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/echo-1.i:2707:8-2707: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/echo-1.i:2430:11-2430:19)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[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/echo-1.i:2588:6-2588:24)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2707:8-2707: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/echo-1.i:2311:11-2311:19)
[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/echo-1.i:2430:11-2430: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/echo-1.i:2707:8-2707:27)
[Warning][Deadcode][CWE-570] condition '! (*bb_errno == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2528:6-2528:23)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2508:13-2508:22)
[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/echo-1.i:2508:13-2508:22)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2430:11-2430:19)
[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/echo-1.i:2707:8-2707:27)
[Warning][Deadcode][CWE-570] condition '! (len == 0ul)' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2545:6-2545:58)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2707:8-2707: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/echo-1.i:2451:9-2451: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/echo-1.i:2473:9-2473:17)
[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/echo-1.i:2692:6-2692:25)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2451:9-2451:18)
[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/echo-1.i:2692:6-2692: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/echo-1.i:2707:8-2707: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/echo-1.i:2707:8-2707: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/echo-1.i:2430:11-2430: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/echo-1.i:2692:6-2692: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/echo-1.i:2508:13-2508:22)
[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/echo-1.i:2456:9-2456:17)
[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/echo-1.i:2707:8-2707:27)
[Warning][Deadcode][CWE-570] condition 'r > 255u' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2300:8-2300:16)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2692:6-2692:25)
[Warning][Deadcode][CWE-570] condition '208 + (int )((unsigned char )((int )*(arg + 1l))) < 8' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2495:16-2495:76)
[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/echo-1.i:2707:8-2707:27)
[Warning][Deadcode][CWE-571] condition 'num_digits < 3u' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/echo-1.i:2306:9-2306: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/echo-1.i:2707:8-2707: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/echo-1.i:2692:6-2692: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/echo-1.i:2456:9-2456:17)
[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/echo-1.i:2473:9-2473:17)
[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/echo-1.i:2707:8-2707: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/echo-1.i:2430:11-2430: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/echo-1.i:2707:8-2707: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/echo-1.i:2692:6-2692: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/echo-1.i:2508:13-2508:22)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
