#include <goto_convert_class.h>

Inheritance diagram for goto_convertt:

Collaboration diagram for goto_convertt:

Classes
struct	break_continue_targetst

struct	break_switch_targetst

struct	leave_targett

struct	targetst

struct	throw_targett

Public Member Functions
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 Types
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 Member Functions
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	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)

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

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

Detailed Description

Definition at line 30 of file goto_convert_class.h.

Member Typedef Documentation

◆ cases_mapt

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

protected

Definition at line 381 of file goto_convert_class.h.

◆ casest

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

protected

Definition at line 380 of file goto_convert_class.h.

◆ caset

typedef exprt::operandst goto_convertt::caset

protected

Definition at line 379 of file goto_convert_class.h.

◆ computed_gotost

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

protected

Definition at line 378 of file goto_convert_class.h.

◆ gotost

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

protected

Definition at line 377 of file goto_convert_class.h.

◆ labelst

typedef std::map<irep_idt, std::pair<goto_programt::targett, node_indext> > goto_convertt::labelst

protected

Definition at line 375 of file goto_convert_class.h.

Constructor & Destructor Documentation

◆ goto_convertt()

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

inline

Definition at line 36 of file goto_convert_class.h.

◆ ~goto_convertt()

virtual goto_convertt::~goto_convertt ( )

inlinevirtual

Definition at line 46 of file goto_convert_class.h.

Member Function Documentation

◆ assignment_lhs_needs_temporary()

static bool goto_convertt::assignment_lhs_needs_temporary ( const exprt & lhs )

inlinestaticprotected

Definition at line 96 of file goto_convert_class.h.

◆ case_guard()

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

protected

Definition at line 1120 of file goto_convert.cpp.

◆ clean_expr()

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

protected

Definition at line 166 of file goto_clean_expr.cpp.

◆ clean_expr_address_of()

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

protected

Definition at line 439 of file goto_clean_expr.cpp.

◆ collect_operands()

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

staticprotected

Definition at line 1482 of file goto_convert.cpp.

◆ convert()

void goto_convertt::convert	(	const codet &	code,
		goto_programt &	dest,
		const irep_idt &	mode
	)

protected

converts 'code' and appends the result to 'dest'

Definition at line 430 of file goto_convert.cpp.

◆ convert_asm()

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

protected

Definition at line 14 of file goto_asm.cpp.

◆ convert_assert()

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

protected

Definition at line 827 of file goto_convert.cpp.

◆ convert_assign()

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

protected

Definition at line 682 of file goto_convert.cpp.

◆ convert_assume()

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

protected

Definition at line 849 of file goto_convert.cpp.

◆ convert_atomic_begin()

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

protected

Definition at line 1412 of file goto_convert.cpp.

◆ convert_atomic_end()

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

protected

Definition at line 1424 of file goto_convert.cpp.

◆ convert_block()

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

protected

Definition at line 543 of file goto_convert.cpp.

◆ convert_break()

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

protected

Definition at line 1270 of file goto_convert.cpp.

◆ convert_continue()

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

protected

Definition at line 1347 of file goto_convert.cpp.

◆ convert_cpp_delete()

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

protected

Definition at line 765 of file goto_convert.cpp.

◆ convert_CPROVER_throw()

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

protected

Definition at line 181 of file goto_convert_exceptions.cpp.

◆ convert_CPROVER_try_catch()

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

protected

Definition at line 145 of file goto_convert_exceptions.cpp.

◆ convert_CPROVER_try_finally()

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

protected

Definition at line 212 of file goto_convert_exceptions.cpp.

◆ convert_decl_type()

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

protected

Definition at line 675 of file goto_convert.cpp.

◆ convert_dowhile()

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

protected

Definition at line 1051 of file goto_convert.cpp.

◆ convert_end_thread()

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

protected

Definition at line 1400 of file goto_convert.cpp.

◆ convert_expression()

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

protected

Definition at line 573 of file goto_convert.cpp.

◆ convert_for()

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

protected

Definition at line 903 of file goto_convert.cpp.

◆ convert_frontend_decl()

void goto_convertt::convert_frontend_decl	(	const code_frontend_declt &	code,
		goto_programt &	dest,
		const irep_idt &	mode
	)

protected

Definition at line 610 of file goto_convert.cpp.

◆ convert_function_call()

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

protected

Definition at line 18 of file goto_convert_function_call.cpp.

◆ convert_gcc_computed_goto()

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

protected

Definition at line 1376 of file goto_convert.cpp.

◆ convert_gcc_local_label()

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

protected

Definition at line 350 of file goto_convert.cpp.

◆ convert_gcc_switch_case_range()

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

protected

Definition at line 389 of file goto_convert.cpp.

◆ convert_goto()

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

protected

