#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 ()
	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 goto_modelt &)
	writes the goto functions in the function table to a binary format object file. More...

bool	write_bin_object_file (const std::string &, const goto_modelt &)
	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 messaget
virtual void	set_message_handler (message_handlert &_message_handler)

message_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

messaget &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () 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

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_idt >	seen_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 (class configt &config) const

void	convert_symbols (goto_functionst &dest)

bool	add_written_cprover_symbols (const symbol_tablet &symbol_table)

Protected Attributes
cmdlinet &	cmdline

bool	warning_is_fatal

std::map< irep_idt, symbolt >	written_macros

bool	wrote_object

Protected Attributes inherited from messaget
message_handlert *	message_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 25 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 37 of file compile.h.

Constructor & Destructor Documentation

◆ compilet()

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

constructor

Returns: nothing

Definition at line 659 of file compile.cpp.

◆ ~compilet()

compilet::~compilet ( )

cleans up temporary files

Returns: nothing

Definition at line 673 of file compile.cpp.

Member Function Documentation

◆ add_compiler_specific_defines()

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

protected

Definition at line 693 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 230 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 190 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()

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

◆ convert_symbols()

void compilet::convert_symbols ( goto_functionst & dest )

protected

Definition at line 699 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 78 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 306 of file compile.cpp.

◆ function_body_count()

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

protected

Definition at line 682 of file compile.cpp.

◆ link()

bool compilet::link ( )

parses object files and links them

Returns: true on error, false otherwise

Definition at line 346 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 459 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 633 of file compile.cpp.

◆ parse_stdin()

bool compilet::parse_stdin ( )

parses a source file (low-level parsing)

Returns: true on error, false otherwise

Definition at line 543 of file compile.cpp.

◆ write_bin_object_file()

bool compilet::write_bin_object_file	(	const std::string &	file_name,
		const goto_modelt &	goto_model
	)

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

◆ write_object_file()

bool compilet::write_object_file	(	const std::string &	file_name,
		const goto_modelt &	goto_model
	)

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 587 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 33 of file compile.h.

◆ goto_model

goto_modelt compilet::goto_model

Definition at line 30 of file compile.h.

◆ libraries

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

Definition at line 48 of file compile.h.

◆ library_paths

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

Definition at line 45 of file compile.h.

◆ mode

enum { ... } compilet::mode

◆ ns

namespacet compilet::ns

Definition at line 29 of file compile.h.

◆ object_file_extension

std::string compilet::object_file_extension

Definition at line 52 of file compile.h.

◆ object_files

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

Definition at line 47 of file compile.h.

◆ output_directory_object

std::string compilet::output_directory_object

Definition at line 56 of file compile.h.

◆ output_file_executable

std::string compilet::output_file_executable

Definition at line 53 of file compile.h.

◆ output_file_object

std::string compilet::output_file_object

Definition at line 56 of file compile.h.

◆ override_language

std::string compilet::override_language

Definition at line 35 of file compile.h.

◆ seen_modes

std::list<irep_idt> compilet::seen_modes

Definition at line 50 of file compile.h.

◆ source_files

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

Definition at line 46 of file compile.h.

◆ tmp_dirs

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

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

◆ written_macros

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

protected

Definition at line 106 of file compile.h.

◆ wrote_object

bool compilet::wrote_object

protected

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

Public Attributes

Protected Member Functions

Protected Attributes

Additional Inherited Members

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

◆ write_object_file()

◆ wrote_object_files()

Member Data Documentation

◆ cmdline

◆ echo_file_name

◆ goto_model

◆ libraries

◆ library_paths

◆ mode

◆ ns

◆ object_file_extension

◆ object_files

◆ output_directory_object

◆ output_file_executable

◆ output_file_object

◆ override_language

◆ seen_modes

◆ source_files

◆ tmp_dirs

◆ warning_is_fatal

◆ working_directory

◆ written_macros

◆ wrote_object