Added unit test for wrong type in table

Builds a goto model with one function 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

jbmc/lib/java-models-library

@@ -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_model_function_type_consistency.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \

unit/Makefile

@@ -0,0 +1,69 @@
+/*******************************************************************\
+
+ Module: Unit tests for goto_model::validate
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <goto-programs/goto_model.h>
+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO(
+  "Validation of consistent program/table pair (function type)",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A model with one function")
+  {
+    const typet type1 = signedbv_typet(32);
+    const typet type2 = signedbv_typet(64);
+    code_typet fun_type1({}, type1);
+    code_typet fun_type2({}, type2);
+
+    symbolt function_symbol;
+    irep_idt function_symbol_name = "foo";
+    function_symbol.name = function_symbol_name;
+
+    goto_modelt goto_model;
+    goto_model.goto_functions.function_map[function_symbol.name] =
+      goto_functiont();
+    goto_model.goto_functions.function_map[function_symbol.name].type =
+      fun_type1;
+
+    WHEN("Symbol table has the right type")
+    {
+      function_symbol.type = fun_type1;
+      goto_model.symbol_table.insert(function_symbol);
+      namespacet ns(goto_model.symbol_table);
+
+      THEN("The consistency check succeeds")
+      {
+        goto_model.validate(ns, validation_modet::INVARIANT);
+
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Symbol table has the wrong type")
+    {
+      function_symbol.type = fun_type2;
+      goto_model.symbol_table.insert(function_symbol);
+      namespacet ns(goto_model.symbol_table);
+
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_model.validate(ns, validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}