cprover
|
#include <compile.h>
Public Types | |
enum | { PREPROCESS_ONLY, COMPILE_ONLY, ASSEMBLE_ONLY, LINK_LIBRARY, COMPILE_LINK, COMPILE_LINK_EXECUTABLE } |
![]() | |
typedef ui_message_handlert::uit | uit |
Public Member Functions | |
compilet (cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror) | |
constructor More... | |
~compilet () | |
cleans up temporary files More... | |
bool | add_input_file (const std::string &) |
puts input file names into a list and does preprocessing for libraries. More... | |
bool | find_library (const std::string &) |
tries to find a library object file that matches the given library name. More... | |
bool | is_elf_file (const std::string &) |
checking if we can load an object file More... | |
bool | parse (const std::string &filename) |
parses a source file (low-level parsing) More... | |
bool | parse_stdin () |
parses a source file (low-level parsing) More... | |
bool | doit () |
reads and source and object files, compiles and links them into goto program objects. More... | |
bool | compile () |
parses source files and writes object files, or keeps the symbols in the symbol_table depending on the doLink flag. More... | |
bool | link () |
parses object files and links them More... | |
bool | parse_source (const std::string &) |
parses a source file More... | |
bool | write_object_file (const std::string &, const symbol_tablet &, goto_functionst &) |
writes the goto functions in the function table to a binary format object file. More... | |
bool | write_bin_object_file (const std::string &, const symbol_tablet &, goto_functionst &) |
writes the goto functions in the function table to a binary format object file. More... | |
![]() | |
language_uit (const cmdlinet &cmdline, ui_message_handlert &ui_message_handler) | |
Constructor. More... | |
virtual | ~language_uit () |
Destructor. More... | |
virtual bool | parse () |
virtual bool | typecheck () |
virtual bool | final () |
virtual void | clear_parse () |
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) |
uit | get_ui () |
Public Attributes | |
namespacet | ns |
goto_functionst | compiled_functions |
bool | echo_file_name |
std::string | working_directory |
std::string | override_language |
enum compilet:: { ... } | mode |
std::list< std::string > | library_paths |
std::list< std::string > | source_files |
std::list< std::string > | object_files |
std::list< std::string > | libraries |
std::list< std::string > | tmp_dirs |
std::list< irep_idt > | seen_modes |
std::string | object_file_extension |
std::string | output_file_object |
std::string | output_file_executable |
![]() | |
language_filest | language_files |
symbol_tablet | symbol_table |
Protected Member Functions | |
unsigned | function_body_count (const goto_functionst &) |
void | add_compiler_specific_defines (class configt &config) const |
void | convert_symbols (goto_functionst &dest) |
Protected Attributes | |
cmdlinet & | cmdline |
bool | warning_is_fatal |
![]() | |
const cmdlinet & | _cmdline |
ui_message_handlert & | ui_message_handler |
Additional Inherited Members |
anonymous enum |
compilet::compilet | ( | cmdlinet & | _cmdline, |
ui_message_handlert & | mh, | ||
bool | Werror | ||
) |
constructor
Definition at line 646 of file compile.cpp.
References COMPILE_LINK_EXECUTABLE, echo_file_name, get_current_working_directory(), mode, and working_directory.
compilet::~compilet | ( | ) |
cleans up temporary files
Definition at line 659 of file compile.cpp.
References delete_directory(), and tmp_dirs.
|
protected |
Definition at line 683 of file compile.cpp.
References configt::ansi_c, CBMC_VERSION, config, and configt::ansi_ct::defines.
Referenced by doit().
bool compilet::add_input_file | ( | const std::string & | file_name | ) |
puts input file names into a list and does preprocessing for libraries.
Definition at line 140 of file compile.cpp.
References concat_dir_file(), messaget::eom(), messaget::error(), get_temporary_directory(), is_goto_binary(), object_files, r, source_files, tmp_dirs, messaget::warning(), warning_is_fatal, and working_directory.
Referenced by doit(), and find_library().
bool compilet::compile | ( | ) |
parses source files and writes object files, or keeps the symbols in the symbol_table depending on the doLink flag.
Definition at line 388 of file compile.cpp.
References ASSEMBLE_ONLY, symbol_tablet::clear(), goto_functions_templatet< bodyT >::clear(), cmdline, COMPILE_ONLY, compiled_functions, convert_symbols(), echo_file_name, messaget::eom(), get_base_name(), cmdlinet::get_value(), mode, object_file_extension, output_file_object, parse_source(), r, source_files, messaget::status(), language_uit::symbol_table, messaget::warning(), and write_object_file().
Referenced by doit().
|
protected |
Definition at line 688 of file compile.cpp.
References goto_convert_functionst::convert_function(), messaget::debug(), messaget::eom(), Forall_symbols, messaget::get_message_handler(), size_type(), language_uit::symbol_table, and symbol_tablet::symbols.
bool compilet::doit | ( | ) |
reads and source and object files, compiles and links them into goto program objects.
Definition at line 74 of file compile.cpp.
References language_uit::_cmdline, add_compiler_specific_defines(), add_input_file(), cmdlinet::args, goto_functions_templatet< bodyT >::clear(), compile(), COMPILE_LINK, COMPILE_LINK_EXECUTABLE, compiled_functions, config, messaget::debug(), messaget::eom(), messaget::error(), find_library(), message_handlert::get_message_count(), messaget::get_message_handler(), libraries, link(), LINK_LIBRARY, messaget::M_WARNING, mode, object_files, PREPROCESS_ONLY, source_files, messaget::statistics(), and warning_is_fatal.
bool compilet::find_library | ( | const std::string & | name | ) |
tries to find a library object file that matches the given library name.
Definition at line 282 of file compile.cpp.
References add_input_file(), messaget::eom(), is_elf_file(), is_goto_binary(), library_paths, messaget::warning(), and warning_is_fatal.
Referenced by doit().
|
protected |
Definition at line 669 of file compile.cpp.
References goto_functions_templatet< bodyT >::function_map.
Referenced by write_bin_object_file().
bool compilet::is_elf_file | ( | const std::string & | file_name | ) |
checking if we can load an object file
Definition at line 322 of file compile.cpp.
Referenced by find_library().
bool compilet::link | ( | ) |
parses object files and links them
Definition at line 342 of file compile.cpp.
References ansi_c_entry_point(), COMPILE_LINK_EXECUTABLE, compiled_functions, convert_symbols(), goto_functions_templatet< goto_programt >::entry_point(), messaget::eom(), goto_functions_templatet< bodyT >::function_map, messaget::get_message_handler(), mode, object_files, output_file_executable, read_object_and_link(), symbol_tablet::remove(), messaget::statistics(), language_uit::symbol_table, and write_object_file().
Referenced by doit().
|
virtual |
parses a source file (low-level parsing)
Reimplemented from language_uit.
Definition at line 443 of file compile.cpp.
References cmdline, messaget::eom(), messaget::error(), language_filest::file_map, language_filet::filename, get_language_from_filename(), get_language_from_mode(), messaget::get_message_handler(), language_filet::get_modules(), language_uit::get_ui(), cmdlinet::get_value(), cmdlinet::isset(), language_filet::language, language_uit::language_files, mode, override_language, languaget::parse(), parse_stdin(), ui_message_handlert::PLAIN, languaget::preprocess(), PREPROCESS_ONLY, messaget::set_message_handler(), messaget::statistics(), and widen().
bool compilet::parse_source | ( | const std::string & | file_name | ) |
parses a source file
Definition at line 626 of file compile.cpp.
References language_filest::file_map, has_suffix(), language_uit::language_files, language_uit::parse(), and language_uit::typecheck().
Referenced by compile().
bool compilet::parse_stdin | ( | ) |
parses a source file (low-level parsing)
Definition at line 534 of file compile.cpp.
References cmdline, messaget::eom(), messaget::error(), messaget::get_message_handler(), language_uit::get_ui(), cmdlinet::get_value(), cmdlinet::isset(), mode, ansi_c_languaget::parse(), ui_message_handlert::PLAIN, ansi_c_languaget::preprocess(), PREPROCESS_ONLY, messaget::set_message_handler(), and messaget::statistics().
Referenced by parse().
bool compilet::write_bin_object_file | ( | const std::string & | file_name, |
const symbol_tablet & | lsymbol_table, | ||
goto_functionst & | functions | ||
) |
writes the goto functions in the function table to a binary format object file.
Definition at line 591 of file compile.cpp.
References messaget::eom(), messaget::error(), function_body_count(), goto_functions_templatet< bodyT >::function_map, messaget::statistics(), symbol_tablet::symbols, and write_goto_binary().
Referenced by write_object_file().
bool compilet::write_object_file | ( | const std::string & | file_name, |
const symbol_tablet & | lsymbol_table, | ||
goto_functionst & | functions | ||
) |
writes the goto functions in the function table to a binary format object file.
Definition at line 579 of file compile.cpp.
References write_bin_object_file().
|
protected |
Definition at line 76 of file compile.h.
Referenced by compile(), parse(), and parse_stdin().
goto_functionst compilet::compiled_functions |
bool compilet::echo_file_name |
Definition at line 28 of file compile.h.
Referenced by compile(), and compilet().
std::list<std::string> compilet::libraries |
std::list<std::string> compilet::library_paths |
Definition at line 40 of file compile.h.
Referenced by find_library().
enum { ... } compilet::mode |
Referenced by compile(), compilet(), as_modet::doit(), gcc_modet::doit(), doit(), link(), parse(), and parse_stdin().
namespacet compilet::ns |
std::string compilet::object_file_extension |
std::list<std::string> compilet::object_files |
Definition at line 42 of file compile.h.
Referenced by add_input_file(), doit(), and link().
std::string compilet::output_file_executable |
std::string compilet::output_file_object |
std::string compilet::override_language |
std::list<std::string> compilet::source_files |
Definition at line 41 of file compile.h.
Referenced by add_input_file(), compile(), and doit().
std::list<std::string> compilet::tmp_dirs |
Definition at line 44 of file compile.h.
Referenced by add_input_file(), and ~compilet().
|
protected |
Definition at line 77 of file compile.h.
Referenced by add_input_file(), doit(), and find_library().
std::string compilet::working_directory |
Definition at line 29 of file compile.h.
Referenced by add_input_file(), and compilet().