#include <compile.h>

Collaboration diagram for compilet:

Public Types
enum	{ PREPROCESS_ONLY , COMPILE_ONLY , ASSEMBLE_ONLY , LINK_LIBRARY , COMPILE_LINK , COMPILE_LINK_EXECUTABLE }

Public Member Functions
	compilet (cmdlinet &_cmdline, message_handlert &mh, bool Werror)
	constructor
	~compilet ()
	cleans up temporary files
bool	add_input_file (const std::string &)
	puts input file names into a list and does preprocessing for libraries.
bool	find_library (const std::string &)
	tries to find a library object file that matches the given library name.
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 (const std::string &filename, language_filest &)
	parses a source file (low-level parsing)
bool	parse_stdin (languaget &)
	parses a source file (low-level parsing)
bool	doit ()
	reads and source and object files, compiles and links them into goto program objects.
std::optional< symbol_tablet >	compile ()
	Parses source files and writes object files, or keeps the symbols in the symbol_table if not compiling/assembling only.
bool	link (std::optional< symbol_tablet > &&symbol_table)
	parses object files and links them
std::optional< symbol_tablet >	parse_source (const std::string &)
	Parses and type checks a source file located at `file_name`.
bool	wrote_object_files () const
	Has this compiler written any object files?
void	cprover_macro_arities (std::map< irep_idt, std::size_t > &cprover_macros) const
	__CPROVER_... macros written to object files and their arities

Static Public Member Functions
static bool	write_bin_object_file (const std::string &file_name, const goto_modelt &src_goto_model, bool validate_goto_model, message_handlert &message_handler)
	Writes the goto functions of `src_goto_model` to a binary format object file.

Public Attributes
bool	echo_file_name
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::string	object_file_extension
std::string	output_file_executable
std::string	output_file_object
std::string	output_directory_object

Protected Member Functions
bool	write_bin_object_file (const std::string &file_name, const goto_modelt &src_goto_model)
void	add_compiler_specific_defines () const
void	convert_symbols (goto_modelt &)
bool	add_written_cprover_symbols (const symbol_tablet &symbol_table)

Static Protected Member Functions
static std::size_t	function_body_count (const goto_functionst &)

Protected Attributes
std::string	working_directory
std::string	override_language
std::list< std::string >	tmp_dirs
std::list< irep_idt >	seen_modes
messaget	log
cmdlinet &	cmdline
bool	warning_is_fatal
const bool	keep_file_local
	Whether to keep implementations of file-local symbols.
const std::string	file_local_mangle_suffix
	String to include in all mangled names.
std::map< irep_idt, symbolt >	written_macros
bool	wrote_object

Detailed Description

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

Constructor & Destructor Documentation

◆ compilet()

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

constructor

Definition at line 647 of file compile.cpp.

◆ ~compilet()

compilet::~compilet ( )

cleans up temporary files

Definition at line 673 of file compile.cpp.

Member Function Documentation

◆ add_compiler_specific_defines()

void compilet::add_compiler_specific_defines ( ) const

protected

Definition at line 692 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 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

Definition at line 740 of file compile.cpp.

◆ compile()

std::optional< symbol_tablet > compilet::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

Definition at line 698 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

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

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

Definition at line 681 of file compile.cpp.

◆ 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

Definition at line 122 of file compile.h.

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

Member Data Documentation

◆ cmdline

cmdlinet& compilet::cmdline

protected

Definition at line 111 of file compile.h.

◆ echo_file_name

bool compilet::echo_file_name

Definition at line 35 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 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

Definition at line 49 of file compile.h.

◆ library_paths

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

Definition at line 46 of file compile.h.

◆ log

messaget compilet::log

protected

Definition at line 110 of file compile.h.

◆ []

enum { ... } compilet::mode

◆ object_file_extension

std::string compilet::object_file_extension

Definition at line 51 of file compile.h.

◆ object_files

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

Definition at line 48 of file compile.h.

◆ output_directory_object

std::string compilet::output_directory_object

Definition at line 55 of file compile.h.

◆ output_file_executable

std::string compilet::output_file_executable

Definition at line 52 of file compile.h.

◆ output_file_object

std::string compilet::output_file_object

Definition at line 55 of file compile.h.

◆ override_language

std::string compilet::override_language

protected

Definition at line 105 of file compile.h.

◆ seen_modes

std::list<irep_idt> compilet::seen_modes

protected

Definition at line 108 of file compile.h.

◆ source_files

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

Definition at line 47 of file compile.h.

◆ tmp_dirs

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

protected

Definition at line 107 of file compile.h.

◆ validate_goto_model

bool compilet::validate_goto_model = false

Definition at line 36 of file compile.h.

◆ warning_is_fatal

bool compilet::warning_is_fatal

protected

Definition at line 112 of file compile.h.

◆ working_directory

std::string compilet::working_directory

protected

Definition at line 104 of file compile.h.

◆ written_macros

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

protected

Definition at line 145 of file compile.h.

◆ wrote_object

bool compilet::wrote_object

protected

Definition at line 152 of file compile.h.

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

goto-cc/compile.h
goto-cc/compile.cpp

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Enumeration Documentation

◆ anonymous enum

Constructor & Destructor Documentation

◆ compilet()

◆ ~compilet()

Member Function Documentation

◆ add_compiler_specific_defines()

◆ add_files_from_archive()

◆ add_input_file()

◆ add_written_cprover_symbols()

◆ compile()

◆ convert_symbols()

◆ cprover_macro_arities()

◆ doit()

◆ find_library()

◆ function_body_count()

◆ link()

◆ parse()

◆ parse_source()

◆ parse_stdin()

◆ write_bin_object_file() [1/2]

◆ write_bin_object_file() [2/2]

◆ wrote_object_files()

Member Data Documentation

◆ cmdline

◆ echo_file_name

◆ file_local_mangle_suffix

◆ keep_file_local

◆ libraries

◆ library_paths

◆ log

◆ []

◆ object_file_extension

◆ object_files

◆ output_directory_object

◆ output_file_executable

◆ output_file_object

◆ override_language

◆ seen_modes

◆ source_files

◆ tmp_dirs

◆ validate_goto_model

◆ warning_is_fatal

◆ working_directory

◆ written_macros

◆ wrote_object