cprover
|
#include <compile.h>
Public Types | |
enum | { PREPROCESS_ONLY, COMPILE_ONLY, ASSEMBLE_ONLY, LINK_LIBRARY, COMPILE_LINK, COMPILE_LINK_EXECUTABLE } |
Public Member Functions | |
compilet (cmdlinet &_cmdline, 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, language_filest &) |
parses a source file (low-level parsing) More... | |
bool | parse_stdin (languaget &) |
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_bin_object_file (const std::string &, const goto_modelt &) |
Writes the goto functions of src_goto_model 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... | |
Public Attributes | |
namespacet | ns |
goto_modelt | goto_model |
bool | echo_file_name |
std::string | working_directory |
std::string | override_language |
bool | validate_goto_model = false |
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 |
Protected Member Functions | |
std::size_t | function_body_count (const goto_functionst &) const |
void | add_compiler_specific_defines () 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 |
const bool | keep_file_local |
Whether to keep implementations of file-local symbols. More... | |
const std::string | file_local_mangle_suffix |
String to include in all mangled names. More... | |
std::map< irep_idt, symbolt > | written_macros |
bool | wrote_object |
Additional Inherited Members |
anonymous enum |
compilet::compilet | ( | cmdlinet & | _cmdline, |
message_handlert & | mh, | ||
bool | Werror | ||
) |
compilet::~compilet | ( | ) |
|
protected |
Definition at line 676 of file compile.cpp.
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 211 of file compile.cpp.
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 171 of file compile.cpp.
|
protected |
Definition at line 723 of file compile.cpp.
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 365 of file compile.cpp.
|
protected |
Definition at line 682 of file compile.cpp.
|
inline |
bool compilet::doit | ( | ) |
reads and source and object files, compiles and links them into goto program objects.
Definition at line 57 of file compile.cpp.
bool compilet::find_library | ( | const std::string & | name | ) |
tries to find a library object file that matches the given library name.
Definition at line 270 of file compile.cpp.
|
protected |
Definition at line 665 of file compile.cpp.
bool compilet::link | ( | ) |
parses object files and links them
Definition at line 311 of file compile.cpp.
bool compilet::parse | ( | const std::string & | file_name, |
language_filest & | language_files | ||
) |
parses a source file (low-level parsing)
Definition at line 438 of file compile.cpp.
bool compilet::parse_source | ( | const std::string & | file_name | ) |
parses a source file
Definition at line 605 of file compile.cpp.
bool compilet::parse_stdin | ( | languaget & | language | ) |
parses a source file (low-level parsing)
language | source language processor |
Definition at line 523 of file compile.cpp.
bool compilet::write_bin_object_file | ( | const std::string & | file_name, |
const goto_modelt & | src_goto_model | ||
) |
Writes the goto functions of src_goto_model
to a binary format object file.
file_name | Target file to serialize src_goto_model to |
src_goto_model | goto model to serialize |
Definition at line 564 of file compile.cpp.
|
inline |
|
protected |
goto_modelt compilet::goto_model |
|
protected |
enum { ... } compilet::mode |
namespacet compilet::ns |