Merge pull request #7232 from qinheping/crangler-loop-invariant

Crangler: support full loop contracts

Author: qinheping

doc/man/crangler.1

@@ -15,8 +15,8 @@ The supported transformations are:
 .IP
 Add a contract (pre/post/assigns) to a named C function.
 .IP
-Add a loop invariant to a loop identified by the name of the function its in and
-a loop number.
+Add a loop contract to a loop identified by the name of the function containing
+the loop and a loop number.
 .IP
 Remove the
 .B static

regression/crangler/loop-invariant-01/main.c renamed to regression/crangler/loop-contract-01/main.c

@@ -1,7 +1,7 @@
 CORE
 test.json
 
-^\s+while\(i \< 2\) \_\_CPROVER\_loop\_invariant
+^\s+while\(i \< 2\) \_\_CPROVER\_assigns.*\_\_CPROVER\_loop\_invariant.*\_\_CPROVER_decreases
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/crangler/loop-invariant-01/test.desc renamed to regression/crangler/loop-contract-01/test.desc

@@ -0,0 +1,15 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "while 1 invariant i >= 0",
+        "while 1 assigns i, __CPROVER_POINTER_OBJECT(arr)",
+        "while 1 decreases 2-i"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

regression/crangler/loop-contract-01/test.json

@@ -1,7 +1,7 @@
 CORE
 test.json
 
-^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER\_loop\_invariant
+^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER\_assigns.*\_\_CPROVER\_loop\_invariant.*\_\_CPROVER_decreases
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/crangler/loop-invariant-02/main.c renamed to regression/crangler/loop-contract-02/main.c

@@ -0,0 +1,15 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "for 1 invariant i >= 0",
+        "for 1 assigns i, __CPROVER_POINTER_OBJECT(arr)",
+        "for 1 decreases 2-i"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

regression/crangler/loop-invariant-02/test.desc renamed to regression/crangler/loop-contract-02/test.desc

@@ -1,7 +1,7 @@
 CORE
 test.json
 
-^\s+while\(i \< 2\) \_\_CPROVER\_loop\_invariant
+^\s+while\(i \< 2\) \_\_CPROVER\_assigns.*\_\_CPROVER\_loop\_invariant.*\_\_CPROVER_decreases
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/crangler/loop-contract-02/test.json

@@ -0,0 +1,15 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "loop 2 assigns i, __CPROVER_POINTER_OBJECT(arr)",
+        "loop 2 invariant i>=0",
+        "loop 2 decreases 2-i"
+      ]
+    }
+  ],
+  "output": "stdout"
+}