Small fixes based on comments

This commit will likely be squashed.

Author: Petr Bauch

src/goto-programs/goto_functions.h

@@ -115,19 +115,6 @@ class goto_functionst
       function_map[fun.first].copy_from(fun.second);
   }
 
-  /// Check that the goto functions are well-formed
-  ///
-  /// The validation mode indicates whether well-formedness check failures are
-  /// reported via DATA_INVARIANT violations or exceptions.
-  void validate(const namespacet &ns, const validation_modet vm) const
-  {
-    for(const auto &entry : function_map)
-    {
-      const goto_functiont &goto_function = entry.second;
-      goto_function.validate(ns, vm);
-    }
-  }
-
   std::vector<function_mapt::const_iterator> sorted() const;
   std::vector<function_mapt::iterator> sorted();
 

src/goto-symex/symex_target_equation.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_target_equation.h"
 
+#include <util/base_type.h>
 #include <util/format_expr.h>
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
@@ -977,6 +978,9 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
   out << "Guard: " << format(guard) << '\n';
 }
 
+/// Check that the SSA step is well-formed
+/// \param ns namespace to lookup identifiers
+/// \param vm validation mode to be used for reporting failures
 void symex_target_equationt::SSA_stept::validate(
   const namespacet &ns,
   const validation_modet vm) const
@@ -997,27 +1001,32 @@ void symex_target_equationt::SSA_stept::validate(
     validate_expr_full_pick(ssa_full_lhs, ns, vm);
     validate_expr_full_pick(original_full_lhs, ns, vm);
     validate_expr_full_pick(ssa_rhs, ns, vm);
+    base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns);
     break;
   case goto_trace_stept::typet::INPUT:
   case goto_trace_stept::typet::OUTPUT:
     for(const auto &expr : io_args)
       validate_expr_full_pick(expr, ns, vm);
-    for(const auto &expr : converted_io_args)
-      validate_expr_full_pick(expr, ns, vm);
     break;
   case goto_trace_stept::typet::FUNCTION_CALL:
     for(const auto &expr : ssa_function_arguments)
       validate_expr_full_pick(expr, ns, vm);
-    for(const auto &expr : converted_function_arguments)
-      validate_expr_full_pick(expr, ns, vm);
   case goto_trace_stept::typet::FUNCTION_RETURN:
   {
     const symbolt *symbol;
     DATA_CHECK(
       !ns.lookup(function_identifier, symbol), "unknown function identifier");
   }
   break;
-  default:
+  case goto_trace_stept::typet::NONE:
+  case goto_trace_stept::typet::LOCATION:
+  case goto_trace_stept::typet::DEAD:
+  case goto_trace_stept::typet::SHARED_READ:
+  case goto_trace_stept::typet::SHARED_WRITE:
+  case goto_trace_stept::typet::SPAWN:
+  case goto_trace_stept::typet::MEMORY_BARRIER:
+  case goto_trace_stept::typet::ATOMIC_BEGIN:
+  case goto_trace_stept::typet::ATOMIC_END:
     break;
   }
 }

src/util/ssa_expr.h

@@ -142,7 +142,7 @@ class ssa_exprt:public symbol_exprt
 
   void check(const validation_modet vm = validation_modet::INVARIANT) const
   {
-    DATA_CHECK(!has_operands(), "SSA expression do not have operands");
+    DATA_CHECK(!has_operands(), "SSA expression should not have operands");
     DATA_CHECK(id() == ID_symbol, "SSA expression symbols are symbols");
     DATA_CHECK(get_bool(ID_C_SSA_symbol), "wrong SSA expression ID");
   }

src/util/validate_expressions.cpp

@@ -14,7 +14,7 @@ Author: Daniel Poetzl
 
 #include "expr.h"
 #include "namespace.h"
-#include "std_expr.h"
+#include "ssa_expr.h"
 #include "validate.h"
 
 #define CALL_ON_EXPR(expr_type)                                                \
@@ -31,6 +31,10 @@ void call_on_expr(const exprt &expr, Args &&... args)
   {
     CALL_ON_EXPR(plus_exprt);
   }
+  else if(expr.get_bool(ID_C_SSA_symbol))
+  {
+    CALL_ON_EXPR(ssa_exprt);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS