./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/rm-3.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/rm-3.i:2592:5-2598:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2643:3-2644:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2685:3-2696:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2718:3-2719:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2745:7-2751:22 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2735:3-2754:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2763:5-2769:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2776:5-2793:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2800:9-2803:9 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2795:5-2813:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2885:13-2888:13 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2973:25-2979:23 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2952:19-2981:19 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2821:3-2995:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3001:5-3020:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3030:5-3033:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3023:3-3057:18 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3059:3-3068:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3119:3-3120:5 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3191:5-3207:20 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3302:5-3337:45 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3347:3-3355:35 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3435:11-3449:11 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3519:5-3520:49 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3600:3-3601:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3602:3-3603:53 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:3-3655:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3661:3-3667:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3681:3-3682:34 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3696:5-3697:42 with factor 10
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3691:3-3698:3 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3700:3-3701:23 with factor 2
[Info] longjmp -> enabling longjmp analyses "activeLongjmp, activeSetjmp, taintPartialContexts, modifiedSinceSetjmp, poisonVariables, expsplit, vla"
[Info] Setting "ana.int.interval" to true
[Info] function remove_file is recursive, disable interval and interval_set contexts
[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/rm-3.i:3688:8-3688:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3688:8-3688:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3688:8-3688:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3689:8-3689:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3689:8-3689:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3689:8-3689:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3697:7-3697:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3697:7-3697:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3697:7-3697:42)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2718:6-2718:82)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2744:7-2744:68)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2744:7-2744:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2740:5-2740:47)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2744:7-2744:68)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2562:3-2562:49)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___5) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2946:21-2946:84)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___5) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2946:21-2946:84)
[Info][Imprecise] Invalidating expressions: (void *)(& tmp___5) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2946:21-2946:84)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3003:10-3003:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3005:12-3005:41)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3011:11-3011:89)
[Info][Unsound] Unknown value in {&(alloc@sid:2366(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3015:11-3015:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3003:10-3003:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3005:12-3005:41)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3011:11-3011:89)
[Info][Unsound] Unknown value in {&(alloc@sid:2366)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3015:11-3015:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3003:10-3003:40)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3005:12-3005:41)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3011:11-3011:89)
[Info][Unsound] Unknown value in {&(alloc@sid:2366)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3015:11-3015:22)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2366(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2366)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3638:10-3638:39)
[Info][Unsound] Unknown value in {&(alloc@sid:2366(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3638:10-3638:39)
[Info][Unsound] Unknown value in {&(alloc@sid:2366)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3638:10-3638:39)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3611:6-3611:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3619:7-3619:15)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3621:6-3621:68)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3626:7-3626:15)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3040:7-3040:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3040:7-3040:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3044:9-3044:76)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3119:6-3119:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3119:6-3119:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3119:6-3119:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3119:6-3119:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3119:6-3119:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3119:6-3119:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3123:3-3123:56)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3124:4-3124:36)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3049:11-3049:64)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3373:3-3373:92)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3379:3-3379:114)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3409:6-3409:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3412:5-3412:99)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3419:19-3419:73)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3419:19-3419:73)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3428:5-3428:35)
[Info][Unsound] Unknown address in {&e} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3428:5-3428:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3428:5-3428:35)
[Info][Imprecise] Invalidating expressions: (char ** __restrict  )end (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2626:3-2626:25)
[Info][Imprecise] Invalidating expressions: & v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2626:3-2626:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3450:12-3450:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3461:11-3461:141)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3468:3-3468:54)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3050:11-3050:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3054:13-3054:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2366(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2366)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3040:7-3040:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3040:7-3040:46)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3044:9-3044:76)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3049:11-3049:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3050:11-3050:91)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3054:13-3054:48)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3040:7-3040:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3040:7-3040:46)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3054:13-3054:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3049:11-3049:64)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3050:11-3050:91)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3044:9-3044:76)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2366(#0))} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Info][Unsound] Unknown value in {&(alloc@sid:2366)} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3025:5-3025:84)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3077:5-3077:25)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3305:7-3305:51)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2589:3-2589:31)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3109:7-3109:56)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3110:7-3110:34)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2600:3-2600:93)
[Info][Imprecise] Invalidating expressions: & slash (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2569:3-2569:26)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3306:10-3306:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3328:9-3328:61)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3130:3-3130:47)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3581:10-3581:25)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3560:3-3560:51)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3562:3-3562:49)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3563:3-3563:49)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3565:3-3565:50)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3566:3-3566:57)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3567:3-3567:55)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3568:3-3568:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3569:3-3569:58)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3570:3-3570:58)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3135:7-3135:45)
[Info][Imprecise] Invalidating expressions: & return_value_strerror$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2611:5-2611:48)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2616:3-2616:37)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2616:3-2616:37)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3140:7-3140:47)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3156:7-3156:48)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2555:3-2555:49)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3161:7-3161:44)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3182:7-3182:78)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3182:7-3182:78)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3182:7-3182:78)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3188:5-3188:21)
[Warning][Unknown] size of error: abstract type (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3501:10-3501:19)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3515:5-3515:41)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3517:5-3517:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3197:7-3197:52)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2658:9-2658:31)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2662:11-2662:121)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2662:11-2662:121)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2662:11-2662:121)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2664:11-2664:33)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2665:9-2665:103)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2665:9-2665:103)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2665:9-2665:103)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2668:16-2668:35)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2672:3-2672:60)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2672:3-2672:60)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2641:5-2641:14)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2642:3-2642:28)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2642:3-2642:28)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3108:7-3108:38)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3109:7-3109:56)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3110:7-3110:34)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3112:16-3112:25)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3115:10-3115:29)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2643:6-2643:63)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2643:6-2643:63)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2643:6-2643:63)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2646:3-2646:101)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2646:3-2646:101)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2646:3-2646:101)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2646:3-2646:101)
[Info][Unsound] Unknown value type given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3364:3-3364:38)
[Info][Unsound] Unknown address in {&string_ptr} has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3364:3-3364:38)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3364:3-3364:38)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3364:3-3364:38)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3653:7-3653:20)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:14-3654:19)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:6-3654:41)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:63-3654:76)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:14-3654:19)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:6-3654:41)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:63-3654:76)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:14-3654:19)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:14-3654:19)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:6-3654:41)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3654:63-3654:76)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3655:19-3655:45)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3655:19-3655:45)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3655:19-3655:45)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3655:73-3655:84)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3655:73-3655:84)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:22:136-22:139)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3656:7-3656:51)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3656:7-3656:51)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3658:12-3658:14)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3659:3-3659:36)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3659:3-3659:36)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3660:7-3660:12)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (lib/sv-comp/stub/src/sv-comp.c:20:141-20:144)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3663:6-3663:41)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3666:5-3666:8)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3663:6-3663:41)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3666:5-3666:8)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3663:6-3663:41)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3666:5-3666:8)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3668:3-3668:44)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:10:1-10:1)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3669:10-3669:11)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3367:5-3367:50)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2562:3-2562:49)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2636:1-2636:1)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3368:10-3368:20)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2647:10-2647:34)
[Warning][Unknown] lval (& d___0)->d_name points to a non-local variable. Invalid pointer dereference may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2673:10-2673:41)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3201:9-3201:64)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)new_path in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3204:9-3204:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3197:7-3197:52)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3201:9-3201:64)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)new_path in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3204:9-3204:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3197:7-3197:52)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3201:9-3201:64)
[Warning][Behavior > Undefined > InvalidMemoryDeallocation][CWE-590] Points-to set for pointer (void *)new_path in function free is top. Potentially invalid memory deallocation may occur (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3204:9-3204:31)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3212:7-3212:46)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3217:7-3217:72)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3217:7-3217:72)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3217:7-3217:72)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3224:5-3224:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3227:7-3227:47)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3236:5-3236:43)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3265:5-3265:60)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3265:5-3265:60)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3265:5-3265:60)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3272:3-3272:38)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3275:5-3275:45)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3305:7-3305:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3306:10-3306:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3328:9-3328:61)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3305:7-3305:51)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3306:10-3306:33)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3328:9-3328:61)
[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/rm-3.i:3701:5-3701: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/rm-3.i:3701:5-3701: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/rm-3.i:3701:5-3701:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.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/rm-3.i:1080:1-1084:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:1085:1-1089:1)
[Warning][Deadcode] Function 'fflush_all' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2675:1-2680:1)
[Warning][Deadcode] Function 'full_write' is uncalled: 10 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2681:1-2698:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3280:1-3282:1)
[Warning][Deadcode] Function 'safe_write' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3343:1-3357:1)
[Warning][Deadcode] Function 'xfunc_die' is uncalled: 5 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3382:1-3391:1)
[Warning][Deadcode] Function 'sleep' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3545:1-3549:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3595:1-3605:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3640:1-3648:1)
[Warning][Deadcode] Function 'write' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3671:1-3676:1)
[Warning][Deadcode] Function 'getopt32' has dead code:
  on lines 2761..2763 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2761-2763)
  on lines 2766..2768 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2766-2768)
  on lines 2771..2775 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2771-2775)
  on lines 2778..2779 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2778-2779)
  on line 2781 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2781-2781)
  on lines 2783..2791 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2783-2791)
  on lines 2793..2795 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2793-2795)
  on line 2797 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2797-2797)
  on lines 2799..2801 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2799-2801)
  on line 2803 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2803-2803)
  on lines 2805..2809 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2805-2809)
  on line 2814 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2814-2814)
  on line 2826 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2826-2826)
