Merge pull request #6797 from tautschnig/cleanup/remove-return_value_visitor

CONTRACTS: Replace return_value_visitor by has_subexpr

Author: tautschnig

src/goto-instrument/contracts/contracts.cpp

@@ -780,9 +780,10 @@ void code_contractst::apply_function_contract(
     {
       // If the function does return a value, but the return value is
       // disregarded, check if the postcondition includes the return value.
-      return_value_visitort v;
-      ensures.visit(v);
-      if(v.found_return_value())
+      if(has_subexpr(ensures, [](const exprt &e) {
+           return e.id() == ID_symbol && to_symbol_expr(e).get_identifier() ==
+                                           CPROVER_PREFIX "return_value";
+         }))
       {
         // The postcondition does mention __CPROVER_return_value, so mint a
         // fresh variable to replace __CPROVER_return_value with.

src/goto-instrument/contracts/memory_predicates.cpp

@@ -23,19 +23,6 @@ Date: July 2021
 #include <util/config.h>
 #include <util/prefix.h>
 
-bool return_value_visitort::found_return_value()
-{
-  return found;
-}
-
-void return_value_visitort::operator()(const exprt &exp)
-{
-  if(exp.id() != ID_symbol)
-    return;
-  const symbol_exprt &sym = to_symbol_expr(exp);
-  found |= sym.get_identifier() == CPROVER_PREFIX "return_value";
-}
-
 std::set<irep_idt> &functions_in_scope_visitort::function_calls()
 {
   return function_set;

src/goto-instrument/contracts/memory_predicates.h

@@ -101,25 +101,6 @@ class find_is_fresh_calls_visitort
   std::set<goto_programt::targett> function_set;
 };
 
-/// Predicate to be used with the exprt::visit() function. The function
-/// found_return_value() will return `true` iff this predicate is called on an
-/// expr that contains `__CPROVER_return_value`.
-class return_value_visitort : public const_expr_visitort
-{
-public:
-  return_value_visitort() : const_expr_visitort(), found(false)
-  {
-  }
-
-  // \brief Has this object been passed to exprt::visit() on an exprt whose
-  //        descendants contain __CPROVER_return_value?
-  bool found_return_value();
-  void operator()(const exprt &exp) override;
-
-protected:
-  bool found;
-};
-
 /// Predicate to be used with the exprt::visit() function. The function
 /// found_return_value() will return `true` iff this predicate is called on an
 /// expr that contains `__CPROVER_return_value`.