Introduce get_goto_model_from_c() for use in unit tests

The function takes a C program (as a string or an input stream) and converts it
to a goto model.

Author: danpoe

unit/Makefile

@@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        big-int/big-int.cpp \
        compound_block_locations.cpp \
+       get_goto_model_from_c_test.cpp \
        goto-checker/report_util/is_property_less_than.cpp \
        goto-instrument/cover_instrument.cpp \
        goto-instrument/cover/cover_only.cpp \

unit/get_goto_model_from_c_test.cpp

@@ -0,0 +1,43 @@
+/*******************************************************************\
+
+Module: Get goto model test
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#include <testing-utils/use_catch.h>
+#include <testing-utils/get_goto_model_from_c.h>
+
+TEST_CASE("Get goto model from C test", "[core]")
+{
+  const std::string code =
+    "int g;"
+    "void f(int a) { int b; }"
+    "void main() {}";
+
+  const auto goto_model_opt = get_goto_model_from_c(code);
+  REQUIRE(goto_model_opt);
+
+  const auto &goto_model = *goto_model_opt;
+
+  const auto &function_map = goto_model.goto_functions.function_map;
+
+  REQUIRE(function_map.find("main") != function_map.end());
+  REQUIRE(function_map.find(CPROVER_PREFIX "_start") != function_map.end());
+  REQUIRE(function_map.find("f") != function_map.end());
+
+  const auto &main_instructions = function_map.at("main").body.instructions;
+  REQUIRE(!main_instructions.empty());
+
+  const auto &f_instructions = function_map.at("f").body.instructions;
+  REQUIRE(f_instructions.size() >= 2);
+
+  const auto &symbol_table = goto_model.symbol_table;
+
+  REQUIRE(symbol_table.has_symbol("main"));
+  REQUIRE(symbol_table.has_symbol(CPROVER_PREFIX "_start"));
+  REQUIRE(symbol_table.has_symbol("g"));
+  REQUIRE(symbol_table.has_symbol("f::a"));
+  REQUIRE(symbol_table.has_symbol("f::1::b"));
+}

unit/json_symbol_table.cpp

@@ -23,6 +23,7 @@
 #include <util/options.h>
 #include <util/symbol_table.h>
 
+#include <testing-utils/get_goto_model_from_c.h>
 #include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
@@ -49,67 +50,14 @@ class test_ui_message_handlert : public ui_message_handlert
   json_stream_arrayt json_stream_array;
 };
 
-void get_goto_model(std::istream &in, goto_modelt &goto_model)
-{
-  optionst options;
-  cbmc_parse_optionst::set_default_options(options);
-
-  messaget null_message(null_message_handler);
-
-  language_filest language_files;
-  language_files.set_message_handler(null_message_handler);
-
-  std::string filename;
-
-  language_filet &language_file = language_files.add_file(filename);
-
-  language_file.language = get_default_language();
-
-  languaget &language = *language_file.language;
-  language.set_message_handler(null_message_handler);
-  language.set_language_options(options);
-
-  {
-    bool r = language.parse(in, filename);
-    REQUIRE(!r);
-  }
-
-  language_file.get_modules();
-
-  {
-    bool r = language_files.typecheck(goto_model.symbol_table);
-    REQUIRE(!r);
-  }
-
-  REQUIRE(!goto_model.symbol_table.has_symbol(goto_functionst::entry_point()));
-
-  {
-    bool r = language_files.generate_support_functions(goto_model.symbol_table);
-    REQUIRE(!r);
-  }
-
-  goto_convert(
-    goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
-}
-
 TEST_CASE("json symbol table read/write consistency")
 {
-  register_language(new_ansi_c_language);
-
-  cmdlinet cmdline;
-  config.main = std::string("main");
-  config.set(cmdline);
-
-  goto_modelt goto_model;
-
   // Get symbol table associated with goto program
+  const std::string program = "int main() { return 0; }\n";
+  const auto goto_model_opt = get_goto_model_from_c(program);
 
-  {
-    std::string program = "int main() { return 0; }\n";
-
-    std::istringstream in(program);
-    get_goto_model(in, goto_model);
-  }
+  REQUIRE(goto_model_opt);
+  const auto &goto_model = *goto_model_opt;
 
   const symbol_tablet &symbol_table1 = goto_model.symbol_table;
 

unit/testing-utils/Makefile

@@ -1,6 +1,7 @@
 SRC = \
   call_graph_test_utils.cpp \
   free_form_cmdline.cpp \
+  get_goto_model_from_c.cpp \
   invariant.cpp \
   message.cpp \
   require_expr.cpp \

unit/testing-utils/get_goto_model_from_c.cpp

@@ -0,0 +1,105 @@
+/*******************************************************************\
+
+Module: Get goto model
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#include "get_goto_model_from_c.h"
+
+#include <ansi-c/ansi_c_language.h>
+
+#include <cbmc/cbmc_parse_options.h>
+
+#include <goto-programs/goto_convert_functions.h>
+
+#include <langapi/language_file.h>
+#include <langapi/mode.h>
+
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/invariant.h>
+#include <util/message.h>
+#include <util/options.h>
+#include <util/symbol_table.h>
+
+#include <testing-utils/message.h>
+
+namespace
+{
+bool initialized = false;
+optionst options;
+
+void initialize()
+{
+  PRECONDITION(!initialized);
+
+  register_language(new_ansi_c_language);
+
+  cmdlinet cmdline;
+
+  config.main = std::string("main");
+  config.set(cmdline);
+
+  optionst options;
+  cbmc_parse_optionst::set_default_options(options);
+}
+}
+
+optionalt<goto_modelt> get_goto_model_from_c(std::istream &in)
+{
+  if(!initialized)
+  {
+    initialize();
+    initialized = true;
+  }
+
+  language_filest language_files;
+  language_files.set_message_handler(null_message_handler);
+
+  language_filet &language_file = language_files.add_file("");
+
+  language_file.language = get_default_language();
+
+  languaget &language = *language_file.language;
+  language.set_message_handler(null_message_handler);
+  language.set_language_options(options);
+
+  {
+    const bool error = language.parse(in, "");
+
+    if(error)
+      return {};
+  }
+
+  language_file.get_modules();
+
+  goto_modelt goto_model;
+
+  {
+    const bool error = language_files.typecheck(goto_model.symbol_table);
+
+    if(error)
+      return {};
+  }
+
+  {
+    const bool error =
+      language_files.generate_support_functions(goto_model.symbol_table);
+
+    if(error)
+      return {};
+  }
+
+  goto_convert(
+    goto_model.symbol_table, goto_model.goto_functions, null_message_handler);
+
+  return goto_model;
+}
+
+optionalt<goto_modelt> get_goto_model_from_c(const std::string &code)
+{
+  std::istringstream in(code);
+  return get_goto_model_from_c(in);
+}

unit/testing-utils/get_goto_model_from_c.h

@@ -0,0 +1,30 @@
+/*******************************************************************\
+
+Module: Get goto model
+
+Author: Daniel Poetzl
+
+\*******************************************************************/
+
+#ifndef UNIT_TESTING_UTILS_GET_GOTO_MODEL_H
+#define UNIT_TESTING_UTILS_GET_GOTO_MODEL_H
+
+#include <goto-programs/goto_model.h>
+
+#include <util/optional.h>
+
+#include <iosfwd>
+
+/// Convert C program to a goto model
+///
+/// \param code: string giving the C program
+/// \return goto model if successful, empty optional otherwise
+optionalt<goto_modelt> get_goto_model_from_c(const std::string &code);
+
+/// Convert C program to a goto model
+///
+/// \param in: input stream to read a C program from
+/// \return goto model if successful, empty optional otherwise
+optionalt<goto_modelt> get_goto_model_from_c(const std::istream &in);
+
+#endif /* UNIT_TESTING_UTILS_GET_GOTO_MODEL_H_ */