Merge pull request #7557 from remi-delmas-3000/contrracts-do-while-syntax

CONTRACTS: place contracts after do for do-while loops

Author: remi-delmas-3000

regression/contracts/do_while_syntax_fail/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  int i = 0;
+  do
+  {
+    i++;
+  } while(i < 10)
+    // clang-format off
+   __CPROVER_assigns(i)
+   __CPROVER_loop_invariant(0 <= i && i <= 10)
+   __CPROVER_decreases(20 - i)
+    // clang-format on
+    ;
+}

regression/contracts/do_while_syntax_fail/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^PARSING ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+Checks that loop contracts for do-while loops cannot be attached after
+the `while` keyword.

regression/contracts/do_while_syntax_pass/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  int i = 0;
+  do
+    // clang-format off
+   __CPROVER_assigns(i)
+   __CPROVER_loop_invariant(0 <= i && i <= 10)
+   __CPROVER_decreases(20 - i)
+    // clang-format on
+    {
+      i++;
+    }
+  while(i < 10);
+}

regression/contracts/do_while_syntax_pass/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Checks that loop contracts for do-while loops can be attached after the `do`
+keyword.

regression/contracts/loop_contracts_do_while/main.c

@@ -5,9 +5,15 @@ int main()
   int x = 0;
 
   do
-  {
-    x++;
-  } while(x < 10) __CPROVER_loop_invariant(0 <= x && x <= 10);
+    // clang-format off
+   __CPROVER_assigns(x)
+   __CPROVER_loop_invariant(0 <= x && x <= 10)
+   __CPROVER_decreases(20 - x)
+    // clang-format on
+    {
+      x++;
+    }
+  while(x < 10);
 
   assert(x == 10);
 }

regression/contracts/loop_contracts_do_while/test.desc

@@ -7,3 +7,4 @@ main.c
 --
 --
 This test checks that loop contracts work correctly on do/while loops.
+Fails because contracts are not yet supported on do while loops.

src/ansi-c/parser.y

@@ -2493,23 +2493,25 @@ iteration_statement:
           if(!parser_stack($7).operands().empty())
             static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($7).operands());
         }
-        | TOK_DO statement TOK_WHILE '(' comma_expression ')'
+        | TOK_DO
           cprover_contract_assigns_opt
-          cprover_contract_loop_invariant_list_opt 
-          cprover_contract_decreases_opt ';'
+          cprover_contract_loop_invariant_list_opt
+          cprover_contract_decreases_opt
+          statement
+          TOK_WHILE '(' comma_expression ')' ';'
         {
           $$=$1;
           statement($$, ID_dowhile);
-          parser_stack($$).add_to_operands(std::move(parser_stack($5)), std::move(parser_stack($2)));
+          parser_stack($$).add_to_operands(std::move(parser_stack($8)), std::move(parser_stack($5)));
 
-          if(!parser_stack($7).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($7).operands());
+          if(!parser_stack($2).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_assigns)).operands().swap(parser_stack($2).operands());
 
-          if(!parser_stack($8).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($8).operands());
+          if(!parser_stack($3).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_loop_invariant)).operands().swap(parser_stack($3).operands());
 
-          if(!parser_stack($9).operands().empty())
-            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($9).operands());
+          if(!parser_stack($4).operands().empty())
+            static_cast<exprt &>(parser_stack($$).add(ID_C_spec_decreases)).operands().swap(parser_stack($4).operands());
         }
         | TOK_FOR
           {