diff --git a/regression/ansi-c/undeclared_function/fileA.c b/regression/ansi-c/undeclared_function/fileA.c
new file mode 100644
index 00000000000..e6f88a9f664
--- /dev/null
+++ b/regression/ansi-c/undeclared_function/fileA.c
@@ -0,0 +1,7 @@
+// There is no #include <stdlib.h> here, deliberately,
+// to trigger automatic generation of a signature below.
+
+int main(void)
+{
+  malloc(4);
+}
diff --git a/regression/ansi-c/undeclared_function/fileB.c b/regression/ansi-c/undeclared_function/fileB.c
new file mode 100644
index 00000000000..08bdda49110
--- /dev/null
+++ b/regression/ansi-c/undeclared_function/fileB.c
@@ -0,0 +1,6 @@
+#include <stdlib.h>
+
+int f()
+{
+  malloc(4);
+}
diff --git a/regression/ansi-c/undeclared_function/undeclared_function1.desc b/regression/ansi-c/undeclared_function/undeclared_function1.desc
new file mode 100644
index 00000000000..d002ebcf531
--- /dev/null
+++ b/regression/ansi-c/undeclared_function/undeclared_function1.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+fileA.c
+fileB.c --validate-goto-model
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-cc/armcc_mode.cpp
index 03a3a0e689a..09d6f563320 100644
--- a/src/goto-cc/armcc_mode.cpp
+++ b/src/goto-cc/armcc_mode.cpp
@@ -51,6 +51,9 @@ int armcc_modet::doit()
 
   debug() << "ARM mode" << eom;
 
+  // model validation
+  compiler.validate_goto_model = cmdline.isset("validate-goto-model");
+
   // get configuration
   config.set(cmdline);
 
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 11e6ca36f98..8b47a0aa10b 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -542,6 +542,12 @@ bool compilet::write_bin_object_file(
   const std::string &file_name,
   const goto_modelt &src_goto_model)
 {
+  if(validate_goto_model)
+  {
+    status() << "Validating goto model" << eom;
+    src_goto_model.validate(validation_modet::INVARIANT);
+  }
+
   statistics() << "Writing binary format object `"
                << file_name << "'" << eom;
 
diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h
index 6a157371160..3d80d0d8e7b 100644
--- a/src/goto-cc/compile.h
+++ b/src/goto-cc/compile.h
@@ -34,6 +34,7 @@ class compilet : public messaget
   bool echo_file_name;
   std::string working_directory;
   std::string override_language;
+  bool validate_goto_model = false;
 
   enum { PREPROCESS_ONLY, // gcc -E
          COMPILE_ONLY, // gcc -c
diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-cc/cw_mode.cpp
index eed01de1d55..fbfc56c6128 100644
--- a/src/goto-cc/cw_mode.cpp
+++ b/src/goto-cc/cw_mode.cpp
@@ -51,6 +51,9 @@ int cw_modet::doit()
 
   debug() << "CodeWarrior mode" << eom;
 
+  // model validation
+  compiler.validate_goto_model = cmdline.isset("validate-goto-model");
+
   // get configuration
   config.set(cmdline);
 
diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp
index 5b52abfd2b3..a80ffa91da7 100644
--- a/src/goto-cc/gcc_cmdline.cpp
+++ b/src/goto-cc/gcc_cmdline.cpp
@@ -49,6 +49,7 @@ const char *goto_cc_options_without_argument[]=
   "--big-endian",
   "--no-arch",
   "--partial-inlining",
+  "--validate-goto-model",
   "-?",
   nullptr
 };
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
index 921c3a7230c..358708157dd 100644
--- a/src/goto-cc/gcc_mode.cpp
+++ b/src/goto-cc/gcc_mode.cpp
@@ -423,6 +423,9 @@ int gcc_modet::doit()
       debug() << "GCC mode" << eom;
   }
 
+  // model validation
+  compiler.validate_goto_model = cmdline.isset("validate-goto-model");
+
   // determine actions to be undertaken
   if(cmdline.isset('S'))
     compiler.mode=compilet::ASSEMBLE_ONLY;
diff --git a/src/goto-cc/ld_cmdline.cpp b/src/goto-cc/ld_cmdline.cpp
index a96880b4f8d..86da9e24b77 100644
--- a/src/goto-cc/ld_cmdline.cpp
+++ b/src/goto-cc/ld_cmdline.cpp
@@ -22,6 +22,7 @@ const char *goto_ld_options_with_argument[]=
   "--verbosity",
   "--native-compiler",
   "--native-linker",
+  "--validate-goto-model",
   nullptr
 };
 
diff --git a/src/goto-cc/ld_mode.cpp b/src/goto-cc/ld_mode.cpp
index 1c6e0298e93..e00a6746436 100644
--- a/src/goto-cc/ld_mode.cpp
+++ b/src/goto-cc/ld_mode.cpp
@@ -96,6 +96,9 @@ int ld_modet::doit()
   // determine actions to be undertaken
   compiler.mode = compilet::LINK_LIBRARY;
 
+  // model validation
+  compiler.validate_goto_model = cmdline.isset("validate-goto-model");
+
   // get configuration
   config.set(cmdline);
 
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp
index ad1df7e69de..9736ce801a2 100644
--- a/src/goto-cc/ms_cl_cmdline.cpp
+++ b/src/goto-cc/ms_cl_cmdline.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening
 /// parses the command line options into a cmdlinet
 /// \par parameters: argument count, argument strings
 /// \return none
+// clang-format off
 const char *non_ms_cl_options[]=
 {
   "--show-symbol-table",
@@ -44,8 +45,10 @@ const char *non_ms_cl_options[]=
   "--partial-inlining",
   "--verbosity",
   "--function",
+  "--validate-goto-model",
   nullptr
 };
+// clang-format on
 
 bool ms_cl_cmdlinet::parse(const std::vector<std::string> &arguments)
 {
diff --git a/src/goto-cc/ms_cl_mode.cpp b/src/goto-cc/ms_cl_mode.cpp
index 8fc9f2c47c9..2dc6706c3dd 100644
--- a/src/goto-cc/ms_cl_mode.cpp
+++ b/src/goto-cc/ms_cl_mode.cpp
@@ -65,6 +65,9 @@ int ms_cl_modet::doit()
 
   debug() << "Visual Studio mode " << ms_cl_version << eom;
 
+  // model validation
+  compiler.validate_goto_model = cmdline.isset("validate-goto-model");
+
   // get configuration
   config.set(cmdline);