Definition at line 1366 of file goto_convert.cpp.

◆ convert_ifthenelse()

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

protected

Definition at line 1436 of file goto_convert.cpp.

◆ convert_label()

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

protected

Definition at line 309 of file goto_convert.cpp.

◆ convert_loop_contracts()

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

protected

Definition at line 861 of file goto_convert.cpp.

◆ convert_msc_leave()

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

protected

Definition at line 70 of file goto_convert_exceptions.cpp.

◆ convert_msc_try_except()

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

protected

Definition at line 55 of file goto_convert_exceptions.cpp.

◆ convert_msc_try_finally()

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

protected

Definition at line 17 of file goto_convert_exceptions.cpp.

◆ convert_return()

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

protected

Definition at line 1287 of file goto_convert.cpp.

◆ convert_skip()

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

protected

Definition at line 841 of file goto_convert.cpp.

◆ convert_start_thread()

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

protected

Definition at line 1388 of file goto_convert.cpp.

◆ convert_switch()

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

protected

Definition at line 1149 of file goto_convert.cpp.

◆ convert_switch_case()

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

protected

Definition at line 357 of file goto_convert.cpp.

◆ convert_try_catch()

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

protected

Definition at line 86 of file goto_convert_exceptions.cpp.

◆ convert_while()

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

protected

Definition at line 995 of file goto_convert.cpp.

◆ copy()

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

protected

Definition at line 300 of file goto_convert.cpp.

◆ cpp_new_initializer()

void goto_convertt::cpp_new_initializer	(	const exprt &	lhs,
		const side_effect_exprt &	rhs,
		goto_programt &	dest
	)

protected

builds a goto program for object initialization after new

Definition at line 510 of file builtin_functions.cpp.

◆ do_array_equal()

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

protected

◆ do_array_op()

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

protected

Definition at line 571 of file builtin_functions.cpp.

◆ do_atomic_begin()

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

protected

Definition at line 343 of file builtin_functions.cpp.

◆ do_atomic_end()

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

protected

Definition at line 366 of file builtin_functions.cpp.

◆ do_cpp_new()

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

protectedvirtual

Definition at line 389 of file builtin_functions.cpp.

◆ do_create_thread()

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

protected

◆ do_enum_is_in_range()

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

protected

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.

Note that the check for the range of values is done by creating a disjunction comparing the expression with each possible valid value.

Parameters

lhs	The destination for the generated assignment.
function	The `enum_is_in_range` symbol of the source function call.
arguments	A collection of arguments, which is expected to contain a single argument which is an expression that resolves to a value of enum type. The arguments are expected to have been prevalidated by the typechecking process.
dest	The goto program into which the generated assignment is copied.

Definition at line 618 of file builtin_functions.cpp.

◆ do_function_call()

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

protectedvirtual

Definition at line 31 of file goto_convert_function_call.cpp.

◆ do_function_call_if()

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

protectedvirtual

Definition at line 83 of file goto_convert_function_call.cpp.

◆ do_function_call_other()

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

protectedvirtual

Definition at line 146 of file goto_convert_function_call.cpp.

◆ do_function_call_symbol() [1/2]

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

protectedvirtual

add function calls to function queue for later processing

Definition at line 725 of file builtin_functions.cpp.

◆ do_function_call_symbol() [2/2]

virtual void goto_convertt::do_function_call_symbol ( const symbolt & )

inlineprotectedvirtual

Definition at line 218 of file goto_convert_class.h.

◆ do_havoc_slice()

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

protected

Definition at line 645 of file builtin_functions.cpp.

◆ do_input()

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

protected

Definition at line 313 of file builtin_functions.cpp.

◆ do_java_new()

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

protected

◆ do_java_new_array()

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

protected

◆ do_output()

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

protected

Definition at line 328 of file builtin_functions.cpp.

◆ do_printf()

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

protected

Definition at line 196 of file builtin_functions.cpp.

◆ do_prob_coin()

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

protected

Definition at line 110 of file builtin_functions.cpp.

◆ do_prob_uniform()

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

protected

Definition at line 32 of file builtin_functions.cpp.

◆ do_scanf()

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

protected

Definition at line 210 of file builtin_functions.cpp.

◆ exception_flag()

symbol_exprt goto_convertt::exception_flag ( const irep_idt & mode )

protected

Definition at line 236 of file goto_convert_exceptions.cpp.

◆ finish_computed_gotos()

void goto_convertt::finish_computed_gotos ( goto_programt & dest )

protected

Definition at line 202 of file goto_convert.cpp.

◆ finish_gotos()

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

protected

Definition at line 109 of file goto_convert.cpp.

◆ generate_conditional_branch() [1/2]

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

protected

Definition at line 1666 of file goto_convert.cpp.

◆ generate_conditional_branch() [2/2]

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

