Merge pull request #7751 from jparsert/fix_cpp20_requires_keyword

Changed "requires" as variable names to differentiate from c++20 keyword requires

Author: kroening

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

@@ -553,10 +553,14 @@ void dfcc_wrapper_programt::encode_requires_clauses()
   // translate each requires clause
   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();
-    if(has_subexpr(requires, ID_exists) || has_subexpr(requires, ID_forall))
-      add_quantified_variable(goto_model.symbol_table, requires, language_mode);
+    exprt requires_lmbd =
+      to_lambda_expr(r).application(contract_lambda_parameters);
+    requires_lmbd.add_source_location() = r.source_location();
+    if(
+      has_subexpr(requires_lmbd, ID_exists) ||
+      has_subexpr(requires_lmbd, ID_forall))
+      add_quantified_variable(
+        goto_model.symbol_table, requires_lmbd, language_mode);
 
     source_locationt sl(r.source_location());
     if(statement_type == ID_assert)
@@ -566,7 +570,7 @@ void dfcc_wrapper_programt::encode_requires_clauses()
         "Check requires clause of contract " + id2string(contract_symbol.name) +
         " for function " + id2string(wrapper_id));
     }
-    codet requires_statement(statement_type, {std::move(requires)}, sl);
+    codet requires_statement(statement_type, {std::move(requires_lmbd)}, sl);
     converter.goto_convert(requires_statement, requires_program, language_mode);
   }
 

src/goto-instrument/contracts/memory_predicates.cpp

@@ -111,10 +111,10 @@ void find_is_fresh_calls_visitort::operator()(goto_programt &prog)
   }
 }
 
-void is_fresh_baset::update_requires(goto_programt &requires)
+void is_fresh_baset::update_requires(goto_programt &requires_)
 {
   find_is_fresh_calls_visitort requires_visitor;
-  requires_visitor(requires);
+  requires_visitor(requires_);
   for(auto it : requires_visitor.is_fresh_calls())
   {
     create_requires_fn_call(it);

src/goto-instrument/contracts/memory_predicates.h

@@ -33,7 +33,7 @@ class is_fresh_baset
   {
   }
 
-  void update_requires(goto_programt &requires);
+  void update_requires(goto_programt &requires_);
   void update_ensures(goto_programt &ensures);
 
   virtual void create_declarations() = 0;