Merge pull request #4212 from diffblue/undeclared_function

added test for undeclared functions

Author: tautschnig

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);
+}

regression/ansi-c/undeclared_function/fileB.c

@@ -0,0 +1,6 @@
+#include <stdlib.h>
+
+int f()
+{
+  malloc(4);
+}

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$

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);
 

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;
 

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

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);
 

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
 };

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;

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
 };
 

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);
 

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)
 {

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);