protected

if(guard) goto target_true; else goto target_false;

Definition at line 1700 of file goto_convert.cpp.

◆ generate_ifthenelse()

void goto_convertt::generate_ifthenelse	(	const exprt &	cond,
		goto_programt &	true_case,
		goto_programt &	false_case,
		const source_locationt &	source_location,
		goto_programt &	dest,
		const irep_idt &	mode
	)

protected

if(guard) true_case; else false_case;

Definition at line 1509 of file goto_convert.cpp.

◆ generate_thread_block()

void goto_convertt::generate_thread_block	(	const code_blockt &	thread_body,
		goto_programt &	dest,
		const irep_idt &	mode
	)

protected

Generates the necessary goto-instructions to represent a thread-block.

Specifically, the following instructions are generated:

A: START_THREAD : C B: GOTO Z C: SKIP D: {THREAD BODY} E: END_THREAD Z: SKIP

Parameters

	thread_body	Sequence of codet's that can be executed in parallel
[out]	dest	Resulting goto-instructions
	mode	Language mode

Definition at line 1950 of file goto_convert.cpp.

◆ get_array_argument()

exprt goto_convertt::get_array_argument ( const exprt & src )

protected

Definition at line 538 of file builtin_functions.cpp.

◆ get_constant()

exprt goto_convertt::get_constant ( const exprt & expr )

protected

Definition at line 1835 of file goto_convert.cpp.

◆ get_string_constant() [1/2]

irep_idt goto_convertt::get_string_constant ( const exprt & expr )

protected

Definition at line 1821 of file goto_convert.cpp.

◆ get_string_constant() [2/2]

bool goto_convertt::get_string_constant	(	const exprt &	expr,
		irep_idt &	value
	)

protected

Definition at line 1774 of file goto_convert.cpp.

◆ goto_convert()

void goto_convertt::goto_convert	(	const codet &	code,
		goto_programt &	dest,
		const irep_idt &	mode
	)

Definition at line 279 of file goto_convert.cpp.

◆ goto_convert_rec()

void goto_convertt::goto_convert_rec	(	const codet &	code,
		goto_programt &	dest,
		const irep_idt &	mode
	)

protected

Definition at line 287 of file goto_convert.cpp.

◆ has_function_call()

bool goto_convertt::has_function_call ( const exprt & expr )

staticprotected

Definition at line 25 of file goto_convert_side_effect.cpp.

◆ make_compound_literal()

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

protected

Definition at line 20 of file goto_clean_expr.cpp.

◆ make_temp_symbol()

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

protected

Definition at line 1884 of file goto_convert.cpp.

◆ needs_cleaning()

bool goto_convertt::needs_cleaning ( const exprt & expr )

staticprotected

Returns 'true' for expressions that may change the program state.

Expressions that may trigger undefined behavior (e.g., dereference, index, division) are deliberately not included.

Definition at line 67 of file goto_clean_expr.cpp.

◆ new_tmp_symbol()

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

protected

Definition at line 1861 of file goto_convert.cpp.

◆ optimize_guarded_gotos()

void goto_convertt::optimize_guarded_gotos ( goto_programt & dest )

protected

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.

parameters: Destination goto program

Definition at line 235 of file goto_convert.cpp.

◆ remove_assignment()

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

protected

Definition at line 38 of file goto_convert_side_effect.cpp.

◆ remove_cpp_delete()

void goto_convertt::remove_cpp_delete	(	side_effect_exprt &	expr,
		goto_programt &	dest
	)

protected

Definition at line 447 of file goto_convert_side_effect.cpp.

◆ remove_cpp_new()

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

protected

Definition at line 420 of file goto_convert_side_effect.cpp.

◆ remove_function_call()

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

protected

Definition at line 354 of file goto_convert_side_effect.cpp.

◆ remove_gcc_conditional_expression()

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

protected

Definition at line 508 of file goto_clean_expr.cpp.

◆ remove_malloc()

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

protected

Definition at line 463 of file goto_convert_side_effect.cpp.

◆ remove_overflow()

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

protected

Definition at line 601 of file goto_convert_side_effect.cpp.

◆ remove_post()

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

protected

Definition at line 271 of file goto_convert_side_effect.cpp.

◆ remove_pre()

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

protected

Definition at line 179 of file goto_convert_side_effect.cpp.

◆ remove_side_effect()

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

protected

Definition at line 673 of file goto_convert_side_effect.cpp.

◆ remove_statement_expression()

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

protected

Definition at line 532 of file goto_convert_side_effect.cpp.

◆ remove_temporary_object()

void goto_convertt::remove_temporary_object	(	side_effect_exprt &	expr,
		goto_programt &	dest
	)

protected

Definition at line 496 of file goto_convert_side_effect.cpp.

