Code contracts: match up introducing/removing parameter map modifications

regression/ansi-c/code_contracts1/main.c

@@ -0,0 +1,22 @@
+// clang-format off
+int foo()
+__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1})
+// clang-format on
+{
+  return 1;
+}
+
+// clang-format off
+int bar()
+__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1} &&
+                  __CPROVER_return_value == 1)
+// clang-format on
+{
+  return 1;
+}
+
+int main()
+{
+  foo();
+  bar();
+}

regression/ansi-c/code_contracts1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/contracts/function_check_02/main.c

@@ -1,8 +1,6 @@
 // function_check_02
 
 // This test checks the use of quantifiers in ensures clauses.
-// A known bug (resolved in PR #2278) causes the use of quantifiers
-// in ensures to fail.
 
 int initialize(int *arr)
   __CPROVER_ensures(

regression/contracts/function_check_02/test.desc

@@ -1,10 +1,7 @@
-KNOWNBUG
+CORE
 main.c
---check-code-contracts
+--apply-code-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
---
-Ensures statements currently do not allow quantified predicates unless the
-function has void return type.

src/ansi-c/c_typecheck_base.cpp

@@ -748,11 +748,15 @@ void c_typecheck_baset::typecheck_declaration(
       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)
+      {
+        DATA_INVARIANT(
+          parameter_map.empty(), "parameter map should be cleared");
         parameter_map[CPROVER_PREFIX "return_value"] = ret_type;
+      }
       typecheck_spec_expr(static_cast<codet &>(contract), ID_C_spec_ensures);
-      parameter_map.clear();
+      if(ret_type.id() != ID_empty)
+        parameter_map.clear();
 
       irept assigns_to_add = contract.find(ID_C_spec_assigns);
       if(assigns_to_add.is_not_nil())