cprover
compilet Class Reference

#include <compile.h>

Inheritance diagram for compilet:
[legend]
Collaboration diagram for compilet:
[legend]

Public Types

enum  {
  PREPROCESS_ONLY, COMPILE_ONLY, ASSEMBLE_ONLY, LINK_LIBRARY,
  COMPILE_LINK, COMPILE_LINK_EXECUTABLE
}
 
- Public Types inherited from language_uit
typedef ui_message_handlert::uit uit
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

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...
 
- Public Member Functions inherited from language_uit
 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 Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

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_idtseen_modes
 
std::string object_file_extension
 
std::string output_file_object
 
std::string output_file_executable
 
- Public Attributes inherited from language_uit
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

cmdlinetcmdline
 
bool warning_is_fatal
 
std::map< irep_idt, symboltwritten_macros
 
bool wrote_object
 
- Protected Attributes inherited from language_uit
const cmdlinet_cmdline
 
ui_message_handlertui_message_handler
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 23 of file compile.h.

Member Enumeration Documentation

◆ anonymous enum

anonymous enum
Enumerator
PREPROCESS_ONLY 
COMPILE_ONLY 
ASSEMBLE_ONLY 
LINK_LIBRARY 
COMPILE_LINK 
COMPILE_LINK_EXECUTABLE 

Definition at line 32 of file compile.h.

Constructor & Destructor Documentation

◆ compilet()

compilet::compilet ( cmdlinet _cmdline,
ui_message_handlert mh,
bool  Werror 
)

constructor

Returns
nothing

Definition at line 639 of file compile.cpp.

References COMPILE_LINK_EXECUTABLE, echo_file_name, get_current_working_directory(), mode, working_directory, and wrote_object.

◆ ~compilet()

compilet::~compilet ( )

cleans up temporary files

Returns
nothing

Definition at line 653 of file compile.cpp.

References delete_directory(), and tmp_dirs.

Member Function Documentation

◆ add_compiler_specific_defines()

void compilet::add_compiler_specific_defines ( class configt config) const
protected

Definition at line 677 of file compile.cpp.

References configt::ansi_c, config, and configt::ansi_ct::defines.

Referenced by doit().

◆ 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 223 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().

◆ 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 183 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().

◆ add_written_cprover_symbols()

bool compilet::add_written_cprover_symbols ( const symbol_tablet symbol_table)
protected

◆ compile()

bool compilet::compile ( )

parses source files and writes object files, or keeps the symbols in the symbol_table depending on the doLink flag.

Returns
true on error, false otherwise

Definition at line 385 of file compile.cpp.

References add_written_cprover_symbols(), ASSEMBLE_ONLY, goto_functionst::clear(), symbol_tablet::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().

◆ convert_symbols()

◆ 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

Returns
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 84 of file compile.h.

References code_typet::parameters(), PRECONDITION, to_code_type(), written_macros, and wrote_object.

Referenced by gcc_modet::run_gcc().

◆ doit()

◆ 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 299 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().

◆ function_body_count()

unsigned compilet::function_body_count ( const goto_functionst functions) const
protected

Definition at line 663 of file compile.cpp.

References goto_functionst::function_map.

Referenced by write_bin_object_file().

◆ link()

◆ parse()

◆ parse_source()

bool compilet::parse_source ( const std::string &  file_name)

parses a source file

Returns
true on error, false otherwise

Definition at line 619 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().

◆ parse_stdin()

◆ write_bin_object_file()

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.

parameters: file_name, functions table
Returns
true on error, false otherwise

Definition at line 583 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().

◆ 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.

parameters: file_name, functions table
Returns
true on error, false otherwise

Definition at line 571 of file compile.cpp.

References write_bin_object_file().

Referenced by linker_script_merget::add_linker_script_definitions(), compile(), and link().

◆ wrote_object_files()

bool compilet::wrote_object_files ( ) const
inline

Has this compiler written any object files?

Definition at line 77 of file compile.h.

References wrote_object.

Referenced by gcc_modet::run_gcc().

Member Data Documentation

◆ cmdline

cmdlinet& compilet::cmdline
protected

Definition at line 94 of file compile.h.

Referenced by compile(), parse(), and parse_stdin().

◆ compiled_functions

goto_functionst compilet::compiled_functions

Definition at line 27 of file compile.h.

Referenced by compile(), doit(), and link().

◆ echo_file_name

bool compilet::echo_file_name

Definition at line 28 of file compile.h.

Referenced by compile(), and compilet().

◆ libraries

std::list<std::string> compilet::libraries

Definition at line 43 of file compile.h.

Referenced by doit().

◆ library_paths

std::list<std::string> compilet::library_paths

Definition at line 40 of file compile.h.

Referenced by find_library().

◆ mode

enum { ... } compilet::mode

◆ ns

namespacet compilet::ns

Definition at line 26 of file compile.h.

◆ object_file_extension

std::string compilet::object_file_extension

Definition at line 47 of file compile.h.

Referenced by compile().

◆ object_files

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().

◆ output_file_executable

std::string compilet::output_file_executable

Definition at line 48 of file compile.h.

Referenced by link().

◆ output_file_object

std::string compilet::output_file_object

Definition at line 48 of file compile.h.

Referenced by compile().

◆ override_language

std::string compilet::override_language

Definition at line 30 of file compile.h.

Referenced by parse().

◆ seen_modes

std::list<irep_idt> compilet::seen_modes

Definition at line 45 of file compile.h.

◆ source_files

std::list<std::string> compilet::source_files

Definition at line 41 of file compile.h.

Referenced by add_input_file(), compile(), and doit().

◆ tmp_dirs

std::list<std::string> compilet::tmp_dirs

Definition at line 44 of file compile.h.

Referenced by add_files_from_archive(), and ~compilet().

◆ warning_is_fatal

bool compilet::warning_is_fatal
protected

Definition at line 95 of file compile.h.

Referenced by add_input_file(), doit(), and find_library().

◆ working_directory

std::string compilet::working_directory

Definition at line 29 of file compile.h.

Referenced by add_files_from_archive(), and compilet().

◆ written_macros

std::map<irep_idt, symbolt> compilet::written_macros
protected

Definition at line 104 of file compile.h.

Referenced by add_written_cprover_symbols(), and cprover_macro_arities().

◆ wrote_object

bool compilet::wrote_object
protected

The documentation for this class was generated from the following files: