From 226526499a50d7e3f70e62a3f602ec958632d2a1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 10 Apr 2022 13:30:37 +0000
Subject: [PATCH] CONTRACTS: Replace return_value_visitor by has_subexpr

There is no need to create infrastructure when an existing utility can
be used instead.
---
 src/goto-instrument/contracts/contracts.cpp   |  7 ++++---
 .../contracts/memory_predicates.cpp           | 13 -------------
 .../contracts/memory_predicates.h             | 19 -------------------
 3 files changed, 4 insertions(+), 35 deletions(-)

diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 6793bc025d8..4579b127cea 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/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.
diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp
index 37a5b6e7a0d..10eaa88f1d0 100644
--- a/src/goto-instrument/contracts/memory_predicates.cpp
+++ b/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;
diff --git a/src/goto-instrument/contracts/memory_predicates.h b/src/goto-instrument/contracts/memory_predicates.h
index 98820cbc955..4d71baa8d3a 100644
--- a/src/goto-instrument/contracts/memory_predicates.h
+++ b/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`.