#include <goto_convert_functions.h>

Inheritance diagram for goto_convert_functionst:

Collaboration diagram for goto_convert_functionst:

Public Member Functions
void	goto_convert (goto_functionst &functions)

void	convert_function (const irep_idt &identifier, goto_functionst::goto_functiont &result)

	goto_convert_functionst (symbol_table_baset &_symbol_table, message_handlert &_message_handler)

virtual	~goto_convert_functionst ()

Public Member Functions inherited from goto_convertt
void	goto_convert (const codet &code, goto_programt &dest, const irep_idt &mode)

	goto_convertt (symbol_table_baset &_symbol_table, message_handlert &_message_handler)

virtual	~goto_convertt ()

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

Protected Member Functions
void	add_return (goto_functionst::goto_functiont &, const typet &return_type, const source_locationt &)

Protected Member Functions inherited from goto_convertt
void	goto_convert_rec (const codet &code, goto_programt &dest, const irep_idt &mode)

symbolt &	new_tmp_symbol (const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)

symbol_exprt	make_compound_literal (const exprt &expr, goto_programt &dest, const irep_idt &mode)

void	clean_expr (exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)

void	clean_expr_address_of (exprt &expr, goto_programt &dest, const irep_idt &mode)

void	make_temp_symbol (exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)

void	rewrite_boolean (exprt &dest)
	re-write boolean operators into ?: More...

void	remove_side_effect (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used, bool address_taken)

void	remove_assignment (side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)

void	remove_pre (side_effect_exprt &expr, goto_programt &dest, bool result_is_used, bool address_taken, const irep_idt &mode)

void	remove_post (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)

void	remove_function_call (side_effect_expr_function_callt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)

void	remove_cpp_new (side_effect_exprt &expr, goto_programt &dest, bool result_is_used)

void	remove_cpp_delete (side_effect_exprt &expr, goto_programt &dest)

void	remove_malloc (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)

void	remove_temporary_object (side_effect_exprt &expr, goto_programt &dest)

void	remove_statement_expression (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used)

void	remove_gcc_conditional_expression (exprt &expr, goto_programt &dest, const irep_idt &mode)

void	remove_overflow (side_effect_expr_overflowt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode)

virtual void	do_cpp_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)

void	do_java_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)

void	do_java_new_array (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)

void	cpp_new_initializer (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
	builds a goto program for object initialization after new More...

virtual void	do_function_call (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)

virtual void	do_function_call_if (const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)

virtual void	do_function_call_symbol (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
	add function calls to function queue for later processing More...

virtual void	do_function_call_symbol (const symbolt &)

virtual void	do_function_call_other (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	convert_block (const code_blockt &code, goto_programt &dest, const irep_idt &mode)

void	convert_frontend_decl (const code_frontend_declt &, goto_programt &, const irep_idt &mode)

void	convert_decl_type (const codet &code, goto_programt &dest)

void	convert_expression (const code_expressiont &code, goto_programt &dest, const irep_idt &mode)

void	convert_assign (const code_assignt &code, goto_programt &dest, const irep_idt &mode)

void	convert_cpp_delete (const codet &code, goto_programt &dest)

void	convert_loop_contracts (const codet &code, goto_programt::targett loop, const irep_idt &mode)

void	convert_for (const code_fort &code, goto_programt &dest, const irep_idt &mode)

void	convert_while (const code_whilet &code, goto_programt &dest, const irep_idt &mode)

void	convert_dowhile (const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)

void	convert_assume (const code_assumet &code, goto_programt &dest, const irep_idt &mode)

void	convert_assert (const code_assertt &code, goto_programt &dest, const irep_idt &mode)

void	convert_switch (const code_switcht &code, goto_programt &dest, const irep_idt &mode)

void	convert_break (const code_breakt &code, goto_programt &dest, const irep_idt &mode)

void	convert_return (const code_frontend_returnt &, goto_programt &dest, const irep_idt &mode)

void	convert_continue (const code_continuet &code, goto_programt &dest, const irep_idt &mode)

void	convert_ifthenelse (const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)

void	convert_goto (const code_gotot &code, goto_programt &dest)

void	convert_gcc_computed_goto (const codet &code, goto_programt &dest)

void	convert_skip (const codet &code, goto_programt &dest)

void	convert_label (const code_labelt &code, goto_programt &dest, const irep_idt &mode)

void	convert_gcc_local_label (const codet &code, goto_programt &dest)

void	convert_switch_case (const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)

void	convert_gcc_switch_case_range (const code_gcc_switch_case_ranget &, goto_programt &dest, const irep_idt &mode)

void	convert_function_call (const code_function_callt &code, goto_programt &dest, const irep_idt &mode)

void	convert_start_thread (const codet &code, goto_programt &dest)

void	convert_end_thread (const codet &code, goto_programt &dest)

void	convert_atomic_begin (const codet &code, goto_programt &dest)

void	convert_atomic_end (const codet &code, goto_programt &dest)

void	convert_msc_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode)

void	convert_msc_try_except (const codet &code, goto_programt &dest, const irep_idt &mode)

void	convert_msc_leave (const codet &code, goto_programt &dest, const irep_idt &mode)

void	convert_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode)

void	convert_CPROVER_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode)