[Warning][Deadcode] Function 'xmalloc' has dead code:
  on lines 3398..3399 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3398-3399)
[Warning][Deadcode] Function 'xstrtou_range_sfx' has dead code:
  on line 3435 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3435-3435)
  on lines 3440..3442 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3440-3442)
  on line 3444 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3444-3444)
  on line 3446 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3446-3446)
  on line 3469 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3469-3469)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 540
  dead: 95 (48 in uncalled functions)
  total lines: 635
[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/rm-3.i:2952:25-2952:33)
[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/rm-3.i:3057:9-3057:18)
[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/rm-3.i:3661:9-3661:29)
[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/rm-3.i:3057:9-3057: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/rm-3.i:2952:25-2952:33)
[Warning][Deadcode][CWE-570] condition 'c >= 32' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2737:8-2737:15)
[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/rm-3.i:2821:9-2821:17)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )s == (unsigned long )((unsigned char const   *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2823:8-2823:52)
[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/rm-3.i:3681:6-3681: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/rm-3.i:2751:13-2751:22)
[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/rm-3.i:3681:6-3681: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/rm-3.i:2751:13-2751:22)
[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/rm-3.i:3681:6-3681: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/rm-3.i:2751:13-2751:22)
[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/rm-3.i:3681:6-3681:25)
[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/rm-3.i:3681:6-3681:25)
[Warning][Deadcode][CWE-570] condition 'c >= 32' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2737:8-2737:15)
[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/rm-3.i:3681:6-3681:25)
[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/rm-3.i:3396:6-3396: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/rm-3.i:3057:9-3057: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/rm-3.i:3681:6-3681: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/rm-3.i:2952:25-2952:33)
[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/rm-3.i:3681:6-3681: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/rm-3.i:2751:13-2751:22)
[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/rm-3.i:3681:6-3681: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/rm-3.i:2751:13-2751:22)
[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/rm-3.i:3681:6-3681: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/rm-3.i:2751:13-2751:22)
[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/rm-3.i:3681:6-3681:25)
[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/rm-3.i:3434:12-3434:62)
[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/rm-3.i:2751:13-2751: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/rm-3.i:2751:13-2751: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/rm-3.i:3696:8-3696: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/rm-3.i:2952:25-2952:33)
[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/rm-3.i:2751:13-2751: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696:27)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )applet_long_options == (unsigned long )((char const   *)((void *)0)))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2757:6-2757:59)
[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/rm-3.i:3696:8-3696: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/rm-3.i:2952:25-2952:33)
[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/rm-3.i:3696:8-3696:27)
[Warning][Deadcode][CWE-571] condition 'r >= lower' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:3454:14-3454: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:2821:9-2821:17)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )s == (unsigned long )((unsigned char const   *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2823:8-2823:52)
[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/rm-3.i:2952:25-2952:33)
[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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3207:11-3207:20)
[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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3207:11-3207:20)
[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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3207:11-3207:20)
[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/rm-3.i:3696:8-3696: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/rm-3.i:2952:25-2952:33)
[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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:2952:25-2952:33)
[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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:3696:8-3696: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/rm-3.i:2821:9-2821:17)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )s == (unsigned long )((unsigned char const   *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2823:8-2823:52)
[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/rm-3.i:2952:25-2952:33)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )f == (unsigned long )((char const   *)((void *)0)))' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/rm-3.i:2653:6-2653:41)
[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/rm-3.i:3654:6-3654:41)
[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/rm-3.i:3654:6-3654:41)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
