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

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

Protected Types
typedef std::list< std::pair< goto_programt::targett, goto_programt::instructiont > >	declaration_hop_instrumentationt

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, goto_programt::target_less_than >	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)

clean_expr_resultt	clean_expr (exprt &expr, const irep_idt &mode, bool result_is_used=true)

clean_expr_resultt	clean_expr_address_of (exprt &expr, const irep_idt &mode)

irep_idt	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 ?:

clean_expr_resultt	remove_side_effect (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used, bool address_taken)

clean_expr_resultt	remove_assignment (side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)

clean_expr_resultt	remove_pre (side_effect_exprt &expr, bool result_is_used, bool address_taken, const irep_idt &mode)

clean_expr_resultt	remove_post (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)

clean_expr_resultt	remove_function_call (side_effect_expr_function_callt &expr, const irep_idt &mode, bool result_is_used)

clean_expr_resultt	remove_cpp_new (side_effect_exprt &expr, bool result_is_used)

clean_expr_resultt	remove_cpp_delete (side_effect_exprt &expr)

clean_expr_resultt	remove_malloc (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)

clean_expr_resultt	remove_temporary_object (side_effect_exprt &expr)

clean_expr_resultt	remove_statement_expression (side_effect_exprt &expr, const irep_idt &mode, bool result_is_used)

clean_expr_resultt	remove_gcc_conditional_expression (exprt &expr, const irep_idt &mode)

clean_expr_resultt	remove_overflow (side_effect_expr_overflowt &expr, 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

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

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)

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'

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, std::optional< node_indext > destructor_end_point={}, std::optional< node_indext > destructor_start_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).

declaration_hop_instrumentationt	build_declaration_hops (goto_programt &dest, std::unordered_map< irep_idt, symbolt, irep_id_hash > &label_flags, const build_declaration_hops_inputst &inputs)

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.

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

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

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;

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.

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

