Function type consistency between goto programs and symbol table

A simple iteration over goto-functions to check that it's base type is the same
as the one stored in the symbol table. Includes a unit test.

Author: Petr Bauch

src/goto-programs/goto_functions.h

@@ -127,6 +127,14 @@ class goto_functionst
     for(const auto &entry : function_map)
     {
       const goto_functiont &goto_function = entry.second;
+      const auto &function_name = entry.first;
+
+      DATA_CHECK(
+        goto_function.type == ns.lookup(function_name).type,
+        id2string(function_name) + " type inconsistency\ngoto program type: " +
+          goto_function.type.id_string() +
+          "\nsymbol table type: " + ns.lookup(function_name).type.id_string());
+
       goto_function.validate(ns, vm);
     }
   }

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 \
        compound_block_locations.cpp \
+       goto-programs/goto_model_function_type_consistency.cpp \
        goto-programs/goto_program_assume.cpp \
        goto-programs/goto_program_dead.cpp \
        goto-programs/goto_program_declaration.cpp \

unit/goto-programs/goto_model_function_type_consistency.cpp

@@ -0,0 +1,67 @@
+/*******************************************************************\
+
+ 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);
+
+      THEN("The consistency check succeeds")
+      {
+        goto_model.validate(validation_modet::INVARIANT);
+
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Symbol table has the wrong type")
+    {
+      function_symbol.type = fun_type2;
+      goto_model.symbol_table.insert(function_symbol);
+
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_model.validate(validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}