CONTRACTS: drop (requires|ensures)_contract clauses

Removes support for contract clauses
- `__CPROVER_requires_contract(fptr, contract)`
- `__CPROVER_ensures_contract(fptr, contract)`
The clause format was cumbersome to use for pointers embedded
in other data structures, they will be replaced by a predicate.

Author: Remi Delmas

regression/contracts-dfcc/function-pointer-contracts-enforce/main.c

@@ -259,12 +259,6 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       static_cast<const exprt &>(static_cast<const irept &>(type));
     requires.push_back(to_unary_expr(as_expr).op());
   }
-  else if(type.id() == ID_C_spec_requires_contract)
-  {
-    const exprt &as_expr =
-      static_cast<const exprt &>(static_cast<const irept &>(type));
-    requires_contract.push_back(to_unary_expr(as_expr).op());
-  }
   else if(type.id() == ID_C_spec_assigns)
   {
     const exprt &as_expr =
@@ -287,12 +281,6 @@ void ansi_c_convert_typet::read_rec(const typet &type)
       static_cast<const exprt &>(static_cast<const irept &>(type));
     ensures.push_back(to_unary_expr(as_expr).op());
   }
-  else if(type.id() == ID_C_spec_ensures_contract)
-  {
-    const exprt &as_expr =
-      static_cast<const exprt &>(static_cast<const irept &>(type));
-    ensures_contract.push_back(to_unary_expr(as_expr).op());
-  }
   else
     other.push_back(type);
 }
@@ -342,10 +330,6 @@ void ansi_c_convert_typet::write(typet &type)
     if(!requires.empty())
       to_code_with_contract_type(type).requires() = std::move(requires);
 
-    if(!requires_contract.empty())
-      to_code_with_contract_type(type).requires_contract() =
-        std::move(requires_contract);
-
     if(!assigns.empty())
       to_code_with_contract_type(type).assigns() = std::move(assigns);
 
@@ -355,10 +339,6 @@ void ansi_c_convert_typet::write(typet &type)
     if(!ensures.empty())
       to_code_with_contract_type(type).ensures() = std::move(ensures);
 
-    if(!ensures_contract.empty())
-      to_code_with_contract_type(type).ensures_contract() =
-        std::move(ensures_contract);
-
     if(constructor || destructor)
     {
       if(constructor && destructor)

regression/contracts-dfcc/function-pointer-contracts-enforce/test-manual-swap.desc

@@ -47,8 +47,7 @@ class ansi_c_convert_typet:public messaget
   bool constructor, destructor;
 
   // contracts
-  exprt::operandst assigns, frees, ensures, requires, ensures_contract,
-    requires_contract;
+  exprt::operandst assigns, frees, ensures, requires;
 
   // storage spec
   c_storage_spect c_storage_spec;