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

@@ -258,12 +258,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 =
@@ -286,12 +280,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);
 }
@@ -341,10 +329,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);
 
@@ -354,10 +338,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)