./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/sleep-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/sleep-2.i:2478:3-2489:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2496:3-2504:35 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2529:3-2573:43 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2584:3-2590:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2647:11-2661:11 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2714:3-2715:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2716:3-2717:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2768:3-2769:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2775:3-2781:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2795:3-2796:34 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2810:5-2811:42 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2805:3-2812:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2814:3-2815: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/sleep-2.i:2802:8-2802:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2802:8-2802:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2802:8-2802:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2803:8-2803:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2803:8-2803:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2803:8-2803:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2811:7-2811:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2811:7-2811:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2811:7-2811:42)
[Info][Imprecise] Invalidating expressions: & return_value___builtin_strchr$14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2534:5-2534:53)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2540:7-2540:39)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2540:7-2540:39)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )(& pp) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2545:7-2545:25)
[Info][Imprecise] Invalidating expressions: & d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2545:7-2545:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2550:9-2550:114)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2561:7-2561:54)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2596:3-2596:51)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2602:3-2602:162)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2631:19-2631:73)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )(& e) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2640:5-2640:33)
[Info][Imprecise] Invalidating expressions: & r (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2640:5-2640:33)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2658:15-2658:61)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2658:15-2658:61)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2658:15-2658:61)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2662:12-2662:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2673:11-2673:141)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2382:3-2382:49)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2402:3-2402:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2402:3-2402:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2402:3-2402:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2407:3-2407:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2407:3-2407: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/sleep-2.i:2422:3-2422:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2422:3-2422:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2422:3-2422:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2437:5-2437:101)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2438:5-2438:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2440:5-2440:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2441:5-2441:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2457:5-2457:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2471:3-2471:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2471:3-2471:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2462:5-2462:62)
[Info][Unsound] Unknown value in {&(alloc@sid:43)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2462:5-2462:62)
[Info][Unsound] Unknown value in {&(alloc@sid:43)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2480:5-2480:32)
[Info][Unsound] Unknown value in {&(alloc@sid:43)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2498:5-2498:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2478:6-2478:58)
[Info][Unsound] Unknown value in {&(alloc@sid:43)[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/sleep-2.i:2480:5-2480:32)
[Info][Unsound] Unknown value in {&(alloc@sid:43)[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/sleep-2.i:2498:5-2498:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2487:5-2487:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2478:6-2478:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2487:5-2487:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2478:6-2478:58)
[Info][Unsound] Unknown value in {&(alloc@sid:43)[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/sleep-2.i:2480:5-2480:32)
[Info][Unsound] Unknown value in {&(alloc@sid:43)[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/sleep-2.i:2498:5-2498:28)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2680:3-2680:54)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2562:7-2562:67)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2562:7-2562:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2568:7-2568:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2621:6-2621:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2624:5-2624:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2631:19-2631:73)
[Info][Unsound] Unknown value in {&(alloc@sid:43)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2498:5-2498:28)
[Info][Unsound] Unknown value in {&(alloc@sid:43)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2498:5-2498:28)
[Info][Unsound] Unknown value in {&(alloc@sid:43)[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/sleep-2.i:2498:5-2498:28)
[Info][Unsound] Unknown value in {&(alloc@sid:43)[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/sleep-2.i:2498:5-2498:28)
[Info][Unsound] Unknown value in {&(alloc@sid:43)[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/sleep-2.i:2498:5-2498:28)
[Info][Unsound] Unknown value in {&(alloc@sid:43)[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/sleep-2.i:2498:5-2498:28)
[Info][Imprecise] Invalidating expressions: & return_value___builtin_strchr$14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2534:5-2534:53)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2540:7-2540:39)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2540:7-2540:39)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )(& pp) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2545:7-2545:25)
[Info][Imprecise] Invalidating expressions: & d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2545:7-2545:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2550:9-2550:114)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2561:7-2561:54)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2562:7-2562:67)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2562:7-2562:67)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2568:7-2568:54)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2569:7-2569:63)
[Info][Imprecise] Invalidating expressions: & return_value___builtin_strchr$14 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2534:5-2534:53)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2568:7-2568:54)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2569:7-2569:63)
[Info][Imprecise] Invalidating expressions: & tmp (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2540:7-2540:39)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2540:7-2540:39)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )(& pp) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2545:7-2545:25)
[Info][Imprecise] Invalidating expressions: & d (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2545:7-2545:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2550:9-2550:114)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2561:7-2561:54)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2562:7-2562:67)
[Warning][Float][CWE-189][CWE-739] Second operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2562:7-2562:67)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2574:3-2574:210)
[Warning][Integer > Overflow] DefExc: Value was outside of range, indicating overflow, but 'sem.int.signed_overflow' is 'assume_none' -> Returned Bot (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2574:3-2574:210)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2576:6-2576:26)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2576:6-2576:26)
[Warning][Float][CWE-189][CWE-739] First operand of comparison could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2578:8-2578:36)
[Warning][Float][CWE-1077] Equality/Inequality between `double` is dangerous! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2578:8-2578:36)
[Warning][Float][CWE-189][CWE-739] First operand of arithmetic operation could be +/-infinity or Nan (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2581:7-2581:90)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2696:17-2696:72)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2697:17-2697:75)
[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/sleep-2.i:2815:5-2815: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/sleep-2.i:2815:5-2815: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/sleep-2.i:2815:5-2815:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-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/sleep-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/sleep-2.i:81:1-85:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2507:1-2509:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2605:1-2614:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2703:1-2707:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2709:1-2719:1)
[Warning][Deadcode] Function 'getopt' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2720:1-2746:1)
[Warning][Deadcode] Function 'getopt_long' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2747:1-2753:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2754:1-2762:1)
[Warning][Deadcode] Function '__main' has dead code:
  on line 2547 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2547-2547)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2399-2399)
  on line 2401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2401-2401)
  on lines 2412..2413 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2412-2413)
  on lines 2429..2432 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2429-2432)
  on line 2444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2444-2444)
  on lines 2446..2451 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2446-2451)
  on lines 2453..2454 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2453-2454)
  on line 2465 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2465-2465)
