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 | add_files_from_archive (const std::string &file_name, bool thin_archive) |
extracts goto binaries from AR archive and add them as input files. 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... | |
bool | wrote_object_files () const |
Has this compiler written any object files? More... | |
void | cprover_macro_arities (std::map< irep_idt, std::size_t > &cprover_macros) const |
__CPROVER_... macros written to object files and their arities 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_executable |
std::string | output_file_object |
std::string | output_directory_object |
![]() | |
language_filest | language_files |
symbol_tablet | symbol_table |
Protected Member Functions | |
unsigned | function_body_count (const goto_functionst &) const |
void | add_compiler_specific_defines (class configt &config) const |
void | convert_symbols (goto_functionst &dest) |
bool | add_written_cprover_symbols (const symbol_tablet &symbol_table) |
Protected Attributes | |
cmdlinet & | cmdline |
bool | warning_is_fatal |
std::map< irep_idt, symbolt > | written_macros |
bool | wrote_object |
![]() | |
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 649 of file compile.cpp.
References COMPILE_LINK_EXECUTABLE, echo_file_name, get_current_working_directory(), mode, working_directory, and wrote_object.
compilet::~compilet | ( | ) |
cleans up temporary files
Definition at line 663 of file compile.cpp.
References delete_directory(), and tmp_dirs.
|
protected |
Definition at line 687 of file compile.cpp.
References configt::ansi_c, CBMC_VERSION, config, and configt::ansi_ct::defines.
Referenced by doit().
bool compilet::add_files_from_archive | ( | const std::string & | file_name, |
bool | thin_archive | ||
) |
extracts goto binaries from AR archive and add them as input files.
Definition at line 224 of file compile.cpp.
References concat_dir_file(), messaget::debug(), messaget::eom(), messaget::error(), get_temporary_directory(), is_goto_binary(), object_files, tmp_dirs, and working_directory.
Referenced by add_input_file().
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 184 of file compile.cpp.
References add_files_from_archive(), messaget::debug(), detect_file_type(), ELF_OBJECT, messaget::eom(), FAILED_TO_OPEN_FILE, GOTO_BINARY, NORMAL_ARCHIVE, object_files, SOURCE_FILE, source_files, THIN_ARCHIVE, UNKNOWN, UNREACHABLE, messaget::warning(), and warning_is_fatal.
Referenced by doit(), and find_library().
|
protected |
Definition at line 735 of file compile.cpp.
References CPROVER_PREFIX, messaget::eom(), messaget::error(), has_prefix(), irept::id(), id2string(), irept::pretty(), language_uit::symbol_table, symbol_table_baset::symbols, and written_macros.
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 386 of file compile.cpp.
References add_written_cprover_symbols(), ASSEMBLE_ONLY, goto_functionst::clear(), symbol_tablet::clear(), cmdline, COMPILE_ONLY, compiled_functions, concat_dir_file(), convert_symbols(), echo_file_name, messaget::eom(), get_base_name(), cmdlinet::get_value(), mode, object_file_extension, output_directory_object, output_file_object, parse_source(), r, source_files, language_uit::symbol_table, messaget::warning(), and write_object_file().
Referenced by doit().
|
protected |
Definition at line 693 of file compile.cpp.
References goto_convert_functionst::convert_function(), messaget::debug(), messaget::eom(), goto_functionst::function_map, messaget::get_message_handler(), symbol_table_baset::get_writeable_ref(), size_type(), language_uit::symbol_table, symbol_table_baset::symbols, and symbolt::value.
|
inline |
__CPROVER_...
macros written to object files and their arities
__CPROVER
macro that this compiler wrote to one or more object files, to how many parameters that __CPROVER
macro has. Definition at line 87 of file compile.h.
References code_typet::parameters(), PRECONDITION, to_code_type(), written_macros, and wrote_object.
Referenced by gcc_modet::run_gcc().
bool compilet::doit | ( | ) |
reads and source and object files, compiles and links them into goto program objects.
Definition at line 70 of file compile.cpp.
References language_uit::_cmdline, add_compiler_specific_defines(), add_input_file(), cmdlinet::args, goto_functionst::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 300 of file compile.cpp.
References add_input_file(), detect_file_type(), ELF_OBJECT, messaget::eom(), GOTO_BINARY, library_paths, messaget::warning(), and warning_is_fatal.
Referenced by doit().
|
protected |
Definition at line 673 of file compile.cpp.
References goto_functionst::function_map.
Referenced by write_bin_object_file().
bool compilet::link | ( | ) |
parses object files and links them
Definition at line 343 of file compile.cpp.
References add_written_cprover_symbols(), ansi_c_entry_point(), COMPILE_LINK_EXECUTABLE, compiled_functions, convert_symbols(), goto_functionst::entry_point(), messaget::eom(), goto_functionst::function_map, messaget::get_message_handler(), INITIALIZE_FUNCTION, mode, object_files, output_file_executable, read_object_and_link(), symbol_table_baset::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 453 of file compile.cpp.
References language_filest::add_file(), cmdline, messaget::eom(), messaget::error(), 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, parse_stdin(), ui_message_handlert::PLAIN, 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 629 of file compile.cpp.
References has_suffix(), language_uit::language_files, language_uit::parse(), language_filest::remove_file(), and language_uit::typecheck().
Referenced by compile().
bool compilet::parse_stdin | ( | ) |
parses a source file (low-level parsing)
Definition at line 536 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 593 of file compile.cpp.
References messaget::eom(), messaget::error(), function_body_count(), goto_functionst::function_map, messaget::statistics(), symbol_table_baset::symbols, write_goto_binary(), and wrote_object.
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 581 of file compile.cpp.
References write_bin_object_file().
Referenced by linker_script_merget::add_linker_script_definitions(), compile(), and link().
|
inline |
Has this compiler written any object files?
Definition at line 80 of file compile.h.
References wrote_object.
Referenced by gcc_modet::run_gcc().
|
protected |
Definition at line 97 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(), 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_files_from_archive(), add_input_file(), doit(), and link().
std::string compilet::output_directory_object |
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_files_from_archive(), and ~compilet().
|
protected |
Definition at line 98 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_files_from_archive(), and compilet().
Definition at line 107 of file compile.h.
Referenced by add_written_cprover_symbols(), and cprover_macro_arities().
|
protected |
Definition at line 114 of file compile.h.
Referenced by compilet(), cprover_macro_arities(), write_bin_object_file(), and wrote_object_files().