Replace requires with c_requires

Fixes #7675

Author: TGWDB

src/ansi-c/ansi_c_convert_type.cpp

@@ -250,7 +250,7 @@ void ansi_c_convert_typet::read_rec(const typet &type)
   {
     const exprt &as_expr =
       static_cast<const exprt &>(static_cast<const irept &>(type));
-    requires.push_back(to_unary_expr(as_expr).op());
+    c_requires.push_back(to_unary_expr(as_expr).op());
   }
   else if(type.id() == ID_C_spec_assigns)
   {
@@ -322,8 +322,8 @@ void ansi_c_convert_typet::write(typet &type)
     type.swap(other.front());
 
     // the contract expressions are meant for function types only
-    if(!requires.empty())
-      to_code_with_contract_type(type).requires() = std::move(requires);
+    if(!c_requires.empty())
+      to_code_with_contract_type(type).c_requires() = std::move(c_requires);
 
     if(!assigns.empty())
       to_code_with_contract_type(type).assigns() = std::move(assigns);

src/ansi-c/ansi_c_convert_type.h

@@ -48,7 +48,7 @@ class ansi_c_convert_typet
   bool constructor, destructor;
 
   // contracts
-  exprt::operandst assigns, frees, ensures, requires;
+  exprt::operandst assigns, frees, ensures, c_requires;
 
   // storage spec
   c_storage_spect c_storage_spec;

src/ansi-c/c_typecheck_base.cpp

@@ -905,16 +905,16 @@ void c_typecheck_baset::typecheck_declaration(
             parameter_identifier, p.type());
         }
 
-        for(auto &requires : code_type.requires())
+        for(auto &c_requires : code_type.c_requires())
         {
-          typecheck_expr(requires);
-          implicit_typecast_bool(requires);
+          typecheck_expr(c_requires);
+          implicit_typecast_bool(c_requires);
           std::string clause_type = "preconditions";
-          check_history_expr_return_value(requires, clause_type);
-          check_was_freed(requires, clause_type);
-          lambda_exprt lambda{temporary_parameter_symbols, requires};
-          lambda.add_source_location() = requires.source_location();
-          requires.swap(lambda);
+          check_history_expr_return_value(c_requires, clause_type);
+          check_was_freed(c_requires, clause_type);
+          lambda_exprt lambda{temporary_parameter_symbols, c_requires};
+          lambda.add_source_location() = c_requires.source_location();
+          c_requires.swap(lambda);
         }
 
         typecheck_spec_assigns(code_type.assigns());

src/cprover/instrument_contracts.cpp

