Merge pull request #7107 from Herbping/bugfixes/crangler

Fix wrong name ```__CPROVER_invariant``` of invariant clauses

Author: tautschnig

regression/crangler/loop-invariant-01/main.c

@@ -0,0 +1,27 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+
+  for(int i = 0; i < 2; i++)
+  {
+    arr[i] = 0;
+  }
+
+  int i = 0;
+  while(i < 2)
+  {
+    arr[i] = 0;
+    i++;
+  }
+
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/crangler/loop-invariant-01/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.json
+
+^\s+while\(i \< 2\) \_\_CPROVER\_loop\_invariant
+^EXIT=0$
+^SIGNAL=0$
+--
+^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER
+--
+Annotate loop invariant only to the for-loop.

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

@@ -0,0 +1,13 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "while 1 invariant 1==1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

regression/crangler/loop-invariant-02/main.c

@@ -0,0 +1,26 @@
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  for(int i = 0; i < 2; i++)
+  {
+    arr[i] = 0;
+  }
+
+  int i = 0;
+  while(i < 2)
+  {
+    arr[i] = 0;
+    i++;
+  }
+
+  return size < 10 ? 0 : arr[5];
+}
+
+int main()
+{
+  int arr[10];
+  int retval = foo(arr, 10);
+  __CPROVER_assert(retval == arr[5], "should succeed");
+  return 0;
+}

regression/crangler/loop-invariant-02/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.json
+
+^\s+for\(int i = 0; i \< 2; i\+\+\) \_\_CPROVER\_loop\_invariant
+^EXIT=0$
+^SIGNAL=0$
+--
+^\s+while\(i \< 2\) \_\_CPROVER
+--
+Annotate loop invariant only to the while-loop.

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

@@ -0,0 +1,13 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "for 1 invariant 1==1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

src/crangler/c_wrangler.cpp

@@ -456,8 +456,8 @@ static void mangle_function(
             auto t_end = match_bracket(t, '(', ')');
             for(; t != t_end; t++)
               out << t->text;
-            out << ' ' << CPROVER_PREFIX << "invariant(" << defines(invariant)
-                << ')';
+            out << ' ' << CPROVER_PREFIX << "loop_invariant("
+                << defines(invariant) << ')';
           }
         }
       }