[Warning][Deadcode] Function 'xstrtoull_range_sfx' has dead code:
  on line 2681 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2681-2681)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 200
  dead: 65 (45 in uncalled functions)
  total lines: 265
[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/sleep-2.i:2810:8-2810:27)
[Warning][Deadcode][CWE-570] condition '! (*bb_errno == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2546:10-2546:27)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2464:6-2464: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2584:9-2584: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/sleep-2.i:2810:8-2810:27)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2483:10-2483:24)
[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/sleep-2.i:2584:9-2584: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/sleep-2.i:2810:8-2810:27)
[Warning][Deadcode][CWE-571] condition 'r >= lower' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2666:14-2666:24)
[Warning][Deadcode][CWE-571] condition 'upper >= r' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2668:16-2668:26)
[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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2584:9-2584: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810:27)
[Warning][Deadcode][CWE-570] condition '! (*bb_errno == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2546:10-2546: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2768:6-2768: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/sleep-2.i:2810:8-2810:27)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2398:6-2398:30)
[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/sleep-2.i:2400:6-2400: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2768:6-2768:41)
[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/sleep-2.i:2410:6-2410:46)
[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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795:25)
[Warning][Deadcode][CWE-570] condition '! (*bb_errno == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2546:10-2546: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795:25)
[Warning][Deadcode][CWE-571] condition '*bb_errno == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2643:10-2643:24)
[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/sleep-2.i:2427:6-2427:35)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )suffixes == (unsigned long )((struct suffix_mult *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2646:12-2646:62)
[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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2810:8-2810:27)
[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/sleep-2.i:2442:8-2442: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2795:6-2795: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2810:8-2810: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/sleep-2.i:2775:9-2775:29)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2574:3-2574:210)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/sleep-2.i:2459:6-2459:39)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
