Merge pull request #7348 from remi-delmas-3000/remove-requires-ensures-contract-clauses

CONTRACTS: Drop (requires|ensures)_contract clauses

Author: tautschnig

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)

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;