allow contracts on function declarations

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_assigns)
+  {
+    const exprt &as_expr =
+      static_cast<const exprt &>(static_cast<const irept &>(type));
+    assigns = 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
     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();
+    assigns.make_nil();
+    ensures.make_nil();
+
     packed=aligned=constructor=destructor=false;
 
     other.clear();

src/ansi-c/ansi_c_declaration.cpp

@@ -140,8 +140,11 @@ void ansi_c_declarationt::to_symbol(
   symbol.is_weak=get_is_weak();
 
   // is it a function?
+  const typet &type = symbol.type.id() == ID_merged_type
+                        ? to_merged_type(symbol.type).last_type()
+                        : symbol.type;
 
-  if(symbol.type.id()==ID_code && !symbol.is_type)
+  if(type.id() == ID_code && !symbol.is_type)
   {
     symbol.is_static_lifetime=false;
     symbol.is_thread_local=false;

src/ansi-c/c_typecheck_base.cpp

@@ -644,19 +644,6 @@ void c_typecheck_baset::typecheck_declaration(
     // mark as 'already typechecked'
     already_typechecked_typet::make_already_typechecked(declaration.type());
 
-    irept contract;
-
-    {
-      exprt spec_assigns = declaration.spec_assigns();
-      contract.add(ID_C_spec_assigns).swap(spec_assigns);
-
-      exprt spec_ensures = declaration.spec_ensures();
-      contract.add(ID_C_spec_ensures).swap(spec_ensures);
-
-      exprt spec_requires = declaration.spec_requires();
-      contract.add(ID_C_spec_requires).swap(spec_requires);
-    }
-
     // Now do declarators, if any.
     for(auto &declarator : declaration.declarators())
     {
@@ -728,45 +715,45 @@ void c_typecheck_baset::typecheck_declaration(
       irep_idt identifier=symbol.name;
       declarator.set_name(identifier);
 
-      // If the declarator is for a function definition, typecheck it.
-      if(can_cast_type<code_typet>(declarator.type()))
-      {
-        typecheck_assigns(to_code_type(declarator.type()), contract);
-      }
-
       typecheck_symbol(symbol);
 
-      // add code contract (if any); we typecheck this after the
-      // function body done above, so as to have parameter symbols
-      // available
+      // check the contract, if any
       symbolt &new_symbol = symbol_table.get_writeable_ref(identifier);
+      if(new_symbol.type.id() == ID_code)
+      {
+        // We typecheck this after the
+        // function body done above, so as to have parameter symbols
+        // available
+        auto &code_type = to_code_with_contract_type(new_symbol.type);
+
+        if(as_const(code_type).requires().is_not_nil())
+        {
+          auto &requires = code_type.requires();
+          typecheck_expr(requires);
+          implicit_typecast_bool(requires);
+        }
+
+        if(as_const(code_type).assigns().is_not_nil())
+        {
+          for(auto &op : code_type.assigns().operands())
+            typecheck_expr(op);
+        }
 
-      typecheck_assigns_exprs(
-        static_cast<codet &>(contract), ID_C_spec_assigns);
-      typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_requires);
-
-      typet ret_type = void_type();
-      if(new_symbol.type.id()==ID_code)
-        ret_type=to_code_type(new_symbol.type).return_type();
-      assert(parameter_map.empty());
-      if(ret_type.id()!=ID_empty)
-        parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
-      typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
-      parameter_map.clear();
-
-      exprt assigns_to_add =
-        static_cast<const exprt &>(contract.find(ID_C_spec_assigns));
-      if(assigns_to_add.is_not_nil())
-        to_code_with_contract_type(new_symbol.type).assigns() = assigns_to_add;
-      exprt requires_to_add =
-        static_cast<const exprt &>(contract.find(ID_C_spec_requires));
-      if(requires_to_add.is_not_nil())
-        to_code_with_contract_type(new_symbol.type).requires() =
-          requires_to_add;
-      exprt ensures_to_add =
-        static_cast<const exprt &>(contract.find(ID_C_spec_ensures));
-      if(ensures_to_add.is_not_nil())
-        to_code_with_contract_type(new_symbol.type).ensures() = ensures_to_add;
+        if(as_const(code_type).ensures().is_not_nil())
+        {
+          const auto &return_type = code_type.return_type();
+
+          if(return_type.id() != ID_empty)
+            parameter_map[CPROVER_PREFIX "return_value"] = return_type;
+
+          auto &ensures = code_type.ensures();
+          typecheck_expr(ensures);
+          implicit_typecast_bool(ensures);
+
+          if(return_type.id() != ID_empty)
+            parameter_map.erase(CPROVER_PREFIX "return_value");
+        }
+      }
     }
   }
 }

src/ansi-c/c_typecheck_base.h

@@ -145,11 +145,6 @@ class c_typecheck_baset:
   virtual void typecheck_dowhile(code_dowhilet &code);
   virtual void typecheck_start_thread(codet &code);
   virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
-  virtual void
-  typecheck_assigns(const code_typet &function_declarator, const irept &spec);
-  virtual void
-  typecheck_assigns(const ansi_c_declaratort &declarator, const exprt &assigns);
-  virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec);
 
   bool break_is_allowed;
   bool continue_is_allowed;

src/ansi-c/c_typecheck_code.cpp

@@ -819,65 +819,3 @@ void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec)
     implicit_typecast_bool(constraint);
   }
 }