void	convert_CPROVER_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode)

void	convert_CPROVER_throw (const codet &code, goto_programt &dest, const irep_idt &mode)

void	convert_asm (const code_asmt &code, goto_programt &dest)

void	convert (const codet &code, goto_programt &dest, const irep_idt &mode)
	converts 'code' and appends the result to 'dest' More...

void	copy (const codet &code, goto_program_instruction_typet type, goto_programt &dest)

symbol_exprt	exception_flag (const irep_idt &mode)

void	unwind_destructor_stack (const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, optionalt< node_indext > destructor_start_point={}, optionalt< node_indext > destructor_end_point={})
	Unwinds the destructor stack and creates destructors for each node between destructor_start_point and destructor_end_point (including the start, excluding the end). More...

void	finish_gotos (goto_programt &dest, const irep_idt &mode)

void	finish_computed_gotos (goto_programt &dest)

void	optimize_guarded_gotos (goto_programt &dest)
	Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a branch target. More...

exprt	case_guard (const exprt &value, const caset &case_op)

void	generate_ifthenelse (const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
	if(guard) true_case; else false_case; More...

void	generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode)
	if(guard) goto target_true; else goto target_false; More...

void	generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, const source_locationt &, goto_programt &dest, const irep_idt &mode)

void	generate_thread_block (const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode)
	Generates the necessary goto-instructions to represent a thread-block. More...

irep_idt	get_string_constant (const exprt &expr)

bool	get_string_constant (const exprt &expr, irep_idt &)

exprt	get_constant (const exprt &expr)

void	do_enum_is_in_range (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
	Converts calls to the built in `enum_is_in_range` function to a test that the given enum value is in the valid range of values for that enum type. More...

void	do_atomic_begin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	do_atomic_end (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	do_create_thread (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	do_array_equal (const exprt &lhs, const symbol_exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)

void	do_array_op (const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	do_printf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	do_scanf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	do_input (const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)

void	do_output (const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)

void	do_prob_coin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	do_prob_uniform (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)

void	do_havoc_slice (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)

exprt	get_array_argument (const exprt &src)

Static Protected Member Functions
static bool	hide (const goto_programt &)

Static Protected Member Functions inherited from goto_convertt
static bool	needs_cleaning (const exprt &expr)
	Returns 'true' for expressions that may change the program state. More...

static bool	assignment_lhs_needs_temporary (const exprt &lhs)

static bool	has_function_call (const exprt &expr)

static void	replace_new_object (const exprt &object, exprt &dest)

static void	collect_operands (const exprt &expr, const irep_idt &id, std::list< exprt > &dest)

Additional Inherited Members
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 }

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

Protected Types inherited from goto_convertt
typedef std::map< irep_idt, std::pair< goto_programt::targett, node_indext > >	labelst

typedef std::list< std::pair< goto_programt::targett, node_indext > >	gotost

typedef std::list< goto_programt::targett >	computed_gotost

typedef exprt::operandst	caset

typedef std::list< std::pair< goto_programt::targett, caset > >	casest

typedef std::map< goto_programt::targett, casest::iterator >	cases_mapt

Protected Attributes inherited from goto_convertt
symbol_table_baset &	symbol_table

namespacet	ns

std::string	tmp_symbol_prefix

lifetimet	lifetime = lifetimet::STATIC_GLOBAL

struct goto_convertt::targetst	targets

Protected Attributes inherited from messaget
message_handlert *	message_handler

mstreamt	mstream

Detailed Description

Definition at line 40 of file goto_convert_functions.h.

Constructor & Destructor Documentation

◆ goto_convert_functionst()

goto_convert_functionst::goto_convert_functionst	(	symbol_table_baset &	_symbol_table,
		message_handlert &	_message_handler
	)

Definition at line 22 of file goto_convert_functions.cpp.

◆ ~goto_convert_functionst()

goto_convert_functionst::~goto_convert_functionst ( )

virtual

Definition at line 29 of file goto_convert_functions.cpp.

Member Function Documentation

◆ add_return()

void goto_convert_functionst::add_return	(	goto_functionst::goto_functiont &	f,
		const typet &	return_type,
		const source_locationt &	source_location
	)

protected

Definition at line 89 of file goto_convert_functions.cpp.

◆ convert_function()

void goto_convert_functionst::convert_function	(	const irep_idt &	identifier,
		goto_functionst::goto_functiont &	result
	)

Definition at line 142 of file goto_convert_functions.cpp.

◆ goto_convert()

void goto_convert_functionst::goto_convert ( goto_functionst & functions )

Definition at line 33 of file goto_convert_functions.cpp.

◆ hide()

bool goto_convert_functionst::hide ( const goto_programt & goto_program )

staticprotected

Definition at line 75 of file goto_convert_functions.cpp.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_convert_functions.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_convert_functions.cpp

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Additional Inherited Members