Merge pull request #7289 from qinheping/crangler

Crangler: Add three tests for annotating function contracts

Author: tautschnig

regression/crangler/function-contract-01/main.c

@@ -0,0 +1,13 @@
+int f1(int *x1)
+{
+  return *x1 + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 1 && p < 10000);
+  f1(&p);
+
+  return 0;
+}

regression/crangler/function-contract-01/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.json
+
+\_\_CPROVER\_requires.*\_\_CPROVER\_requires.*\_\_CPROVER_ensures
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Annotate function contracts to function f1.

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

@@ -0,0 +1,15 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "f1": [
+        "requires *x1 > 1",
+        "requires *x1 < 10000",
+        "ensures __CPROVER_return_value == *x1 + 1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

regression/crangler/function-contract-02/main.c

@@ -0,0 +1,13 @@
+int foo(int *x)
+{
+  *x = *x + 0;
+  return *x + 5;
+}
+
+int main()
+{
+  int n = 4;
+  n = foo(&n);
+
+  return 0;
+}

regression/crangler/function-contract-02/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.json
+
+\_\_CPROVER\_assigns.*_\_CPROVER_ensures
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Annotate function contracts to function foo.

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

@@ -0,0 +1,14 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "foo": [
+        "assigns *x",
+        "ensures __CPROVER_return_value == *x + 5"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

regression/crangler/function-contract-03/main.c

@@ -0,0 +1,18 @@
+int f1(int *x1)
+{
+  return f2(x1) + 1;
+}
+
+int f2(int *x2)
+{
+  return *x2 + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 1 && p < 10000);
+  f1(&p);
+
+  return 0;
+}

regression/crangler/function-contract-03/test.desc

@@ -0,0 +1,11 @@
+CORE
+test.json
+
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+int f1\(int \*x1\)\n \_\_CPROVER\_requires\(\*x1\>1\&\&\*x1\<10000\) \_\_CPROVER\_ensures\(.*\=\=\*x1\+2\)
+int f2\(int \*x2\)\n \_\_CPROVER\_requires\(\*x2\>1\&\&\*x2\<10000\) \_\_CPROVER\_ensures\(.*\=\=\*x2\+1\)
+--
+--
+Annotate function contracts to functions f1 and f2.

regression/crangler/function-contract-03/test.json

@@ -0,0 +1,18 @@
+{
+  "sources": [
+    "main.c"
+  ],
+  "functions": [
+    {
+      "f1": [
+        "requires *x1 > 1 && *x1 < 10000",
+        "ensures __CPROVER_return_value == *x1 + 2"
+      ],
+      "f2": [
+        "requires *x2 > 1 && *x2 < 10000",
+        "ensures __CPROVER_return_value == *x2 + 1"
+      ]
+    }
+  ],
+  "output": "stdout"
+}