-
-void c_typecheck_baset::typecheck_assigns(
-  const code_typet &function_declarator,
-  const irept &contract)
-{
-  exprt assigns = static_cast<const exprt &>(contract.find(ID_C_spec_assigns));
-
-  // Make sure there is an assigns clause to check
-  if(assigns.is_not_nil())
-  {
-    for(const auto &curr_param : function_declarator.parameters())
-    {
-      if(curr_param.id() == ID_declaration)
-      {
-        const ansi_c_declarationt &param_declaration =
-          to_ansi_c_declaration(curr_param);
-
-        for(const auto &decl : param_declaration.declarators())
-        {
-          typecheck_assigns(decl, assigns);
-        }
-      }
-    }
-  }
-}
-
-void c_typecheck_baset::typecheck_assigns(
-  const ansi_c_declaratort &declarator,
-  const exprt &assigns)
-{
-  for(exprt curr_op : assigns.operands())
-  {
-    if(curr_op.id() != ID_symbol)
-    {
-      continue;
-    }
-    const symbol_exprt &symbol_op = to_symbol_expr(curr_op);
-
-    if(symbol_op.get(ID_C_base_name) == declarator.get_base_name())
-    {
-      error().source_location = declarator.source_location();
-      error() << "Formal parameter " << declarator.get_name() << " without "
-              << "dereference appears in ASSIGNS clause. Assigning this "
-              << "parameter will never affect the state of the calling context."
-              << " Did you mean to write *" << declarator.get_name() << "?"
-              << eom;
-      throw 0;
-    }
-  }
-}
-
-void c_typecheck_baset::typecheck_assigns_exprs(
-  codet &code,
-  const irep_idt &spec)
-{
-  if(code.find(spec).is_not_nil())
-  {
-    exprt &constraint = static_cast<exprt &>(code.add(spec));
-
-    typecheck_expr(constraint);
-  }
-}

src/ansi-c/expr2c.cpp

@@ -550,6 +550,25 @@ std::string expr2ct::convert_rec(
         dest.resize(dest.size()-1);
     }
 
+    // contract, if any
+    if(to_code_with_contract_type(src).requires().is_not_nil())
+    {
+      dest += " [[requires " +
+              convert(to_code_with_contract_type(src).requires()) + "]]";
+    }
+
+    if(!to_code_with_contract_type(src).assigns().operands().empty())
+    {
+      dest += " [[assigns " +
+              convert(to_code_with_contract_type(src).assigns()) + "]]";
+    }
+
+    if(to_code_with_contract_type(src).ensures().is_not_nil())
+    {
+      dest += " [[ensures " +
+              convert(to_code_with_contract_type(src).ensures()) + "]]";
+    }
+
     return dest;
   }
   else if(src.id()==ID_vector)