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 is_elf_file (const std::string &)
 checking if we can load an object file 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...
 
- 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)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

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 &)
 
void add_compiler_specific_defines (class configt &config) const
 
void convert_symbols (goto_functionst &dest)
 

Protected Attributes

cmdlinetcmdline
 
bool warning_is_fatal
 
- 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 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 646 of file compile.cpp.

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

◆ ~compilet()

compilet::~compilet ( )

cleans up temporary files

Returns
nothing

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

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

Referenced by doit().

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

References concat_dir_file(), messaget::eom(), messaget::error(), get_temporary_directory(), is_goto_binary(), object_files, r, source_files, tmp_dirs, messaget::warning(), warning_is_fatal, and working_directory.

Referenced by doit(), and find_library().

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

References ASSEMBLE_ONLY, symbol_tablet::clear(), goto_functions_templatet< bodyT >::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()

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

References add_input_file(), messaget::eom(), is_elf_file(), is_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)
protected

Definition at line 669 of file compile.cpp.

References goto_functions_templatet< bodyT >::function_map.

Referenced by write_bin_object_file().

◆ is_elf_file()

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

checking if we can load an object file

parameters: file name
Returns
true if the given file name exists and is an ELF file, false otherwise

Definition at line 322 of file compile.cpp.

Referenced by find_library().

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

References language_filest::file_map, has_suffix(), language_uit::language_files, language_uit::parse(), 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 591 of file compile.cpp.

References messaget::eom(), messaget::error(), function_body_count(), goto_functions_templatet< bodyT >::function_map, messaget::statistics(), symbol_tablet::symbols, and write_goto_binary().

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

References write_bin_object_file().

Referenced by compile(), and link().

Member Data Documentation

◆ cmdline

cmdlinet& compilet::cmdline
protected

Definition at line 76 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_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_input_file(), and ~compilet().

◆ warning_is_fatal

bool compilet::warning_is_fatal
protected

Definition at line 77 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_input_file(), and compilet().


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