Added unit test for wrong type in table

Builds a goto program with one assertion and checks that: 1) with the right type
in the table the validation succeeds, 2) with the wrong type the validation
fails.

Author: Petr Bauch

src/goto-programs/goto_program.cpp

@@ -675,8 +675,6 @@ void goto_programt::instructiont::validate(
 {
   namespacet ns(table);
   std::vector<std::vector<std::string>> type_collector;
-  std::stringstream location_stream;
-  location_stream << source_location;
 
   auto type_finder = [&](const exprt &e) {
     if(e.id() == ID_symbol)
@@ -685,13 +683,14 @@ void goto_programt::instructiont::validate(
       const auto &symbol_id = symbol_expr.get_identifier();
 
       if(table.has_symbol(symbol_id))
-        DATA_CHECK(
+        DATA_CHECK_WITH_DIAGNOSTICS(
           base_type_eq(
             symbol_expr.type(), table.lookup_ref(symbol_id).type, ns),
-          id2string(symbol_id) + " type inconsistency (" +
-            location_stream.str() + ")\n" + "goto program type: " +
-            symbol_expr.type().id_string() + "\n " + "symbol table type: " +
-            table.lookup_ref(symbol_id).type.id_string());
+          id2string(symbol_id) + " type inconsistency\n" +
+            "goto program type: " + symbol_expr.type().id_string() + "\n " +
+            "symbol table type: " +
+            table.lookup_ref(symbol_id).type.id_string(),
+          source_location);
     }
   };
 

unit/Makefile

@@ -15,6 +15,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        goto-programs/goto_trace_output.cpp \
+       goto-programs/goto_program_symbol_type_table_consistency.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \

unit/goto-programs/goto_program_symbol_type_table_consistency.cpp

@@ -0,0 +1,68 @@
+/*******************************************************************\
+
+ Module: Unit tests for goto_program::validate
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <goto-programs/goto_function.h>
+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO(
+  "Validation of consistent program/table pair (type-wise)",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A program with one assertion")
+  {
+    symbol_tablet symbol_table;
+    const typet type1 = signedbv_typet(32);
+    const typet type2 = signedbv_typet(64);
+    symbolt symbol;
+    irep_idt symbol_name = "a";
+    symbol.name = symbol_name;
+    symbol_exprt varx(symbol_name, type1);
+
+    exprt val10 = from_integer(10, type1);
+    binary_relation_exprt x_le_10(varx, ID_le, val10);
+
+    goto_functiont goto_function;
+    auto &instructions = goto_function.body.instructions;
+    instructions.emplace_back(goto_program_instruction_typet::ASSERT);
+    instructions.back().make_assertion(x_le_10);
+
+    WHEN("Symbol table has the right symbol type")
+    {
+      symbol.type = type1;
+      symbol_table.insert(symbol);
+
+      THEN("The consistency check succeeds")
+      {
+        goto_function.validate(symbol_table, validation_modet::INVARIANT);
+
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Symbol table has the wrong symbol type")
+    {
+      symbol.type = type2;
+      symbol_table.insert(symbol);
+
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_function.validate(symbol_table, validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}