◆ replace_new_object()

void goto_convertt::replace_new_object	(	const exprt &	object,
		exprt &	dest
	)

staticprotected

Definition at line 409 of file goto_convert_side_effect.cpp.

◆ rewrite_boolean()

void goto_convertt::rewrite_boolean ( exprt & dest )

protected

re-write boolean operators into ?:

Definition at line 101 of file goto_clean_expr.cpp.

◆ unwind_destructor_stack()

void goto_convertt::unwind_destructor_stack	(	const source_locationt &	source_location,
		goto_programt &	dest,
		const irep_idt &	mode,
		optionalt< node_indext >	end_index = `{}`,
		optionalt< node_indext >	starting_index = `{}`
	)

protected

Unwinds the destructor stack and creates destructors for each node between destructor_start_point and destructor_end_point (including the start, excluding the end).

If end_index isn't passed, it will unwind the whole stack. If start_index isn't passed, it will unwind from the current node.

When destructors are non-trivial (i.e. if they contain DECL or GOTO statements) then unwinding becomes more complicated because when we call convert on the destructor code it may recursively invoke this function.

Say we have a tree of [3, 2, 1, 0] and we start unwinding from top to bottom. If node 1 has such a non-trivial destructor during the convert it will add nodes to the tree so it ends up looking like this:

3, 2, 1, 0
   5, 4,/

If for example the destructor contained a THROW statement then it would unwind destroying variables 5, 4 and finally 0. Note that we don't have 1 here even if that was the instruction that triggered the recursive unwind because it's already been popped off before convert is called.

After our unwind has finished, we return to our [3, 2, 1, 0] branch and continue processing the branch for destructor 0.

Definition at line 284 of file goto_convert_exceptions.cpp.

Member Data Documentation

◆ lifetime

lifetimet goto_convertt::lifetime = lifetimet::STATIC_GLOBAL

protected

Definition at line 54 of file goto_convert_class.h.

◆ ns

namespacet goto_convertt::ns

protected

Definition at line 52 of file goto_convert_class.h.

◆ symbol_table

symbol_table_baset& goto_convertt::symbol_table

protected

Definition at line 51 of file goto_convert_class.h.

◆ targets

struct goto_convertt::targetst goto_convertt::targets

protected

◆ tmp_symbol_prefix

std::string goto_convertt::tmp_symbol_prefix

protected

Definition at line 53 of file goto_convert_class.h.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_convert_class.h
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/builtin_functions.cpp
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_asm.cpp
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_clean_expr.cpp
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_convert.cpp
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_convert_exceptions.cpp
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_convert_function_call.cpp
/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-programs/goto_convert_side_effect.cpp

Classes

Public Member Functions

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ cases_mapt

◆ casest

◆ caset

◆ computed_gotost

◆ gotost

◆ labelst

Constructor & Destructor Documentation

◆ goto_convertt()

◆ ~goto_convertt()

Member Function Documentation

◆ assignment_lhs_needs_temporary()

◆ case_guard()

◆ clean_expr()

◆ clean_expr_address_of()

◆ collect_operands()

◆ convert()

◆ convert_asm()

◆ convert_assert()

◆ convert_assign()

◆ convert_assume()

◆ convert_atomic_begin()

◆ convert_atomic_end()

◆ convert_block()

◆ convert_break()

◆ convert_continue()

◆ convert_cpp_delete()

◆ convert_CPROVER_throw()

◆ convert_CPROVER_try_catch()

◆ convert_CPROVER_try_finally()

◆ convert_decl_type()

◆ convert_dowhile()

◆ convert_end_thread()

◆ convert_expression()

◆ convert_for()

◆ convert_frontend_decl()

◆ convert_function_call()

◆ convert_gcc_computed_goto()

◆ convert_gcc_local_label()

◆ convert_gcc_switch_case_range()

◆ convert_goto()

◆ convert_ifthenelse()

◆ convert_label()

◆ convert_loop_contracts()

◆ convert_msc_leave()

◆ convert_msc_try_except()

◆ convert_msc_try_finally()

◆ convert_return()

◆ convert_skip()

◆ convert_start_thread()

◆ convert_switch()

◆ convert_switch_case()

◆ convert_try_catch()

◆ convert_while()

◆ copy()

◆ cpp_new_initializer()

◆ do_array_equal()

◆ do_array_op()

◆ do_atomic_begin()

◆ do_atomic_end()

◆ do_cpp_new()

◆ do_create_thread()

◆ do_enum_is_in_range()

◆ do_function_call()

◆ do_function_call_if()

◆ do_function_call_other()

◆ do_function_call_symbol() [1/2]

◆ do_function_call_symbol() [2/2]

◆ do_havoc_slice()

◆ do_input()

◆ do_java_new()

◆ do_java_new_array()