Merge pull request #6986 from tautschnig/bugfixes/crangler-assigns-clauses

Crangler: support semicolon in post-declarator expressions

Author: tautschnig

regression/crangler/assigns-clause-syntax/main-contract-after-declaration.c

@@ -0,0 +1,28 @@
+int foo(int *arr, int size);
+
+int foo(int *arr, int size)
+  // clang-format off
+__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(
+  arr[0], arr[size-1];
+  size >= 10: arr[5];
+)
+__CPROVER_ensures(arr[0] == 0 && arr[size-1] == 0)
+__CPROVER_ensures(size >= 10 ==> arr[5] == __CPROVER_return_value)
+  // clang-format on
+  ;
+
+int foo(int *arr, int size)
+{
+  arr[0] = 0;
+  arr[size - 1] = 0;
+  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/assigns-clause-syntax/test.desc

@@ -0,0 +1,9 @@
+CORE
+test.json
+
+__CPROVER_assigns
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Make sure the semicolon in assigns clauses does not trip up parsing.

regression/crangler/assigns-clause-syntax/test.json

@@ -0,0 +1,6 @@
+{
+  "sources": [
+    "main-contract-after-declaration.c"
+  ],
+  "output": "stdout"
+}

src/crangler/mini_c_parser.cpp

@@ -282,12 +282,27 @@ mini_c_parsert::tokenst mini_c_parsert::parse_post_declarator()
   // 3) '=' (initializer)
 
   tokenst result;
+  std::size_t open_parentheses = 0;
 
   while(true)
   {
     if(eof())
       return result;
 
+    if(peek() == '(')
+    {
+      ++open_parentheses;
+      result.push_back(consume_token());
+      continue;
+    }
+    else if(open_parentheses > 0)
+    {
+      if(peek() == ')')
+        --open_parentheses;
+      result.push_back(consume_token());
+      continue;
+    }
+
     if(peek() == ';' || peek() == '{' || peek() == '=')
       return result;