CN: VIP: simple test that illustrates a problem

This is about the simplest case that exercises the loop invariant mechanism and the need for temporaries (such as the function parameter) to be implicitly added to the invariants.
rems-project · Aug 16, 2023 · f31ebe0 · f31ebe0
1 parent a30715d
commit f31ebe0
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/tests/cn/simple_loop.c b/tests/cn/simple_loop.c
@@ -0,0 +1,12 @@
+
+
+
+int
+simple_loop (int y)
+{
+  while (0)
+  {
+  }
+  return y;
+}
+