diff --git a/unit/Makefile b/unit/Makefile index 2a30357a825..d41c1770752 100644 --- a/unit/Makefile +++ b/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 \ diff --git a/unit/get_goto_model_from_c_test.cpp b/unit/get_goto_model_from_c_test.cpp new file mode 100644 index 00000000000..1b6f278716e --- /dev/null +++ b/unit/get_goto_model_from_c_test.cpp @@ -0,0 +1,40 @@ +/*******************************************************************\ + +Module: Get goto model test + +Author: Daniel Poetzl + +\*******************************************************************/ + +#include +#include + +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 = get_goto_model_from_c(code); + + 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")); +} diff --git a/unit/json_symbol_table.cpp b/unit/json_symbol_table.cpp index 9a475304323..e35a7e41191 100644 --- a/unit/json_symbol_table.cpp +++ b/unit/json_symbol_table.cpp @@ -23,6 +23,7 @@ #include #include +#include #include #include @@ -49,67 +50,11 @@ 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 - - { - std::string program = "int main() { return 0; }\n"; - - std::istringstream in(program); - get_goto_model(in, goto_model); - } + const std::string program = "int main() { return 0; }\n"; + const auto goto_model = get_goto_model_from_c(program); const symbol_tablet &symbol_table1 = goto_model.symbol_table; diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index 72a7f547f0b..df3ef1b5cca 100644 --- a/unit/testing-utils/Makefile +++ b/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 \ diff --git a/unit/testing-utils/get_goto_model_from_c.cpp b/unit/testing-utils/get_goto_model_from_c.cpp new file mode 100644 index 00000000000..d48c8967f10 --- /dev/null +++ b/unit/testing-utils/get_goto_model_from_c.cpp @@ -0,0 +1,95 @@ +/*******************************************************************\ + +Module: Get goto model + +Author: Daniel Poetzl + +\*******************************************************************/ + +#include "get_goto_model_from_c.h" + +#include + +#include + +#include +#include + +#include +#include +#include +#include +#include +#include +#include + +#include + +goto_modelt get_goto_model_from_c(std::istream &in) +{ + { + const bool has_language = get_language_from_mode(ID_C) != nullptr; + + if(!has_language) + { + register_language(new_ansi_c_language); + } + } + + { + cmdlinet cmdline; + + config = configt{}; + config.main = std::string("main"); + config.set(cmdline); + } + + language_filest language_files; + language_files.set_message_handler(null_message_handler); + + language_filet &language_file = language_files.add_file(""); + + language_file.language = get_language_from_mode(ID_C); + CHECK_RETURN(language_file.language); + + languaget &language = *language_file.language; + language.set_message_handler(null_message_handler); + + { + const bool error = language.parse(in, ""); + + if(error) + throw invalid_source_file_exceptiont("parsing failed"); + } + + language_file.get_modules(); + + goto_modelt goto_model; + + { + const bool error = language_files.typecheck(goto_model.symbol_table); + + if(error) + throw invalid_source_file_exceptiont("typechecking failed"); + } + + { + const bool error = + language_files.generate_support_functions(goto_model.symbol_table); + + if(error) + throw invalid_source_file_exceptiont( + "support function generation failed"); + } + + goto_convert( + goto_model.symbol_table, goto_model.goto_functions, null_message_handler); + + return goto_model; +} + +goto_modelt get_goto_model_from_c(const std::string &code) +{ + std::istringstream in(code); + return get_goto_model_from_c(in); +} diff --git a/unit/testing-utils/get_goto_model_from_c.h b/unit/testing-utils/get_goto_model_from_c.h new file mode 100644 index 00000000000..8b5c3d54057 --- /dev/null +++ b/unit/testing-utils/get_goto_model_from_c.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: Get goto model + +Author: Daniel Poetzl + +\*******************************************************************/ + +#ifndef CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H +#define CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H + +#include + +#include + +/// Convert C program to a goto model +/// +/// \param code: string giving the C program +/// \return goto model +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 +goto_modelt get_goto_model_from_c(const std::istream &in); + +#endif /* CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H_ */ diff --git a/unit/testing-utils/module_dependencies.txt b/unit/testing-utils/module_dependencies.txt index 636163352dd..eeed80f6cc0 100644 --- a/unit/testing-utils/module_dependencies.txt +++ b/unit/testing-utils/module_dependencies.txt @@ -1,5 +1,7 @@ +analyses ansi-c catch +goto-programs +langapi testing-utils -util -analyses +util \ No newline at end of file