Go to the documentation of this file.
14 #ifndef CPROVER_GOTO_CC_COMPILE_H
15 #define CPROVER_GOTO_CC_COMPILE_H
87 std::size_t> &cprover_macros)
const
91 cprover_macros.insert({pair.first,
122 #endif // CPROVER_GOTO_CC_COMPILE_H
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::list< std::string > source_files
bool parse(const std::string &filename, language_filest &)
parses a source file (low-level parsing)
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.
bool parse_stdin(languaget &)
parses a source file (low-level parsing)
std::size_t function_body_count(const goto_functionst &) const
bool doit()
reads and source and object files, compiles and links them into goto program objects.
std::list< std::string > libraries
bool wrote_object_files() const
Has this compiler written any object files?
void add_compiler_specific_defines() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool link()
parses object files and links them
std::map< irep_idt, symbolt > written_macros
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
std::string output_file_object
std::list< std::string > object_files
bool add_written_cprover_symbols(const symbol_tablet &symbol_table)
std::string working_directory
const std::string file_local_mangle_suffix
String to include in all mangled names.
compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
constructor
std::string output_file_executable
#define PRECONDITION(CONDITION)
void convert_symbols(goto_functionst &dest)
std::list< std::string > library_paths
std::string object_file_extension
~compilet()
cleans up temporary files
@ COMPILE_LINK_EXECUTABLE
const parameterst & parameters() const
std::string override_language
bool add_input_file(const std::string &)
puts input file names into a list and does preprocessing for libraries.
std::string output_directory_object
bool find_library(const std::string &)
tries to find a library object file that matches the given library name.
const bool keep_file_local
Whether to keep implementations of file-local symbols.
A collection of goto functions.
bool compile()
parses source files and writes object files, or keeps the symbols in the symbol_table depending on th...
bool parse_source(const std::string &)
parses a source file
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.
std::list< irep_idt > seen_modes
std::list< std::string > tmp_dirs
void cprover_macro_arities(std::map< irep_idt, std::size_t > &cprover_macros) const
__CPROVER_... macros written to object files and their arities