CONTRACTS: loop normal form tests for DFCC

Author: Remi Delmas

regression/contracts-dfcc/loop_contracts_reject_inner_loops_without_contracts/main.c

@@ -0,0 +1,17 @@
+int main()
+{
+  int i = 0, j = 0, k = 0;
+
+  while(j < 10)
+  {
+    while(k < 10)
+      __CPROVER_loop_invariant(1 == 1)
+      {
+        while(i < 10)
+        {
+          i++;
+        }
+      }
+    j++;
+  }
+}

regression/contracts-dfcc/loop_contracts_reject_inner_loops_without_contracts/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^file main.c line 10 function main: Found loop without contract nested in a loop with a contract.$
+^Please provide a contract or unwind this loop before applying loop contracts.$
+^EXIT=(6|10)$
+^SIGNAL=0$
+--
+--
+This test checks that our loop contract instrumentation verifies that loops
+nested in loops with contracts also have contracts.

regression/contracts-dfcc/loop_contracts_reject_loops_instruction_not_in_head_latch/main.c

@@ -0,0 +1,18 @@
+void main()
+{
+  int i = 0;
+
+HEAD:
+  if(i > 5)
+    goto EXIT;
+  goto BODY;
+
+LATCH:
+  goto HEAD;
+
+BODY:
+  i++;
+  goto LATCH;
+
+EXIT:;
+}

regression/contracts-dfcc/loop_contracts_reject_loops_instruction_not_in_head_latch/test.desc

@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^Found loop body instruction outside of the \[head, latch\] instruction span$
+^EXIT=(6|10)$
+^SIGNAL=0$
+--
+--
+This test checks that our loop contract instrumentation verifies that loops
+nested in loops with contracts also have contracts.

regression/contracts-dfcc/loop_contracts_reject_loops_overlapping_spans/main.c

@@ -0,0 +1,25 @@
+void main()
+{
+  int i = 0;
+  int j = 0;
+
+HEAD1:
+  if(i > 5)
+    goto EXIT1;
+  goto BODY1;
+
+EXIT1:;
+HEAD2:
+  if(j > 5)
+    goto EXIT2;
+  goto BODY2;
+
+BODY1:
+  i++;
+  goto HEAD1;
+
+BODY2:
+  j++;
+  goto HEAD2;
+EXIT2:;
+}

regression/contracts-dfcc/loop_contracts_reject_loops_overlapping_spans/test.desc

@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^Found loops with overlapping instruction spans$
+^EXIT=(6|10)$
+^SIGNAL=0$
+--
+--
+This test checks that our loop contract instrumentation verifies that loops
+nested in loops with contracts also have contracts.

regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+void main()
+{
+  int i = 0;
+  int j = 0;
+
+HEAD:
+  if(i > 5)
+    goto EXIT1;
+  i++;
+  goto HEAD;
+EXIT1:;
+  if(j > 5)
+    goto EXIT2;
+  j++;
+  goto HEAD;
+EXIT2:;
+}

regression/contracts-dfcc/loop_contracts_reject_loops_two_latches/test.desc

@@ -0,0 +1,10 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^Found loop with more than one latch instruction$
+^EXIT=(6|10)$
+^SIGNAL=0$
+--
+--
+This test checks that our loop contract instrumentation verifies that loops
+nested in loops with contracts also have contracts.