Fix based on comments

Author: Petr Bauch

src/goto-programs/goto_function.h

@@ -119,11 +119,16 @@ class goto_functiont
   void validate(const namespacet &ns, const validation_modet vm) const
   {
     body.validate(ns, vm);
-    source_locationt nil_location;
-    nil_location.make_nil();
-    forall_subtypes(it, type)
+
+    find_symbols_sett typetags;
+    find_type_symbols(type, typetags);
+    const symbolt *symbol;
+    for(const auto &identifier : typetags)
     {
-      find_typetag_in_namespace(*it, nil_location, ns, vm);
+      DATA_CHECK(
+        vm,
+        !ns.lookup(identifier, symbol),
+        id2string(identifier) + " not found");
     }
 
     validate_full_type(type, ns, vm);

src/goto-programs/goto_program.cpp

@@ -11,9 +11,11 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_program.h"
 
-#include <ostream>
+#include <algorithm>
 #include <iomanip>
+#include <ostream>
 
+#include <util/expr_iterator.h>
 #include <util/find_symbols.h>
 #include <util/std_expr.h>
 #include <util/validate.h>
@@ -685,11 +687,18 @@ void goto_programt::instructiont::validate(
     source_location);
 
   auto expr_symbol_finder = [&](const exprt &e) {
-    forall_subtypes(it, e.type())
+    find_symbols_sett typetags;
+    find_type_symbols(e.type(), typetags);
+    find_symbols(e, typetags);
+    const symbolt *symbol;
+    for(const auto &identifier : typetags)
     {
-      find_typetag_in_namespace(*it, source_location, ns, vm);
+      DATA_CHECK_WITH_DIAGNOSTICS(
+        vm,
+        !ns.lookup(identifier, symbol),
+        id2string(identifier) + " not found",
+        source_location);
     }
-    find_symbol_in_namespace(e, source_location, ns, vm);
   };
 
   auto &current_source_location = source_location;
@@ -742,8 +751,8 @@ void goto_programt::instructiont::validate(
       "assert instruction should not have a target",
       source_location);
 
-    guard.visit(expr_symbol_finder);
-    guard.visit(type_finder);
+    std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
+    std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
     break;
   case OTHER:
     break;
@@ -809,8 +818,8 @@ void goto_programt::instructiont::validate(
       "function call instruction should contain a call statement",
       source_location);
 
-    code.visit(expr_symbol_finder);
-    code.visit(type_finder);
+    std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
+    std::for_each(code.depth_begin(), code.depth_end(), type_finder);
     break;
   case THROW:
     break;

src/util/expr.cpp

@@ -279,20 +279,6 @@ void exprt::visit(const_expr_visitort &visitor) const
   }
 }
 
-void exprt::visit(const std::function<void(const exprt &)> &f) const
-{
-  std::stack<const exprt *> stack;
-  stack.push(this);
-  while(!stack.empty())
-  {
-    const exprt &expr = *stack.top();
-    stack.pop();
-    f(expr);
-    forall_operands(it, expr)
-      stack.push(&(*it));
-  }
-}
-
 depth_iteratort exprt::depth_begin()
 { return depth_iteratort(*this); }
 depth_iteratort exprt::depth_end()

src/util/expr.h

@@ -305,12 +305,6 @@ class exprt:public irept
   void visit(class expr_visitort &visitor);
   void visit(class const_expr_visitort &visitor) const;
 
-  /// Recursively traverse the expression tree (via operands) and call \p f on
-  /// every subexpressions, including `this`. The input function has
-  /// side-effects and does not modify the expression.
-  /// \param f: The function to be call on subexpressions
-  void visit(const std::function<void(const exprt &)> &f) const;
-
   depth_iteratort depth_begin();
   depth_iteratort depth_end();
   const_depth_iteratort depth_begin() const;

src/util/find_symbols.cpp

@@ -210,55 +210,3 @@ void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
 {
   find_symbols(kindt::F_BOTH, src, dest);
 }
-
-void find_typetag_in_namespace(
-  const typet &src,
-  const source_locationt &location,
-  const namespacet &ns,
-  const validation_modet vm)
-{
-  irep_idt identifier = ID_nil;
-  if(src.id() == ID_symbol_type)
-  {
-    identifier = to_symbol_type(src).get_identifier();
-  }
-  else if(
-    src.id() == ID_c_enum_tag || src.id() == ID_struct_tag ||
-    src.id() == ID_union_tag)
-  {
-    identifier = to_tag_type(src).get_identifier();
-  }
-  if(identifier != ID_nil)
-  {
-    const symbolt *symbol;
-    if(location.is_nil())
-      DATA_CHECK(
-        vm,
-        !ns.lookup(identifier, symbol),
-        id2string(identifier) + " not found");
-    else
-      DATA_CHECK_WITH_DIAGNOSTICS(
-        vm,
-        !ns.lookup(identifier, symbol),
-        id2string(identifier) + " not found",
-        location);
-  }
-}
-
-void find_symbol_in_namespace(
-  const exprt &src,
-  const source_locationt &location,
-  const namespacet &ns,
-  const validation_modet vm)
-{
-  if(src.id() == ID_symbol)
-  {
-    const symbolt *symbol;
-    auto identifier = to_symbol_expr(src).get_identifier();
-    DATA_CHECK_WITH_DIAGNOSTICS(
-      vm,
-      !ns.lookup(identifier, symbol),
-      id2string(identifier) + " not found",
-      location);
-  }
-}

src/util/find_symbols.h

@@ -18,10 +18,10 @@ Author: Daniel Kroening, [email protected]
 #include "validate.h"
 
 class exprt;
+class source_locationt;
 class symbol_exprt;
-class typet;
 class symbolt;
-class source_locationt;
+class typet;
 
 typedef std::unordered_set<irep_idt> find_symbols_sett;
 
@@ -71,16 +71,4 @@ void find_type_and_expr_symbols(
   const exprt &src,
   find_symbols_sett &dest);
 
-void find_typetag_in_namespace(
-  const typet &src,
-  const source_locationt &location,
-  const namespacet &ns,
-  const validation_modet vm);
-
-void find_symbol_in_namespace(
-  const exprt &src,
-  const source_locationt &location,
-  const namespacet &ns,
-  const validation_modet vm);
-
 #endif // CPROVER_UTIL_FIND_SYMBOLS_H

unit/Makefile

@@ -64,7 +64,6 @@ SRC += analyses/ai/ai.cpp \
        util/string_utils/strip_string.cpp \
        util/symbol_table.cpp \
        util/unicode.cpp \
-       util/visit.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.