allow contracts on function declarations

This changes the grammar of the C frontend to allow contracts on function
declarations.  This also removes the requirement that the contract clauses
appear in any particular order.

Author: kroening

src/ansi-c/ansi_c_convert_type.cpp

@@ -245,6 +245,24 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     UNREACHABLE;
   }
+  else if(type.id() == ID_C_spec_requires)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    requires = to_unary_expr(as_expr).op();
+  }
+  else if(type.id() == ID_C_spec_ensures)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    ensures = to_unary_expr(as_expr).op();
+  }
+  else if(type.id() == ID_C_spec_assigns)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    assigns = to_unary_expr(as_expr).op();
+  }
   else
     other.push_back(type);
 }
@@ -290,6 +308,16 @@ void ansi_c_convert_typet::write(typet &type)
 
     type.swap(other.front());
 
+    // the contract expressions are meant for function types only
+    if(requires.is_not_nil())
+      type.add(ID_C_spec_requires) = std::move(requires);
+
+    if(assigns.is_not_nil())
+      type.add(ID_C_spec_assigns) = std::move(assigns);
+
+    if(ensures.is_not_nil())
+      type.add(ID_C_spec_ensures) = std::move(ensures);
+
     if(constructor || destructor)
     {
       if(constructor && destructor)

src/ansi-c/ansi_c_convert_type.h

@@ -45,6 +45,9 @@ class ansi_c_convert_typet:public messaget
   exprt msc_based; // this is Visual Studio
   bool constructor, destructor;
 
+  // contracts
+  exprt requires, assigns, ensures;
+
   // storage spec
   c_storage_spect c_storage_spec;
 
@@ -82,6 +85,10 @@ class ansi_c_convert_typet:public messaget
     msc_based.make_nil();
     gcc_attribute_mode.make_nil();
 
+    requires.make_nil();
+    ensures.make_nil();
+    ensures.make_nil();
+
     packed=aligned=constructor=destructor=false;
 
     other.clear();

src/ansi-c/parser.y

@@ -497,27 +497,6 @@ loop_invariant_opt:
         { $$=$3; }
         ;
 
-requires_opt:
-        /* nothing */
-        { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
-        { $$=$3; }
-        ;
-
-ensures_opt:
-        /* nothing */
-        { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
-        { $$=$3; }
-        ;
-
-assigns_opt:
-        /* nothing */
-        { init($$); parser_stack($$).make_nil(); }
-        | TOK_CPROVER_ASSIGNS '(' target_list ')'
-        { $$=$3; }
-        ;
-
 target_list:
           target
         {
@@ -1008,6 +987,7 @@ post_declarator_attribute:
           parser_stack($$).set(ID_flavor, ID_gcc);
           parser_stack($$).operands().swap(parser_stack($4).operands());
         }
+        | cprover_contract
         | gcc_attribute_specifier
         ;
 
@@ -2901,29 +2881,16 @@ asm_definition:
 
 function_definition:
           function_head
-          assigns_opt
-          requires_opt
-          ensures_opt
           function_body
         {
-
-          // Capture assigns clause
-          if(parser_stack($2).is_not_nil())
-            parser_stack($1).add(ID_C_spec_assigns).swap(parser_stack($2));
-
-          // Capture code contract
-          if(parser_stack($3).is_not_nil())
-            parser_stack($1).add(ID_C_spec_requires).swap(parser_stack($3));
-          if(parser_stack($4).is_not_nil())
-            parser_stack($1).add(ID_C_spec_ensures).swap(parser_stack($4));
           // The head is a declaration with one declarator,
           // and the body becomes the 'value'.
           $$=$1;
           ansi_c_declarationt &ansi_c_declaration=
             to_ansi_c_declaration(parser_stack($$));
 
           assert(ansi_c_declaration.declarators().size()==1);
-          ansi_c_declaration.add_initializer(parser_stack($5));
+          ansi_c_declaration.add_initializer(parser_stack($2));
 
           // Kill the scope that 'function_head' creates.
           PARSER.pop_scope();
@@ -3285,6 +3252,27 @@ parameter_abstract_declarator:
         | parameter_postfix_abstract_declarator
         ;
 
+cprover_contract:
+          TOK_CPROVER_ENSURES '(' ACSL_binding_expression ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_ensures);
+          mto($$, $3);
+        }
+        | TOK_CPROVER_REQUIRES '(' ACSL_binding_expression ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_requires);
+          mto($$, $3);
+        }
+        | TOK_CPROVER_ASSIGNS '(' ACSL_binding_expression ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_assigns);
+          mto($$, $3);
+        }
+        ;
+
 postfixing_abstract_declarator:
           parameter_postfixing_abstract_declarator
         /* The following two rules implement K&R headers! */