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

Crangler: Add space between crangler-defines tokens

Author: tautschnig

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

@@ -4,8 +4,8 @@ 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\)
+int f1\(int \*x1\)\n \_\_CPROVER\_requires\(\* \( signed long int \* \) x1 \> 1 \&\&.*\_\_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

@@ -5,7 +5,7 @@
   "functions": [
     {
       "f1": [
-        "requires *x1 > 1 && *x1 < 10000",
+        "requires *(signed long int*)x1 > 1 && *(signed long int*)x1 < 10000",
         "ensures __CPROVER_return_value == *x1 + 2"
       ],
       "f2": [

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

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

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

@@ -5,7 +5,7 @@
   "functions": [
     {
       "foo": [
-        "while 1 invariant i >= 0",
+        "while 1 invariant (unsigned long int)i >= 0",
         "while 1 assigns i, __CPROVER_POINTER_OBJECT(arr)",
         "while 1 decreases 2-i"
       ]

src/crangler/c_defines.cpp

@@ -61,7 +61,11 @@ std::string c_definest::operator()(const std::string &src) const
     }
     else
       out << t.text;
+    out << " ";
   }
 
-  return out.str();
+  auto result = out.str();
+  result.pop_back();
+
+  return result;
 }