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.

Author: Petr Bauch

src/cbmc/cbmc_parse_options.cpp

@@ -515,6 +515,10 @@ int cbmc_parse_optionst::doit()
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
 
+  INVARIANT(
+    !goto_model.check_internal_invariants(*this),
+    "goto program internal invariants failed");
+
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {

src/goto-programs/goto_model.h

@@ -12,8 +12,10 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
 
-#include <util/symbol_table.h>
+#include <util/base_type.h>
 #include <util/journalling_symbol_table.h>
+#include <util/message.h>
+#include <util/symbol_table.h>
 
 #include "abstract_goto_model.h"
 #include "goto_functions.h"
@@ -95,6 +97,27 @@ class goto_modelt : public abstract_goto_modelt
     return goto_functions.function_map.find(id) !=
            goto_functions.function_map.end();
   }
+
+  /// Iterates over the functions inside the goto model and checks invariants
+  /// in all of them. Prints out error message collected.
+  /// \param msg message instance to collect errors
+  /// \return true if any violation was found
+  bool check_internal_invariants(messaget &msg) const
+  {
+    bool found_violation = false;
+    namespacet ns(symbol_table);
+    forall_goto_functions(it, goto_functions)
+    {
+      if(!base_type_eq(
+           it->second.type, symbol_table.lookup_ref(it->first).type, ns))
+      {
+        msg.error() << "error" << messaget::eom;
+        found_violation = true;
+      }
+    }
+
+    return found_violation;
+  }
 };
 
 /// Class providing the abstract GOTO model interface onto an unrelated