cprover
compilet Class Reference

#include <compile.h>

+ Inheritance diagram for compilet:
+ Collaboration diagram for compilet:

Public Types

enum  {
  PREPROCESS_ONLY, COMPILE_ONLY, ASSEMBLE_ONLY, LINK_LIBRARY,
  COMPILE_LINK, COMPILE_LINK_EXECUTABLE
}
 
- 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, 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 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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. 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_idtseen_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

cmdlinetcmdline
 
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, symboltwritten_macros
 
bool wrote_object
 
- 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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Definition at line 26 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 39 of file compile.h.

Constructor & Destructor Documentation

◆ compilet()

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

constructor

Returns
nothing

Definition at line 631 of file compile.cpp.

◆ ~compilet()

compilet::~compilet ( )

cleans up temporary files

Returns
nothing

Definition at line 656 of file compile.cpp.

Member Function Documentation

◆ add_compiler_specific_defines()

void compilet::add_compiler_specific_defines ( ) const
protected

Definition at line 676 of file compile.cpp.

◆ 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 211 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 171 of file compile.cpp.

◆ add_written_cprover_symbols()

bool compilet::add_written_cprover_symbols ( const symbol_tablet symbol_table)
protected

Definition at line 723 of file compile.cpp.

◆ 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 365 of file compile.cpp.

◆ convert_symbols()

void compilet::convert_symbols ( goto_functionst dest)
protected

Definition at line 682 of file compile.cpp.

◆ 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 86 of file compile.h.

◆ doit()

bool compilet::doit ( )

reads and source and object files, compiles and links them into goto program objects.

Returns
true on error, false otherwise

Definition at line 57 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 270 of file compile.cpp.

◆ function_body_count()

std::size_t compilet::function_body_count ( const goto_functionst functions) const
protected

Definition at line 665 of file compile.cpp.

◆ link()

bool compilet::link ( )

parses object files and links them

Returns
true on error, false otherwise

Definition at line 311 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 438 of file compile.cpp.

◆ parse_source()

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

parses a source file

Returns
true on error, false otherwise

Definition at line 605 of file compile.cpp.

◆ parse_stdin()

bool compilet::parse_stdin ( languaget language)

parses a source file (low-level parsing)

Parameters
languagesource language processor
Returns
true on error, false otherwise

Definition at line 523 of file compile.cpp.

◆ write_bin_object_file()

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.

Parameters
file_nameTarget file to serialize src_goto_model to
src_goto_modelgoto model to serialize
Returns
true on error, false otherwise

Definition at line 564 of file compile.cpp.

◆ wrote_object_files()

bool compilet::wrote_object_files ( ) const
inline

Has this compiler written any object files?

Definition at line 79 of file compile.h.

Member Data Documentation

◆ cmdline

cmdlinet& compilet::cmdline
protected

Definition at line 96 of file compile.h.

◆ echo_file_name

bool compilet::echo_file_name

Definition at line 34 of file compile.h.

◆ file_local_mangle_suffix

const std::string compilet::file_local_mangle_suffix
protected

String to include in all mangled names.

Definition at line 103 of file compile.h.

◆ goto_model

goto_modelt compilet::goto_model

Definition at line 31 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 100 of file compile.h.

◆ libraries

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

Definition at line 50 of file compile.h.

◆ library_paths

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

Definition at line 47 of file compile.h.

◆ mode

enum { ... } compilet::mode

◆ ns

namespacet compilet::ns

Definition at line 30 of file compile.h.

◆ object_file_extension

std::string compilet::object_file_extension

Definition at line 54 of file compile.h.

◆ object_files

std::list<std::string> compilet::object_files

Definition at line 49 of file compile.h.

◆ output_directory_object

std::string compilet::output_directory_object

Definition at line 58 of file compile.h.

◆ output_file_executable

std::string compilet::output_file_executable

Definition at line 55 of file compile.h.

◆ output_file_object

std::string compilet::output_file_object

Definition at line 58 of file compile.h.

◆ override_language

std::string compilet::override_language

Definition at line 36 of file compile.h.

◆ seen_modes

std::list<irep_idt> compilet::seen_modes

Definition at line 52 of file compile.h.

◆ source_files

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

Definition at line 48 of file compile.h.

◆ tmp_dirs

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

Definition at line 51 of file compile.h.

◆ validate_goto_model

bool compilet::validate_goto_model = false

Definition at line 37 of file compile.h.

◆ warning_is_fatal

bool compilet::warning_is_fatal
protected

Definition at line 97 of file compile.h.

◆ working_directory

std::string compilet::working_directory

Definition at line 35 of file compile.h.

◆ written_macros

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

Definition at line 112 of file compile.h.

◆ wrote_object

bool compilet::wrote_object
protected

Definition at line 119 of file compile.h.


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