./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/dirname-1.i


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:3-1237:38 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1247:3-1248:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1249:3-1250:53 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1301:3-1302:3 with factor 6
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1308:3-1314:3 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1328:3-1329:34 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1343:5-1344:42 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1338:3-1345:3 with factor 1
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1347:3-1348:23 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[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"
[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/dirname-1.i:1335:8-1335:45)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1335:8-1335:45)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1335:8-1335:45)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1336:8-1336:50)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1336:8-1336:50)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1336:8-1336:50)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1344:7-1344:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1344:7-1344:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1192:18-1192:120)
[Info][Unsound] Unknown address given as function argument (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1153:3-1153:61)
[Info][Imprecise] Invalidating expressions: (struct _IO_FILE *)((void *)0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1162:3-1162:63)
[Info][Imprecise] Invalidating expressions: & return_value_fflush$1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1162:3-1162:63)
[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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348: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/dirname-1.i:1348:5-1348:23)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:22:1-22:169)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:76:1-80:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:81:1-85:1)
[Warning][Deadcode] Function 'syslog' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1145:1-1147:1)
[Warning][Deadcode] Function 'getutent' is uncalled: 9 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1242:1-1252:1)
[Warning][Deadcode] Function 'getopt' is uncalled: 17 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1253:1-1279:1)
[Warning][Deadcode] Function 'getopt_long' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1280:1-1286:1)
[Warning][Deadcode] Function 'read' is uncalled: 6 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1287:1-1295:1)
[Warning][Deadcode] Function 'vasprintf' is uncalled: 15 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1296:1-1317:1)
[Warning][Deadcode] Function 'write' is uncalled: 3 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1318:1-1323:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 79
  dead: 55 (55 in uncalled functions)
  total lines: 134
[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/dirname-1.i:1343:8-1343: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/dirname-1.i:1328:6-1328: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/dirname-1.i:1343:8-1343: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/dirname-1.i:1328:6-1328:25)
[Warning][Deadcode][CWE-571] condition 'i < 42' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:6-1236: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/dirname-1.i:1343:8-1343:27)
[Warning][Deadcode][CWE-571] condition 'i < 42' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:6-1236: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/dirname-1.i:1343:8-1343:27)
[Warning][Deadcode][CWE-571] condition 'i < 42' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:6-1236: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/dirname-1.i:1343:8-1343:27)
[Warning][Deadcode][CWE-571] condition 'i < 42' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:6-1236: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/dirname-1.i:1343:8-1343:27)
[Warning][Deadcode][CWE-571] condition 'i < 42' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:6-1236: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/dirname-1.i:1343:8-1343:27)
[Warning][Deadcode][CWE-571] condition 'i < 42' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:6-1236: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/dirname-1.i:1343:8-1343:27)
[Warning][Deadcode][CWE-571] condition 'i < 42' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:6-1236:25)
[Warning][Deadcode][CWE-571] condition 'i < 42' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1236:6-1236: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/dirname-1.i:1343:8-1343: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/dirname-1.i:1343:8-1343: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/dirname-1.i:1343:8-1343: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/dirname-1.i:1343:8-1343:27)
[Warning][Deadcode][CWE-571] condition '(_Bool)1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1176:8-1176:16)
[Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1343:8-1343:27)
[Warning][Deadcode][CWE-571] condition '__s2_len < 4UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/busybox-1.22.0/dirname-1.i:1181:7-1181:107)
[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/dirname-1.i:1343:8-1343: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/dirname-1.i:1343:8-1343: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/dirname-1.i:1328:6-1328: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/dirname-1.i:1343:8-1343: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/dirname-1.i:1328:6-1328: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/dirname-1.i:1328:6-1328: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/dirname-1.i:1328:6-1328: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/dirname-1.i:1328:6-1328: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/dirname-1.i:1328:6-1328:25)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
