./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/usleep-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/usleep-2.i:2358:3-2369:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2376:3-2384:35 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2453:11-2467:11 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2507:3-2508:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2509:3-2510:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2561:3-2562:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2568:3-2574:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2588:3-2589:34 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2603:5-2604:42 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2598:3-2605:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2607:3-2608: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/usleep-2.i:2595:8-2595:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2595:8-2595:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2595:8-2595:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2596:8-2596:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2596:8-2596:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2596:8-2596:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2604:7-2604:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2604:7-2604:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2604:7-2604:42)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2395:3-2395:55)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2402:3-2402:80)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2408:3-2408:128)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2427:6-2427:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2430:5-2430:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2437:19-2437:73)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2437:19-2437:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2446:5-2446:35)
[Info][Unsound] Unknown address in {&e} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2446:5-2446:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2446:5-2446:35)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2262:3-2262:25)
[Info][Imprecise] Invalidating expressions: & v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2262:3-2262:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2468:12-2468:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2486:3-2486:54)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2251:3-2251:49)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2282:3-2282:29)
[Info][Unsound] Unknown address in {&msg} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2282:3-2282:29)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2282:3-2282:29)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2287:3-2287:74)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2287:3-2287: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/usleep-2.i:2302:3-2302:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2302:3-2302:116)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2302:3-2302:116)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2302:3-2302:116)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2318:5-2318:29)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2320:5-2320:54)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2321:5-2321:54)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2337:5-2337:29)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2351:3-2351:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2351:3-2351:63)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2342:5-2342:62)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2342:5-2342:62)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2360:5-2360:32)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2378:5-2378:28)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2378:5-2378:28)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2378:5-2378:28)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2358:6-2358:58)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))[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/usleep-2.i:2360:5-2360:32)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))[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/usleep-2.i:2378:5-2378:28)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))[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/usleep-2.i:2378:5-2378:28)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))[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/usleep-2.i:2378:5-2378:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2367:5-2367:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2358:6-2358:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2367:5-2367:23)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2358:6-2358:58)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))[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/usleep-2.i:2360:5-2360:32)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))[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/usleep-2.i:2378:5-2378:28)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))[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/usleep-2.i:2378:5-2378:28)
[Info][Unsound] Unknown value in {&(alloc@sid:49(#0))[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/usleep-2.i:2378:5-2378:28)
[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/usleep-2.i:2608:5-2608: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/usleep-2.i:2608:5-2608: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/usleep-2.i:2608:5-2608:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-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/usleep-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/usleep-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/usleep-2.i:2255:1-2258:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2387:1-2389:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2411:1-2420:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2488:1-2492:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2502:1-2512:1)
[Warning][Deadcode] Function 'getopt' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2513:1-2539:1)
[Warning][Deadcode] Function 'getopt_long' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2540:1-2546:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2547:1-2555:1)
[Warning][Deadcode] Function 'bb_verror_msg' has dead code:
  on line 2279 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2279-2279)
  on line 2281 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2281-2281)
  on lines 2292..2293 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2292-2293)
  on lines 2309..2312 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2309-2312)
  on line 2324 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2324-2324)
  on lines 2326..2331 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2326-2331)
  on lines 2333..2334 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2333-2334)
  on line 2345 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2345-2345)
[Warning][Deadcode] Function 'xstrtou_range_sfx' has dead code:
  on line 2453 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2453-2453)
  on lines 2458..2460 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2458-2460)
  on line 2462 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2462-2462)
  on line 2464 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2464-2464)
  on line 2479 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2479-2479)
  on line 2487 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2487-2487)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 154
  dead: 72 (46 in uncalled functions)
  total lines: 226
[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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588:25)
[Warning][Deadcode][CWE-571] condition '! ((1 & (int )logmode) == 0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2339:6-2339: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588:25)
[Warning][Deadcode][CWE-570] condition '! ((2 & (int )logmode) == 0)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2344:6-2344:39)
[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/usleep-2.i:2561:6-2561: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588:25)
[Warning][Deadcode][CWE-570] condition '! (total == 0l)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2363:10-2363: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2568:9-2568: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603:27)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )suffixes == (unsigned long )((struct suffix_mult *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2452:12-2452: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603:27)
[Warning][Deadcode][CWE-570] condition '(int )logmode == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2278:6-2278: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2280:6-2280: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2290:6-2290:46)
[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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603:27)
[Warning][Deadcode][CWE-571] condition 'r >= lower' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2472:14-2472: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/usleep-2.i:2603:8-2603:27)
[Warning][Deadcode][CWE-571] condition 'upper >= r' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2474:16-2474:26)
[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/usleep-2.i:2307:6-2307:35)
[Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/usleep-2.i:2588:6-2588: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2322:8-2322: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2603:8-2603: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/usleep-2.i:2588:6-2588: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/usleep-2.i:2561:6-2561:41)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
