diff --git a/doc/architectural/code-walkthrough.md b/doc/architectural/code-walkthrough.md index 008f52d855b..ed65b8bef7f 100644 --- a/doc/architectural/code-walkthrough.md +++ b/doc/architectural/code-walkthrough.md @@ -14,7 +14,7 @@ See \ref goto-programs, \ref goto_programt and [instructiont](\ref goto_programt \section front-end-languages-generating-codet-from-multiple-languages-section Front-end languages: generating codet from multiple languages -\subsection language-uit-section language_uit, language_filest, languaget classes: +\subsection language-uit-section language_filest, languaget classes: See \ref langapi. diff --git a/src/langapi/Makefile b/src/langapi/Makefile index ea85a9213b8..290d2023638 100644 --- a/src/langapi/Makefile +++ b/src/langapi/Makefile @@ -1,5 +1,4 @@ -SRC = language_ui.cpp \ - language_util.cpp \ +SRC = language_util.cpp \ language_file.cpp \ language.cpp \ mode.cpp \ diff --git a/src/langapi/README.md b/src/langapi/README.md index e3c3e94f684..ca50a5cc79b 100644 --- a/src/langapi/README.md +++ b/src/langapi/README.md @@ -19,10 +19,6 @@ To be documented. To be documented. -\section langapi-manipulation-framework The top-level language-file manipulation framework (language_uit, obsolete, replaced by initialize_goto_model) - -To be documented. - \section langapi-mode-related-utils Symbol mode-related utilities (everything in mode.h) To be documented. diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp deleted file mode 100644 index b6d6ba724c8..00000000000 --- a/src/langapi/language_ui.cpp +++ /dev/null @@ -1,245 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@cs.cmu.edu - -\*******************************************************************/ - -#include "language_ui.h" - -#include -#include -#include - -#include -#include -#include -#include -#include - -#include "language.h" -#include "mode.h" - -/// Constructor -language_uit::language_uit( - const cmdlinet &cmdline, - ui_message_handlert &_ui_message_handler, - optionst *_options) - : _cmdline(cmdline), - ui_message_handler(_ui_message_handler), - options(_options) -{ - set_message_handler(ui_message_handler); -} - -/// Destructor -language_uit::~language_uit() -{ -} - -bool language_uit::parse() -{ - for(const auto &filename : _cmdline.args) - if(parse(filename)) - return true; - - return false; -} - -bool language_uit::parse(const std::string &filename) -{ - #ifdef _MSC_VER - std::ifstream infile(widen(filename)); - #else - std::ifstream infile(filename); - #endif - - if(!infile) - { - error() << "failed to open input file `" << filename << "'" << eom; - return true; - } - - language_filet &lf=language_files.add_file(filename); - lf.language=get_language_from_filename(filename); - - if(lf.language==nullptr) - { - source_locationt location; - location.set_file(filename); - error().source_location=location; - error() << "failed to figure out type of file" << eom; - return true; - } - - languaget &language=*lf.language; - language.set_message_handler(get_message_handler()); - - if(options != nullptr) - language.set_language_options(*options); - - status() << "Parsing " << filename << eom; - - if(language.parse(infile, filename)) - { - if(get_ui()==ui_message_handlert::uit::PLAIN) - std::cerr << "PARSING ERROR\n"; - - return true; - } - - lf.get_modules(); - - return false; -} - -bool language_uit::typecheck() -{ - status() << "Converting" << eom; - - language_files.set_message_handler(*message_handler); - - if(language_files.typecheck(symbol_table)) - { - error() << "CONVERSION ERROR" << eom; - return true; - } - - return false; -} - -bool language_uit::final() -{ - language_files.set_message_handler(*message_handler); - - if(language_files.final(symbol_table)) - { - error() << "CONVERSION ERROR" << eom; - return true; - } - - config.set_object_bits_from_symbol_table(symbol_table); - - return false; -} - -void language_uit::show_symbol_table(bool brief) -{ - switch(get_ui()) - { - case ui_message_handlert::uit::PLAIN: - show_symbol_table_plain(std::cout, brief); - break; - - case ui_message_handlert::uit::XML_UI: - show_symbol_table_xml_ui(brief); - break; - - default: - error() << "cannot show symbol table in this format" << eom; - } -} - -void language_uit::show_symbol_table_xml_ui(bool) -{ - error() << "cannot show symbol table in this format" << eom; -} - -void language_uit::show_symbol_table_plain( - std::ostream &out, - bool brief) -{ - if(!brief) - out << "\nSymbols:\n\n"; - - // we want to sort alphabetically - std::set symbols; - - for(const auto &symbol_pair : symbol_table.symbols) - { - symbols.insert(id2string(symbol_pair.first)); - } - - const namespacet ns(symbol_table); - - for(const std::string &id : symbols) - { - const symbolt &symbol=ns.lookup(id); - - std::unique_ptr ptr; - - if(symbol.mode=="") - { - ptr=get_default_language(); - } - else - { - ptr=get_language_from_mode(symbol.mode); - } - - if(!ptr) - throw "symbol "+id2string(symbol.name)+" has unknown mode"; - - std::string type_str, value_str; - - if(symbol.type.is_not_nil()) - ptr->from_type(symbol.type, type_str, ns); - - if(symbol.value.is_not_nil()) - ptr->from_expr(symbol.value, value_str, ns); - - if(brief) - { - out << symbol.name << " " << type_str << '\n'; - continue; - } - - out << "Symbol......: " << symbol.name << '\n' << std::flush; - out << "Pretty name.: " << symbol.pretty_name << '\n'; - out << "Module......: " << symbol.module << '\n'; - out << "Base name...: " << symbol.base_name << '\n'; - out << "Mode........: " << symbol.mode << '\n'; - out << "Type........: " << type_str << '\n'; - out << "Value.......: " << value_str << '\n'; - out << "Flags.......:"; - - if(symbol.is_lvalue) - out << " lvalue"; - if(symbol.is_static_lifetime) - out << " static_lifetime"; - if(symbol.is_thread_local) - out << " thread_local"; - if(symbol.is_file_local) - out << " file_local"; - if(symbol.is_type) - out << " type"; - if(symbol.is_extern) - out << " extern"; - if(symbol.is_input) - out << " input"; - if(symbol.is_output) - out << " output"; - if(symbol.is_macro) - out << " macro"; - if(symbol.is_parameter) - out << " parameter"; - if(symbol.is_auxiliary) - out << " auxiliary"; - if(symbol.is_weak) - out << " weak"; - if(symbol.is_property) - out << " property"; - if(symbol.is_state_var) - out << " state_var"; - if(symbol.is_exported) - out << " exported"; - if(symbol.is_volatile) - out << " volatile"; - - out << '\n'; - out << "Location....: " << symbol.location << '\n'; - - out << '\n' << std::flush; - } -} diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h deleted file mode 100644 index 35ebf0852d5..00000000000 --- a/src/langapi/language_ui.h +++ /dev/null @@ -1,60 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@cs.cmu.edu - -\*******************************************************************/ - - -#ifndef CPROVER_LANGAPI_LANGUAGE_UI_H -#define CPROVER_LANGAPI_LANGUAGE_UI_H - -#include -#include -#include - -#include "language_file.h" - -class cmdlinet; - -class language_uit:public messaget -{ -public: - language_filest language_files; - symbol_tablet symbol_table; - - language_uit( - const cmdlinet &cmdline, - ui_message_handlert &ui_message_handler, - optionst *options = nullptr); - virtual ~language_uit(); - - virtual bool parse(); - virtual bool parse(const std::string &filename); - virtual bool typecheck(); - virtual bool final(); - - virtual void clear_parse() - { - language_files.clear(); - } - - virtual void show_symbol_table(bool brief=false); - virtual void show_symbol_table_plain(std::ostream &out, bool brief); - virtual void show_symbol_table_xml_ui(bool brief); - - typedef ui_message_handlert::uit uit; - - uit get_ui() - { - return ui_message_handler.get_ui(); - } - -protected: - const cmdlinet &_cmdline; - ui_message_handlert &ui_message_handler; - optionst *options; -}; - -#endif // CPROVER_LANGAPI_LANGUAGE_UI_H diff --git a/unit/compound_block_locations.cpp b/unit/compound_block_locations.cpp index 1b1ce3e8e12..1365ab8e51e 100644 --- a/unit/compound_block_locations.cpp +++ b/unit/compound_block_locations.cpp @@ -21,7 +21,6 @@ Author: Kareem Khazem , 2018 #include -#include #include #include diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 3c37bdc60c0..2dbdf2c7afb 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -21,7 +21,6 @@ Author: Kareem Khazem , 2018 #include -#include #include #include