#include <compile.h>
Definition at line 31 of file compile.h.
◆ anonymous enum
| Enumerator |
|---|
| PREPROCESS_ONLY | |
| COMPILE_ONLY | |
| ASSEMBLE_ONLY | |
| LINK_LIBRARY | |
| COMPILE_LINK | |
| COMPILE_LINK_EXECUTABLE | |
Definition at line 38 of file compile.h.
◆ compilet()
◆ ~compilet()
◆ add_compiler_specific_defines()
| void compilet::add_compiler_specific_defines |
( |
| ) |
const |
|
protected |
◆ add_files_from_archive()
| 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.
- Returns
- false on success, true on error.
Definition at line 208 of file compile.cpp.
◆ 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.
- Returns
- false on success, true on error.
Definition at line 167 of file compile.cpp.
◆ add_written_cprover_symbols()
| bool compilet::add_written_cprover_symbols |
( |
const symbol_tablet & |
symbol_table | ) |
|
|
protected |
◆ compile()
Parses source files and writes object files, or keeps the symbols in the symbol_table if not compiling/assembling only.
- Returns
- Symbol table, if parsing and type checking succeeded, else empty
Definition at line 371 of file compile.cpp.
◆ convert_symbols()
| void compilet::convert_symbols |
( |
goto_modelt & |
goto_model | ) |
|
|
protected |
◆ cprover_macro_arities()
| void compilet::cprover_macro_arities |
( |
std::map< irep_idt, std::size_t > & |
cprover_macros | ) |
const |
|
inline |
__CPROVER_... macros written to object files and their arities
- Parameters
-
| [out] | cprover_macros | A mapping from every __CPROVER macro that this compiler wrote to one or more object files, to how many parameters that __CPROVER macro has. |
Definition at line 94 of file compile.h.
◆ doit()
reads and source and object files, compiles and links them into goto program objects.
- Returns
- true on error, false otherwise
Definition at line 54 of file compile.cpp.
◆ find_library()
| bool compilet::find_library |
( |
const std::string & |
name | ) |
|
tries to find a library object file that matches the given library name.
- parameters: library name
- Returns
- true if found, false otherwise
Definition at line 273 of file compile.cpp.
◆ function_body_count()
| std::size_t compilet::function_body_count |
( |
const goto_functionst & |
functions | ) |
|
|
staticprotected |
◆ link()
| bool compilet::link |
( |
std::optional< symbol_tablet > && |
symbol_table | ) |
|
parses object files and links them
- Returns
- true on error, false otherwise
Definition at line 317 of file compile.cpp.
◆ parse()
| bool compilet::parse |
( |
const std::string & |
file_name, |
|
|
language_filest & |
language_files |
|
) |
| |
parses a source file (low-level parsing)
- Returns
- true on error, false otherwise
Definition at line 457 of file compile.cpp.
◆ parse_source()
| std::optional< symbol_tablet > compilet::parse_source |
( |
const std::string & |
file_name | ) |
|
Parses and type checks a source file located at file_name.
- Returns
- A symbol table if, and only if, parsing and type checking succeeded.
Definition at line 621 of file compile.cpp.
◆ parse_stdin()
| bool compilet::parse_stdin |
( |
languaget & |
language | ) |
|
parses a source file (low-level parsing)
- Parameters
-
| language | source language processor |
- Returns
- true on error, false otherwise
Definition at line 538 of file compile.cpp.
◆ write_bin_object_file() [1/2]
| bool compilet::write_bin_object_file |
( |
const std::string & |
file_name, |
|
|
const goto_modelt & |
src_goto_model |
|
) |
| |
|
inlineprotected |
◆ write_bin_object_file() [2/2]
| bool compilet::write_bin_object_file |
( |
const std::string & |
file_name, |
|
|
const goto_modelt & |
src_goto_model, |
|
|
bool |
validate_goto_model, |
|
|
message_handlert & |
message_handler |
|
) |
| |
|
static |
Writes the goto functions of src_goto_model to a binary format object file.
- Parameters
-
| file_name | Target file to serialize src_goto_model to |
| src_goto_model | goto model to serialize |
| validate_goto_model | enable goto-model validation |
| message_handler | message handler |
- Returns
- true on error, false otherwise
Definition at line 574 of file compile.cpp.
◆ wrote_object_files()
| bool compilet::wrote_object_files |
( |
| ) |
const |
|
inline |
Has this compiler written any object files?
Definition at line 87 of file compile.h.
◆ cmdline
◆ echo_file_name
| bool compilet::echo_file_name |
◆ file_local_mangle_suffix
| const std::string compilet::file_local_mangle_suffix |
|
protected |
String to include in all mangled names.
Definition at line 118 of file compile.h.
◆ keep_file_local
| const bool compilet::keep_file_local |
|
protected |
Whether to keep implementations of file-local symbols.
Definition at line 115 of file compile.h.
◆ libraries
| std::list<std::string> compilet::libraries |
◆ library_paths
| std::list<std::string> compilet::library_paths |
◆ log
| enum { ... } compilet::mode |
◆ object_file_extension
| std::string compilet::object_file_extension |
◆ object_files
| std::list<std::string> compilet::object_files |
◆ output_directory_object
| std::string compilet::output_directory_object |
◆ output_file_executable
| std::string compilet::output_file_executable |
◆ output_file_object
| std::string compilet::output_file_object |
◆ override_language
| std::string compilet::override_language |
|
protected |
◆ seen_modes
| std::list<irep_idt> compilet::seen_modes |
|
protected |
◆ source_files
| std::list<std::string> compilet::source_files |
◆ tmp_dirs
| std::list<std::string> compilet::tmp_dirs |
|
protected |
◆ validate_goto_model
| bool compilet::validate_goto_model = false |
◆ warning_is_fatal
| bool compilet::warning_is_fatal |
|
protected |
◆ working_directory
| std::string compilet::working_directory |
|
protected |
◆ written_macros
◆ wrote_object
| bool compilet::wrote_object |
|
protected |
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/goto-cc/compile.h
- /home/runner/work/cbmc/cbmc/src/goto-cc/compile.cpp
Collaboration diagram for compilet: