diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 3887da8922c..54144dabe7a 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/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)
diff --git a/src/ansi-c/ansi_c_convert_type.h b/src/ansi-c/ansi_c_convert_type.h
index 4910d5b8b61..7185ed371b3 100644
--- a/src/ansi-c/ansi_c_convert_type.h
+++ b/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();
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
index 7ba3bb434de..fceaf5e6664 100644
--- a/src/ansi-c/ansi_c_declaration.cpp
+++ b/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;
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index c7a2174da61..9f4bf145c48 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/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");
+        }
+      }
     }
   }
 }
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
index 8a7bda5681b..47b6cd77b05 100644
--- a/src/ansi-c/c_typecheck_base.h
+++ b/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;
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 1b98556e3e0..5ad7179e346 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/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);
-  }
-}
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index bf2835f184f..f3e02a5a449 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/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)
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 6665ca6279f..38bcd911c3a 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -497,50 +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
-        {
-          init($$, ID_target_list);
-          mto($$, $1);
-        }
-        | target_list ',' target
-        {
-          $$=$1;
-          mto($$, $3);
-        }
-        ;
-
-target:
-          identifier
-        | '*' target
-        {
-          $$=$1;
-          set($$, ID_dereference);
-          mto($$, $2);
-        }
-        ;
-
 statement_expression: '(' compound_statement ')'
         { 
           $$=$1;
@@ -2901,21 +2857,8 @@ 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;
@@ -2923,7 +2866,7 @@ function_definition:
             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();
@@ -3065,6 +3008,7 @@ function_head:
         {
           init($$, ID_declaration);
           parser_stack($$).type().swap(parser_stack($1));
+          $2=merge($3, $2);
           PARSER.add_declarator(parser_stack($$), parser_stack($2));
           create_function_scope($$);
         }
@@ -3072,6 +3016,7 @@ function_head:
         {
           init($$, ID_declaration);
           parser_stack($$).type().swap(parser_stack($1));
+          $2=merge($3, $2);
           PARSER.add_declarator(parser_stack($$), parser_stack($2));
           create_function_scope($$);
         }
@@ -3285,6 +3230,43 @@ 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 '(' argument_expression_list ')'
+        {
+          $$=$1;
+          set($$, ID_C_spec_assigns);
+          parser_stack($3).id(ID_target_list);
+          mto($$, $3);
+        }
+        ;
+
+cprover_contract_sequence:
+          cprover_contract
+        | cprover_contract_sequence cprover_contract
+        {
+          $$=$1;
+          merge($$, $2);
+        }
+        ;
+
+cprover_contract_sequence_opt:
+          /* nothing */
+          { init($$); }
+        | cprover_contract_sequence
+        ;
+
 postfixing_abstract_declarator:
           parameter_postfixing_abstract_declarator
         /* The following two rules implement K&R headers! */
@@ -3323,11 +3305,12 @@ postfixing_abstract_declarator:
 parameter_postfixing_abstract_declarator:
           array_abstract_declarator
         | '(' ')'
+          cprover_contract_sequence_opt
         {
-          $$=$1;
-          set($$, ID_code);
-          stack_type($$).add(ID_parameters);
-          stack_type($$).subtype()=typet(ID_abstract);
+          set($1, ID_code);
+          stack_type($1).add(ID_parameters);
+          stack_type($1).subtype()=typet(ID_abstract);
+          $$ = merge($3, $1);
         }
         | '('
           {
@@ -3337,12 +3320,13 @@ parameter_postfixing_abstract_declarator:
               id2string(PARSER.current_scope().last_declarator)+"::");
           }
           parameter_type_list
-          ')' KnR_parameter_header_opt
+          ')'
+          KnR_parameter_header_opt
+          cprover_contract_sequence_opt
         {
-          $$=$1;
-          set($$, ID_code);
-          stack_type($$).subtype()=typet(ID_abstract);
-          stack_type($$).add(ID_parameters).get_sub().
+          set($1, ID_code);
+          stack_type($1).subtype()=typet(ID_abstract);
+          stack_type($1).add(ID_parameters).get_sub().
             swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes()));
           PARSER.pop_scope();
 
@@ -3351,6 +3335,8 @@ parameter_postfixing_abstract_declarator:
             adjust_KnR_parameters(parser_stack($$).add(ID_parameters), parser_stack($5));
             parser_stack($$).set(ID_C_KnR, true);
           }
+
+          $$ = merge($6, $1);
         }
         ;
 
diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc
index 494325c88c3..f5a823dbf94 100644
--- a/src/ansi-c/parser_static.inc
+++ b/src/ansi-c/parser_static.inc
@@ -341,12 +341,21 @@ static void create_function_scope(const YYSTYPE d)
                      id2string(function_name)+"::";
   PARSER.new_scope(prefix);
 
+  // We look at the last type in case of a merged declarator type.
+  typet *declarator_type = &declarator.type();
+  if(declarator_type->id()==ID_merged_type)
+  {
+    // we want the last one
+    auto &merged_type = to_merged_type(*declarator_type);
+    declarator_type = &merged_type.last_type();
+  }
+
   // The grammar doesn't actually enforce that a function type
   // is used to define a function body. We will complain in the
   // type checker about it.
-  if(declarator.type().id()==ID_code)
+  if(declarator_type->id()==ID_code)
   {
-    code_typet &code_type=to_code_type(declarator.type());
+    code_typet &code_type=to_code_type(*declarator_type);
 
     code_typet::parameterst &parameters=code_type.parameters();