void	do_alloca (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
	alloca allocates memory that is freed when leaving the function (and not the block, as regular destructors would do).

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.

static bool	assignment_lhs_needs_temporary (const exprt &lhs)

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.

static commandt	command (unsigned c)
	Create an ECMA-48 SGR (Select Graphic Rendition) command.

Static Public Attributes inherited from messaget
static eomt	eom

static const commandt	reset
	return to default formatting, as defined by the terminal

static const commandt	red
	render text with red foreground color

static const commandt	green
	render text with green foreground color

static const commandt	yellow
	render text with yellow foreground color

static const commandt	blue
	render text with blue foreground color

static const commandt	magenta
	render text with magenta foreground color

static const commandt	cyan
	render text with cyan foreground color

static const commandt	bright_red
	render text with bright red foreground color

static const commandt	bright_green
	render text with bright green foreground color

static const commandt	bright_yellow
	render text with bright yellow foreground color

static const commandt	bright_blue
	render text with bright blue foreground color

static const commandt	bright_magenta
	render text with bright magenta foreground color

static const commandt	bright_cyan
	render text with bright cyan foreground color

static const commandt	bold
	render text with bold font

static const commandt	faint
	render text with faint font

static const commandt	italic
	render italic text

static const commandt	underline
	render underlined text

Detailed Description

Definition at line 33 of file goto_convert_class.h.

Member Typedef Documentation

◆ cases_mapt

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

protected

Definition at line 395 of file goto_convert_class.h.

◆ casest

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

protected

Definition at line 390 of file goto_convert_class.h.

◆ caset

typedef exprt::operandst goto_convertt::caset

protected

Definition at line 389 of file goto_convert_class.h.

◆ computed_gotost

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

protected

Definition at line 388 of file goto_convert_class.h.

◆ declaration_hop_instrumentationt

typedef std::list< std::pair<goto_programt::targett, goto_programt::instructiont> > goto_convertt::declaration_hop_instrumentationt

protected

Definition at line 371 of file goto_convert_class.h.

◆ gotost

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

protected

Definition at line 387 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 386 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 39 of file goto_convert_class.h.

◆ ~goto_convertt()

virtual goto_convertt::~goto_convertt ( )

inlinevirtual

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

◆ build_declaration_hops()

goto_convertt::declaration_hop_instrumentationt goto_convertt::build_declaration_hops	(	goto_programt &	dest,
		std::unordered_map< irep_idt, symbolt, irep_id_hash > &	label_flags,
		const build_declaration_hops_inputst &	inputs
	)

protected

Definition at line 107 of file goto_convert.cpp.

◆ case_guard()

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

protected

Definition at line 1334 of file goto_convert.cpp.

◆ clean_expr()

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

protected

Definition at line 438 of file goto_clean_expr.cpp.

◆ clean_expr_address_of()

goto_convertt::clean_expr_resultt goto_convertt::clean_expr_address_of	(	exprt &	expr,
		const irep_idt &	mode
	)

protected

Definition at line 754 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 1729 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 616 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 1035 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 877 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 1058 of file goto_convert.cpp.

◆ convert_atomic_begin()

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

protected

Definition at line 1644 of file goto_convert.cpp.

◆ convert_atomic_end()

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

protected

Definition at line 1654 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 730 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 1503 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 1580 of file goto_convert.cpp.

◆ convert_cpp_delete()

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

protected

Definition at line 972 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 872 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 1255 of file goto_convert.cpp.

◆ convert_end_thread()

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

protected

Definition at line 1634 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 759 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 1101 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 800 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 20 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 1612 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 530 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 575 of file goto_convert.cpp.

◆ convert_goto()

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

protected

Definition at line 1599 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 1664 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 489 of file goto_convert.cpp.

◆ convert_loop_contracts()

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

protected

Definition at line 1073 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 1520 of file goto_convert.cpp.

◆ convert_skip()

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

protected

Definition at line 1052 of file goto_convert.cpp.

◆ convert_start_thread()

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

protected

Definition at line 1624 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 1363 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 535 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 1199 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 480 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_alloca()

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

protected

alloca allocates memory that is freed when leaving the function (and not the block, as regular destructors would do).

Definition at line 700 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 570 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 340 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 363 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 386 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_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 33 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 91 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 154 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 809 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 225 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 617 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 310 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 325 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 193 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 33 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 207 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 365 of file goto_convert.cpp.

◆ finish_gotos()

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

protected

Definition at line 252 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 1936 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 1975 of file goto_convert.cpp.

◆ generate_ifthenelse()

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

protected

if(guard) true_case; else false_case;

Definition at line 1756 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 2234 of file goto_convert.cpp.

◆ get_array_argument()

exprt goto_convertt::get_array_argument ( const exprt & src )

protected

Definition at line 537 of file builtin_functions.cpp.

◆ get_constant()

exprt goto_convertt::get_constant ( const exprt & expr )

protected

Definition at line 2116 of file goto_convert.cpp.

◆ get_string_constant() [1/2]

irep_idt goto_convertt::get_string_constant ( const exprt & expr )

protected

Definition at line 2102 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 2055 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 459 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 467 of file goto_convert.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 276 of file goto_clean_expr.cpp.

◆ make_temp_symbol()

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

protected

Definition at line 2166 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 323 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 2141 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 398 of file goto_convert.cpp.

◆ remove_assignment()

goto_convertt::clean_expr_resultt goto_convertt::remove_assignment	(	side_effect_exprt &	expr,
		bool	result_is_used,
		bool	address_taken,
		const irep_idt &	mode
	)

protected

Definition at line 27 of file goto_convert_side_effect.cpp.

◆ remove_cpp_delete()

goto_convertt::clean_expr_resultt goto_convertt::remove_cpp_delete ( side_effect_exprt & expr )

protected

Definition at line 461 of file goto_convert_side_effect.cpp.

◆ remove_cpp_new()

goto_convertt::clean_expr_resultt goto_convertt::remove_cpp_new	(	side_effect_exprt &	expr,
		bool	result_is_used
	)

protected

Definition at line 429 of file goto_convert_side_effect.cpp.

◆ remove_function_call()

goto_convertt::clean_expr_resultt goto_convertt::remove_function_call	(	side_effect_expr_function_callt &	expr,
		const irep_idt &	mode,
		bool	result_is_used
	)

protected

Definition at line 361 of file goto_convert_side_effect.cpp.

◆ remove_gcc_conditional_expression()

goto_convertt::clean_expr_resultt goto_convertt::remove_gcc_conditional_expression	(	exprt &	expr,
		const irep_idt &	mode
	)

protected

Definition at line 827 of file goto_clean_expr.cpp.

◆ remove_malloc()

goto_convertt::clean_expr_resultt goto_convertt::remove_malloc	(	side_effect_exprt &	expr,
		const irep_idt &	mode,
		bool	result_is_used
	)

protected

Definition at line 478 of file goto_convert_side_effect.cpp.

◆ remove_overflow()

goto_convertt::clean_expr_resultt goto_convertt::remove_overflow	(	side_effect_expr_overflowt &	expr,
		bool	result_is_used,
		const irep_idt &	mode
	)

protected

Definition at line 633 of file goto_convert_side_effect.cpp.

◆ remove_post()

goto_convertt::clean_expr_resultt goto_convertt::remove_post	(	side_effect_exprt &	expr,
		const irep_idt &	mode,
		bool	result_is_used
	)

protected

Definition at line 274 of file goto_convert_side_effect.cpp.

◆ remove_pre()

goto_convertt::clean_expr_resultt goto_convertt::remove_pre	(	side_effect_exprt &	expr,
		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()

goto_convertt::clean_expr_resultt goto_convertt::remove_side_effect	(	side_effect_exprt &	expr,
		const irep_idt &	mode,
		bool	result_is_used,
		bool	address_taken
	)

protected

Definition at line 712 of file goto_convert_side_effect.cpp.

◆ remove_statement_expression()

goto_convertt::clean_expr_resultt goto_convertt::remove_statement_expression	(	side_effect_exprt &	expr,
		const irep_idt &	mode,
		bool	result_is_used
	)

protected

Definition at line 559 of file goto_convert_side_effect.cpp.

◆ remove_temporary_object()

goto_convertt::clean_expr_resultt goto_convertt::remove_temporary_object ( side_effect_exprt & expr )

protected

Definition at line 515 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 419 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 366 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,
		std::optional< node_indext >	end_index = `{}`,
		std::optional< 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 280 of file goto_convert_exceptions.cpp.

Member Data Documentation

◆ lifetime

lifetimet goto_convertt::lifetime = lifetimet::STATIC_GLOBAL

protected

Definition at line 57 of file goto_convert_class.h.

◆ ns

namespacet goto_convertt::ns

protected

Definition at line 55 of file goto_convert_class.h.

◆ symbol_table

symbol_table_baset& goto_convertt::symbol_table

protected

Definition at line 54 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 56 of file goto_convert_class.h.

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

/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_convert_class.h
/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/builtin_functions.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_asm.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_clean_expr.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_convert.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_convert_exceptions.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_convert_function_call.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/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

◆ declaration_hop_instrumentationt

◆ gotost

◆ labelst

Constructor & Destructor Documentation

◆ goto_convertt()

◆ ~goto_convertt()

Member Function Documentation

◆ assignment_lhs_needs_temporary()

◆ build_declaration_hops()

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

◆ do_array_equal()

◆ do_array_op()

◆ do_atomic_begin()

◆ do_atomic_end()

◆ do_cpp_new()

◆ do_create_thread()

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