Add cram test for YAML witness unrolled loop invariant (issue #1225)

goblint · Feb 29, 2024 · 5d98e2e · 5d98e2e
1 parent 07430d2
commit 5d98e2e
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c
@@ -0,0 +1,6 @@
+int main() {
+  int i = 0;
+  while (i < 10)
+    i++;
+  return 0;
+}
diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
@@ -0,0 +1,6 @@
+  $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' 11-unrolled-loop-invariant.c
+  [Error] YAML witnesses are incompatible with syntactic loop unrolling (https://github.com/goblint/analyzer/pull/1370).
+  Fatal error: exception Failure("Option error")
+  [2]
+
+TODO: Fix loop unrolling with YAML witnesses: https://github.com/goblint/analyzer/pull/1370