./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/dll-01-1.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpachecker.2023-11-29_00-03-15.files/SV-COMP24_unreach-call/dll-01-1.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-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/forester-heap/dll-01-1.i:1006:2-1006:69 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1006:239-1006:342 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1018:3-1018:69 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1019:3-1019:69 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1019:235-1019:336 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1026:2-1026:68 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1038:4-1038:72 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1039:4-1039:79 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1040:4-1040:78 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1043:3-1043:60 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1055:4-1055:70 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1056:4-1056:77 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1057:4-1057:76 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] 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 ! call(reach_error())) )
[Info][Witness] cannot unassume entry of type violation_sequence
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1015:3-1015:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1017:3-1017:25)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1019:170-1019:199)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1019:201-1019:231)
[Warning][Deadcode] Function 'main' has dead code:
  on line 1037 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1037-1037)
  on line 1041 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1041-1041)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 41
  dead: 2
  total lines: 43
[Warning][Deadcode][CWE-571] condition 'len == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1034:8-1034:16)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )((void *)0) != (unsigned long )inner)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1038:13-1038:35)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1038:70-1038:72)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1019:334-1019:336)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )((void *)0) != (unsigned long )end)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1026:11-1026:31)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )((void *)0) != (unsigned long )end)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1055:13-1055:33)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1026:66-1026:68)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1055:68-1055:70)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )end != (unsigned long )((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1019:12-1019:32)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1019:67-1019:69)
[Warning][Deadcode][CWE-570] condition '! (len <= 1)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1043:12-1043:23)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1043:58-1043:60)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1006:340-1006:342)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:992:73-992:74)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )list != (unsigned long )((void *)0))' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1006:11-1006:32)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1006:67-1006:69)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1018:67-1018:69)
[Warning][Deadcode][CWE-571] condition '! ((unsigned long )((void *)0) != (unsigned long )inner->next)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1040:13-1040:41)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )((void *)0) == (unsigned long )end->next)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1057:13-1057:39)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1057:74-1057:76)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )((void *)0) == (unsigned long )inner->inner)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1039:13-1039:42)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1039:77-1039:79)
[Warning][Deadcode][CWE-570] condition '! ((unsigned long )((void *)0) == (unsigned long )end->inner)' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1056:13-1056:40)
[Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/forester-heap/dll-01-1.i:1056:75-1056:77)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 0
SV-COMP result: unknown