@@ -286,11 +286,11 @@ void instrument_contract_checks(
   goto_programt add_at_beginning;
 
   // precondition?
-  if(!contract.requires().empty())
+  if(!contract.c_requires().empty())
   {
     // stick these in as assumptions, preserving the ordering
     goto_programt dest;
-    for(auto &assumption : contract.requires())
+    for(auto &assumption : contract.c_requires())
     {
       exprt assumption_instance = instantiate_contract_lambda(assumption);
       auto fixed_assumption = add_function(f.first, assumption_instance);
@@ -338,7 +338,7 @@ void instrument_contract_checks(
 
   // do 'old' in the body
   if(
-    !contract.assigns().empty() || !contract.requires().empty() ||
+    !contract.assigns().empty() || !contract.c_requires().empty() ||
     !contract.ensures().empty())
   {
     for(auto &instruction : body.instructions)
@@ -359,7 +359,7 @@ void instrument_contract_checks(
 
   // assigns?
   if(
-    !contract.assigns().empty() || !contract.requires().empty() ||
+    !contract.assigns().empty() || !contract.c_requires().empty() ||
     !contract.ensures().empty())
   {
     for(auto it = body.instructions.begin(); it != body.instructions.end();
@@ -449,7 +449,7 @@ void replace_function_calls_by_contracts(
         goto_programt dest;
 
         // assert the preconditions
-        for(auto &precondition : contract.requires())
+        for(auto &precondition : contract.c_requires())
         {
           auto instantiated_precondition =
             instantiate_contract_lambda(precondition);

src/goto-instrument/contracts/contracts.cpp

@@ -673,7 +673,7 @@ void code_contractst::apply_function_contract(
   is_fresh.add_memory_map_decl(new_program);
 
   // Generate: assert(requires)
-  for(const auto &clause : type.requires())
+  for(const auto &clause : type.c_requires())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
@@ -689,8 +689,8 @@ void code_contractst::apply_function_contract(
       converter,
       instantiated_clause,
       mode,
-      [&is_fresh](goto_programt &requires) {
-        is_fresh.update_requires(requires);
+      [&is_fresh](goto_programt &c_requires) {
+        is_fresh.update_requires(c_requires);
       },
       new_program,
       _location);
@@ -1307,7 +1307,7 @@ void code_contractst::add_contract_check(
   visitor.add_memory_map_decl(check);
 
   // Generate: assume(requires)
-  for(const auto &clause : code_type.requires())
+  for(const auto &clause : code_type.c_requires())
   {
     auto instantiated_clause =
       to_lambda_expr(clause).application(instantiation_values);
@@ -1326,8 +1326,8 @@ void code_contractst::add_contract_check(
       converter,
       instantiated_clause,
       function_symbol.mode,
-      [&visitor](goto_programt &requires) {
-        visitor.update_requires(requires);
+      [&visitor](goto_programt &c_requires) {
+        visitor.update_requires(c_requires);
       },
       check,
       _location);

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -577,7 +577,7 @@ void dfcc_wrapper_programt::encode_requires_clauses()
   goto_programt requires_program;
 
   // translate each requires clause
-  for(const auto &r : contract_code_type.requires())
+  for(const auto &r : contract_code_type.c_requires())
   {
     exprt requires = to_lambda_expr(r).application(contract_lambda_parameters);
     requires.add_source_location() = r.source_location();

src/goto-programs/goto_functions.h

@@ -67,7 +67,10 @@ class goto_functionst
   }
 
   /// Remove function from the function map
-  void unload(const irep_idt &name) { function_map.erase(name); }
+  void unload(const irep_idt &name)
+  {
+    function_map.erase(name);
+  }
 
   void clear()
   {

src/goto-programs/goto_model.h

@@ -66,7 +66,10 @@ class goto_modelt : public abstract_goto_modelt
     return *this;
   }
 
-  void unload(const irep_idt &name) { goto_functions.unload(name); }
+  void unload(const irep_idt &name)
+  {
+    goto_functions.unload(name);
+  }
 
   // Implement the abstract goto model interface:
 

src/linking/remove_internal_symbols.cpp

@@ -71,7 +71,7 @@ static void get_symbols(
         find_type_and_expr_symbols(a, new_symbols);
       for(const exprt &e : maybe_contract.ensures())
         find_type_and_expr_symbols(e, new_symbols);
-      for(const exprt &r : maybe_contract.requires())
+      for(const exprt &r : maybe_contract.c_requires())
         find_type_and_expr_symbols(r, new_symbols);
 
       for(const auto &s : new_symbols)

src/util/c_types.h

@@ -390,7 +390,7 @@ class code_with_contract_typet : public code_typet
 
   bool has_contract() const
   {
-    return !ensures().empty() || !requires().empty() || !assigns().empty() ||
+    return !ensures().empty() || !c_requires().empty() || !assigns().empty() ||
            !frees().empty();
   }
 
@@ -414,12 +414,12 @@ class code_with_contract_typet : public code_typet
     return static_cast<exprt &>(add(ID_C_spec_frees)).operands();
   }
 
-  const exprt::operandst &requires() const
+  const exprt::operandst &c_requires() const
   {
     return static_cast<const exprt &>(find(ID_C_spec_requires)).operands();
   }
 
-  exprt::operandst &requires()
+  exprt::operandst &c_requires()
   {
     return static_cast<exprt &>(add(ID_C_spec_requires)).operands();
   }