#include <goto_convert_class.h>

Inheritance diagram for goto_convertt:

Classes
struct	targetst
struct	break_continue_targetst
struct	break_switch_targetst
struct	throw_targett

Public Member Functions
void	goto_convert (const codet &code, goto_programt &dest)
	goto_convertt (contextt &_context, optionst &_options)

Static Public Member Functions
static bool	is_atomic_symbol (const exprt &expr, const namespacet &ns)
	Returns true iff `expr` is a direct reference to a C11 _Atomic variable.
static bool	has_atomic_read (const exprt &expr, const namespacet &ns)
	Returns true iff `expr` contains a direct read of any C11 _Atomic variable (does not recurse into address_of).

Protected Types
typedef std::vector< codet >	destructor_stackt
typedef std::map< irep_idt, std::pair< goto_programt::targett, destructor_stackt > >	labelst
typedef std::list< std::pair< goto_programt::targett, destructor_stackt > >	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
typedef std::map< goto_programt::targett, destructor_stackt >	case_stackst

Protected Member Functions
void	goto_convert_rec (const codet &code, goto_programt &dest)
void	new_name (symbolt &symbol)
symbolt &	new_tmp_symbol (const typet &type)
symbolt &	new_cftest_symbol (const typet &type)
void	make_temp_symbol (exprt &expr, goto_programt &dest)
void	guard_program (const guard2tc &guard, goto_programt &dest)
void	remove_sideeffects (exprt &expr, goto_programt &dest, bool result_is_used=true)
void	remove_sideeffects (expr2tc &expr, goto_programt &dest, bool result_is_used=true)
void	remove_condition_sideeffects (exprt &cond, goto_programt &dest)
	Lowers the condition of an if, loop, for or switch statement, a full-expression whose temporaries are destroyed before the branch ([class.temporary]/4).
void	flatten_contract_clause (exprt &clause, goto_programt &dest)
	Recursively flatten a (possibly nested) &&/\|\| tree forming a contract clause, hoisting side effects (e.g.
void	address_of_replace_objects (exprt &expr, goto_programt &dest)
bool	rewrite_vla_decl (typet &var_type, goto_programt &dest)
bool	rewrite_vla_decl_size (exprt &size, goto_programt &dest)
void	generate_dynamic_size_vla (exprt &var, const locationt &loc, goto_programt &dest, bool allow_zero_size=false)
bool	has_sideeffect (const exprt &expr)
bool	has_sideeffect (const expr2tc &expr)
bool	has_destructible_sideeffect (const exprt &expr)
	True if lowering expr may create a temporary with a destructor.
bool	splits_and_condition (const exprt &cond)
void	remove_sideeffects_for_quantifier_body (exprt &body, const std::set< irep_idt > &bound_vars, goto_programt &dest)
void	inline_calls_in_quantifier_body (exprt &expr, unsigned depth)
	Inline calls to pure single-return functions occurring under a quantifier binder, so that the bound variable stays visible in the body for replace_name_in_body() in smt_solver.cpp.
bool	try_inline_pure_call (const symbolt &fsym, const exprt &call, exprt &out)
	Build the inlined form of `call` to `fsym:` the callee's body must be local declarations with initializers followed by a single return <expr>;.
bool	summarize_pure_call (const symbolt &fsym, const exprt &call, exprt &out)
const exprt *	find_sideeffect_on_bound_var (const exprt &expr, const std::set< irep_idt > &bound_vars)
	Find a side effect that mentions one of `bound_vars`.
void	skolemize_asserted_foralls (exprt &expr, goto_programt &dest)
	In an assertion, a __ESBMC_forall in positive polarity is equivalent to its body over a fresh unconstrained variable: assert(forall x.
void	convert_quantifier_calls (exprt &expr)
void	remove_assignment (exprt &expr, goto_programt &dest, bool result_is_used)
void	remove_post (exprt &expr, goto_programt &dest, bool result_is_used)
void	remove_pre (exprt &expr, goto_programt &dest, bool result_is_used)
void	remove_function_call (exprt &expr, goto_programt &dest, bool result_is_used)
void	remove_cpp_new (exprt &expr, goto_programt &dest, bool result_is_used)
void	remove_cpp_delete (exprt &expr, goto_programt &dest)
void	remove_operand_sideeffects (exprt &expr, goto_programt &dest)
	Remove the side effects of `expr's` operands.
void	drop_destructor (const symbol_exprt &object, std::size_t from)
	Unschedule the destructor call on `object` among the scope-exit entries pushed since the stack held `from` of them.
void	remove_temporary_object (exprt &expr, goto_programt &dest)
void	remove_statement_expression (exprt &expr, goto_programt &dest, bool result_is_used)
void	remove_gcc_conditional_expression (exprt &expr, goto_programt &dest)
virtual void	do_cpp_new (const exprt &lhs, const exprt &rhs, goto_programt &dest)
void	cpp_new_at (const exprt &lhs, const exprt &placement, const locationt &location, goto_programt &dest)
void	cpp_new_initializer (const exprt &lhs, const exprt &rhs, const exprt &elem_count, goto_programt &dest)
void	cpp_new_zero_fill (const exprt &lhs, const exprt &rhs, const exprt &elem_count, goto_programt &dest)
void	cpp_new_store_element (const exprt &base, const exprt &offset, const exprt &init, const locationt &location, const exprt &built, code_blockt &out)
bool	cpp_new_init_list (const exprt &lhs, const exprt &rhs, const exprt &init, const exprt &elem_count, const exprt &built, code_blockt &out)
void	convert_cpp_new_elements (const exprt &base, const exprt &built, const codet &construction, goto_programt &dest)
bool	user_code_throws ()
virtual void	do_function_call (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, const locationt &location, goto_programt &dest)
virtual void	do_function_call_if (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
bool	drop_inactive_contract_clause (bool is_clause) const
	True when a contract clause should be dropped: no contract mode is active, so the clause states nothing.
virtual void	do_function_call_symbol (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
virtual void	do_function_call_dereference (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void	convert_block (const codet &code, goto_programt &dest)
void	convert_controlled (const codet &code, goto_programt &dest)
void	convert_decl (const codet &code, goto_programt &dest)
void	discard_comma_operands (exprt &initializer, goto_programt &dest)
	A comma's left operands are discarded-value expressions and its right operand is its result ([expr.comma]/1), so that operand initialises the variable: a class prvalue there is the variable, not a copied temporary.
void	remove_comma_operand (exprt &operand, goto_programt &dest)
	A comma's operand is a discarded-value expression ([expr.comma]/1), but a temporary object it creates lives until the end of the enclosing full-expression ([class.temporary]/4).
void	destroy_comma_operand_temporaries (std::size_t stack_size, const locationt &location, goto_programt &dest)
	A reference declaration keeps its initializer's temporaries to the end of the scope, but those of a discarded comma operand still die with it.
void	convert_decl_initializer (const exprt &var, exprt &initializer, const codet &new_code, const symbolt &s, goto_programt &dest)
	Lower the initializer of a declaration into `dest`.
bool	construct_in_place (const exprt &object, const exprt &initializer, goto_programt &dest)
	Construct `object` from `initializer` directly when it is a class temporary: a constructor call retargeted at `object`, or a call returning by value made with `object` as its lhs.
void	remove_initializer_sideeffects (const exprt &object, exprt &initializer, goto_programt &dest)
	Remove the side effects of `initializer`, the value of `object`.
void	convert_dynamic_static_init (const codet &decl, const symbolt &s, const symbolt &guard, goto_programt &dest)
	A C++ function-local static with a dynamic initializer is initialized the first time control passes its declaration, and concurrent callers wait for it ([stmt.dcl]/3): atomic { if (!guard) { init; guard = 1; } }.
void	construct_array_elements (const exprt &base, const typet &type, const side_effect_expr_function_callt &ctor, goto_programt &dest)
	The frontend gives an array of a class one constructor call; every element is constructed by it, in increasing index order ([dcl.init]/7).
void	schedule_array_element_destructors (const exprt &base, const typet &type)
	Push a destructor call for every element of an array of class objects, recursing through nested array types so a multi-dimensional array reaches its leaves.
void	convert_decl_block (const codet &code, goto_programt &dest)
void	convert_expression (const codet &code, goto_programt &dest)
void	convert_assign (const code_assignt &code, goto_programt &dest)
void	convert_assign_atomic (const exprt &lhs, const exprt &rhs, const locationt &location, goto_programt &dest)
void	convert_assign_rmw_atomic (const exprt &lhs, const exprt &rhs, const locationt &location, goto_programt &dest)
void	convert_cpp_delete (const codet &code, goto_programt &dest)
void	convert_for (const codet &code, goto_programt &dest)
void	convert_while (const codet &code, goto_programt &dest)
void	convert_dowhile (const codet &code, goto_programt &dest)
void	convert_assume (const codet &code, goto_programt &dest)
void	convert_assert (const codet &code, goto_programt &dest)
bool	emits_assert (const locationt &location) const
void	assume_if_ends_path (const expr2tc &guard, const locationt &location, goto_programt &dest)
void	convert_switch (const codet &code, goto_programt &dest)
void	convert_break (const code_breakt &code, goto_programt &dest)
void	convert_return (const code_returnt &code, goto_programt &dest)
void	remove_return_value_sideeffects (exprt &value, goto_programt &dest)
void	convert_continue (const code_continuet &code, goto_programt &dest)
void	convert_ifthenelse (const codet &code, goto_programt &dest)
void	convert_init (const codet &code, goto_programt &dest)
void	convert_goto (const codet &code, goto_programt &dest)
void	convert_skip (const codet &code, goto_programt &dest)
void	convert_non_deterministic_goto (const codet &code, goto_programt &dest)
void	convert_label (const code_labelt &code, goto_programt &dest)
void	convert_switch_case (const code_switch_caset &code, goto_programt &dest)
void	convert_function_call (const code_function_callt &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 (const codet &code, goto_programt &dest)
void	copy (const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void	convert_full_expression (const codet &code, goto_programt &dest)
	Converts a statement that is a full-expression ([class.temporary]/4), so the temporaries it creates are destroyed when it ends.
bool	destroy_full_expression_temporaries (std::size_t stack_size, const locationt &, goto_programt &dest)
	Emits the scope-exit entries pushed above stack_size when one of them is a destructor call, as the temporaries of a full-expression; plain DEADs of C temporaries keep block scope.
std::size_t	keep_reference_member_temporaries (const exprt &initializer, std::size_t stack_size)
	A temporary bound to a reference member of a declared aggregate lives as long as the aggregate ([class.temporary]/6).
void	unwind_destructor_stack (const locationt &, std::size_t stack_size, goto_programt &dest)
void	unwind_destructor_stack (const locationt &, std::size_t stack_size, goto_programt &dest, destructor_stackt &stack)
void	declare_skipped_locals (const destructor_stackt &stack, std::size_t from, const locationt &location, goto_programt &dest)
	Declares the locals `stack` holds past its first `from` entries: a jump to where `stack` is live skips their declarations.
goto_programt::targett	case_entry (goto_programt::targett target, std::size_t switch_stack_size, const locationt &location, goto_programt &stubs)
	Where a switch dispatch jumps to reach `target:` the target itself, or a stub in `stubs` that first declares the locals the jump skips.
void	kill_condition_temporaries (std::size_t stack_size, const locationt &location, goto_programt &branch, goto_programt &exit)
	End a loop condition's temporaries, pushed since `stack_size`, on both edges of its `branch`, so each iteration's instance dies in that iteration (#9150): after `branch`, and ahead of the break target that starts `exit`, where the branch's jumps to it now land.
void	guard_arm_destructors (exprt &cond, std::size_t true_size, std::size_t false_size, const locationt &location, goto_programt &dest)
void	record_exception_unwind (goto_programt::instructiont &call)
	Attach to `call` the cleanup an exception leaving it runs: the automatic objects constructed since the nearest enclosing try, newest first ([except.ctor]/1), as convert_throw unwinds for a throw in this function.
void	convert_catch (const codet &code, goto_programt &dest)
void	convert_throw (const exprt &expr, goto_programt &dest)
void	finish_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.
void	case_guard (const exprt &value, const caset &case_op, exprt &dest)
void	generate_ifthenelse (const exprt &cond, goto_programt &true_case, goto_programt &false_case, const locationt &location, goto_programt &dest)
	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 locationt &location, goto_programt &dest)
void	generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, const locationt &location, goto_programt &dest)
void	emit_assert_fail_noreturn (const locationt &location, goto_programt &dest)
bool	lower_discarded_short_circuit (exprt &expr, goto_programt &dest, bool result_is_used)
	Lower a value-discarding A && B as if (A) B;, A \|\| B as if (!A) B;.
void	rewrite_short_circuit_as_ternary (exprt &expr)
	Rebuild A && B as A ?
void	do_assert_fail (const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &base_name, std::size_t arity, std::size_t expr_arg)
void	do_abort (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_atomic_begin (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_atomic_end (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_create_thread (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_malloc (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_realloc (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_alloca (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_free (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_sync (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_exit (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	do_printf (const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest, const std::string &bs_name)
void	do_operator_new (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
	Lower a call to ::operator new(n) into a cpp_new side effect.
void	do_mem (bool is_malloc, const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void	get_alloc_size (typet &alloc_type, exprt &alloc_size)

Static Protected Member Functions
static void	replace_new_object (const exprt &object, exprt &dest)
static bool	is_destructor_entry (const codet &entry)
	A destructor call on the destructor stack, possibly guarded by guard_arm_destructors; the other entries are DEADs.
static exprt	case_label (const exprt &lo, const exprt &hi)
static void	collect_operands (const exprt &expr, const irep_idt &id, std::list< exprt > &dest)

Protected Attributes
contextt &	context
optionst &	options
namespacet	ns
symbol_generator	tmp_symbol
bool	in_short_circuit = false
std::map< std::string, std::string >	summary_reject_reasons
std::optional< bool >	user_code_throws_cache
std::set< irep_idt >	comma_operand_temporaries
	Temporaries created by a comma's discarded operands.
struct goto_convertt::targetst	targets

Member Typedef Documentation

◆ case_stackst

typedef std::map<goto_programt::targett, destructor_stackt> goto_convertt::case_stackst

protected

◆ cases_mapt

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

protected

◆ casest

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

protected

◆ caset

typedef exprt::operandst goto_convertt::caset

protected

◆ computed_gotost

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

protected

◆ destructor_stackt

typedef std::vector<codet> goto_convertt::destructor_stackt

protected

◆ gotost

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

protected

◆ labelst

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

protected

Constructor & Destructor Documentation

◆ goto_convertt()

goto_convertt::goto_convertt	(	contextt &	_context,
		optionst &	_options )

inline

Member Function Documentation

◆ address_of_replace_objects()

void goto_convertt::address_of_replace_objects	(	exprt &	expr,
		goto_programt &	dest )

protected

◆ assume_if_ends_path()

void goto_convertt::assume_if_ends_path	(	const expr2tc &	guard,
		const locationt &	location,
		goto_programt &	dest )

protected

◆ case_entry()

goto_programt::targett goto_convertt::case_entry	(	goto_programt::targett	target,
		std::size_t	switch_stack_size,
		const locationt &	location,
		goto_programt &	stubs )

protected

Where a switch dispatch jumps to reach target: the target itself, or a stub in stubs that first declares the locals the jump skips.

◆ case_guard()

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

protected

◆ case_label()

exprt goto_convertt::case_label	(	const exprt &	lo,
		const exprt &	hi )

staticprotected

◆ collect_operands()

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

staticprotected

◆ construct_array_elements()

void goto_convertt::construct_array_elements	(	const exprt &	base,
		const typet &	type,
		const side_effect_expr_function_callt &	ctor,
		goto_programt &	dest )

protected

The frontend gives an array of a class one constructor call; every element is constructed by it, in increasing index order ([dcl.init]/7).

◆ construct_in_place()

bool goto_convertt::construct_in_place	(	const exprt &	object,
		const exprt &	initializer,
		goto_programt &	dest )

protected

Construct object from initializer directly when it is a class temporary: a constructor call retargeted at object, or a call returning by value made with object as its lhs.

Constructing the temporary and copying it would leave it with its own scope-exit destructor, a second destructor for what is semantically one object (github #2306). Returns false, emitting nothing, for any other initializer.

◆ convert()

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

protected

◆ convert_assert()

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

protected

◆ convert_assign()

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

protected

◆ convert_assign_atomic()

void goto_convertt::convert_assign_atomic	(	const exprt &	lhs,
		const exprt &	rhs,
		const locationt &	location,
		goto_programt &	dest )

protected

◆ convert_assign_rmw_atomic()

void goto_convertt::convert_assign_rmw_atomic	(	const exprt &	lhs,
		const exprt &	rhs,
		const locationt &	location,
		goto_programt &	dest )

protected

◆ convert_assume()

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

protected

◆ convert_atomic_begin()

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

protected

◆ convert_atomic_end()

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

protected

◆ convert_block()

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

protected

◆ convert_break()

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

protected

◆ convert_catch()

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

protected

◆ convert_continue()

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

protected

◆ convert_controlled()

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

protected

◆ convert_cpp_delete()

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

protected

◆ convert_cpp_new_elements()

void goto_convertt::convert_cpp_new_elements	(	const exprt &	base,
		const exprt &	built,
		const codet &	construction,
		goto_programt &	dest )

protected

◆ convert_decl()

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

protected

◆ convert_decl_block()

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

protected

◆ convert_decl_initializer()

void goto_convertt::convert_decl_initializer	(	const exprt &	var,
		exprt &	initializer,
		const codet &	new_code,
		const symbolt &	s,
		goto_programt &	dest )

protected

Lower the initializer of a declaration into dest.

Kept out of convert_decl so that neither exceeds the complexity gate.

◆ convert_dowhile()

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

protected

◆ convert_dynamic_static_init()

void goto_convertt::convert_dynamic_static_init	(	const codet &	decl,
		const symbolt &	s,
		const symbolt &	guard,
		goto_programt &	dest )

protected

A C++ function-local static with a dynamic initializer is initialized the first time control passes its declaration, and concurrent callers wait for it ([stmt.dcl]/3): atomic { if (!guard) { init; guard = 1; } }.

The guard is set after the initializer, so one that exits by an exception is retried. The frontend creates guard only for such a static.

◆ convert_expression()

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

protected

◆ convert_for()

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

protected

◆ convert_full_expression()

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

protected

Converts a statement that is a full-expression ([class.temporary]/4), so the temporaries it creates are destroyed when it ends.

◆ convert_function_call()

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

protected

◆ convert_goto()

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

protected

◆ convert_ifthenelse()

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

protected

◆ convert_init()

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

protected

◆ convert_label()

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

protected

◆ convert_non_deterministic_goto()

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

protected

◆ convert_quantifier_calls()

void goto_convertt::convert_quantifier_calls ( exprt & expr )

protected

◆ convert_return()

void goto_convertt::convert_return	(	const code_returnt &	code,
		goto_programt &	dest )

protected

◆ convert_skip()

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

protected

◆ convert_switch()

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

protected

◆ convert_switch_case()

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

protected

◆ convert_throw()

void goto_convertt::convert_throw	(	const exprt &	expr,
		goto_programt &	dest )

protected

◆ convert_while()

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

protected

◆ copy()

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

protected

◆ cpp_new_at()

void goto_convertt::cpp_new_at	(	const exprt &	lhs,
		const exprt &	placement,
		const locationt &	location,
		goto_programt &	dest )

protected

◆ cpp_new_init_list()

bool goto_convertt::cpp_new_init_list	(	const exprt &	lhs,
		const exprt &	rhs,
		const exprt &	init,
		const exprt &	elem_count,
		const exprt &	built,
		code_blockt &	out )

protected

◆ cpp_new_initializer()

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

protected

◆ cpp_new_store_element()

void goto_convertt::cpp_new_store_element	(	const exprt &	base,
		const exprt &	offset,
		const exprt &	init,
		const locationt &	location,
		const exprt &	built,
		code_blockt &	out )

protected

◆ cpp_new_zero_fill()

void goto_convertt::cpp_new_zero_fill	(	const exprt &	lhs,
		const exprt &	rhs,
		const exprt &	elem_count,
		goto_programt &	dest )

protected

◆ declare_skipped_locals()

void goto_convertt::declare_skipped_locals	(	const destructor_stackt &	stack,
		std::size_t	from,
		const locationt &	location,
		goto_programt &	dest )

protected

Declares the locals stack holds past its first from entries: a jump to where stack is live skips their declarations.

◆ destroy_comma_operand_temporaries()

void goto_convertt::destroy_comma_operand_temporaries	(	std::size_t	stack_size,
		const locationt &	location,
		goto_programt &	dest )

protected

A reference declaration keeps its initializer's temporaries to the end of the scope, but those of a discarded comma operand still die with it.

◆ destroy_full_expression_temporaries()

bool goto_convertt::destroy_full_expression_temporaries	(	std::size_t	stack_size,
		const locationt &	location,
		goto_programt &	dest )

protected

Emits the scope-exit entries pushed above stack_size when one of them is a destructor call, as the temporaries of a full-expression; plain DEADs of C temporaries keep block scope.

◆ discard_comma_operands()

void goto_convertt::discard_comma_operands	(	exprt &	initializer,
		goto_programt &	dest )

protected

A comma's left operands are discarded-value expressions and its right operand is its result ([expr.comma]/1), so that operand initialises the variable: a class prvalue there is the variable, not a copied temporary.

◆ do_abort()

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

protected

◆ do_alloca()

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

protected

◆ do_assert_fail()

void goto_convertt::do_assert_fail	(	const exprt &	function,
		const exprt::operandst &	arguments,
		goto_programt &	dest,
		const irep_idt &	base_name,
		std::size_t	arity,
		std::size_t	expr_arg )

protected

◆ do_atomic_begin()

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

protected

◆ do_atomic_end()

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

protected

◆ do_cpp_new()

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

protectedvirtual

◆ do_create_thread()

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

protected

◆ do_exit()

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

protected

◆ do_free()

void goto_convertt::do_free	(	const exprt &	lhs,
		const exprt &	rhs,
		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,
		const locationt &	location,
		goto_programt &	dest )

protectedvirtual

◆ do_function_call_dereference()

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

protectedvirtual

◆ do_function_call_if()

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

protectedvirtual

◆ do_function_call_symbol()

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

protectedvirtual

◆ do_malloc()

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

protected

◆ do_mem()

void goto_convertt::do_mem	(	bool	is_malloc,
		const exprt &	lhs,
		const exprt &	rhs,
		const exprt::operandst &	arguments,
		goto_programt &	dest )

protected

◆ do_operator_new()

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

protected

Lower a call to ::operator new(n) into a cpp_new side effect.

Kept out of do_function_call_symbol, which is already over the complexity gate.

◆ do_printf()

void goto_convertt::do_printf	(	const exprt &	lhs,
		const exprt &	rhs,
		const exprt::operandst &	arguments,
		goto_programt &	dest,
		const std::string &	bs_name )

protected

◆ do_realloc()

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

protected

◆ do_sync()

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

protected

◆ drop_destructor()

void goto_convertt::drop_destructor	(	const symbol_exprt &	object,
		std::size_t	from )

protected

Unschedule the destructor call on object among the scope-exit entries pushed since the stack held from of them.

◆ drop_inactive_contract_clause()

bool goto_convertt::drop_inactive_contract_clause ( bool is_clause ) const

protected

True when a contract clause should be dropped: no contract mode is active, so the clause states nothing.

Split out so the clause handling adds no branching to do_function_call_symbol.

◆ emit_assert_fail_noreturn()

void goto_convertt::emit_assert_fail_noreturn	(	const locationt &	location,
		goto_programt &	dest )

protected

◆ emits_assert()

bool goto_convertt::emits_assert ( const locationt & location ) const

protected

◆ find_sideeffect_on_bound_var()

const exprt * goto_convertt::find_sideeffect_on_bound_var	(	const exprt &	expr,
		const std::set< irep_idt > &	bound_vars )

protected

Find a side effect that mentions one of bound_vars.

Such a side effect cannot be hoisted soundly: the temp would freeze the bound variable at its pre-quantifier value. Quantifier intrinsic calls are skipped, with their own bound variable added while scanning their body.

◆ finish_gotos()

void goto_convertt::finish_gotos ( goto_programt & dest )

protected

◆ flatten_contract_clause()

void goto_convertt::flatten_contract_clause	(	exprt &	clause,
		goto_programt &	dest )

protected

Recursively flatten a (possibly nested) &&/|| tree forming a contract clause, hoisting side effects (e.g.

__ESBMC_old()) at the leaves while preserving the boolean structure.

The earlier path processed only the top-level && or || chain, calling remove_sideeffects() on each part. For a disjunctive clause whose disjuncts are themselves && chains containing __ESBMC_old(), that lowered a whole nested && at once and silently dropped its leading conjuncts (#6298). Recursing so remove_sideeffects() only ever sees a leaf keeps every conjunct and still snapshots __ESBMC_old() unconditionally at function entry.

◆ generate_conditional_branch() [1/2]

void goto_convertt::generate_conditional_branch	(	const exprt &	guard,
		goto_programt::targett	target_true,
		const locationt &	location,
		goto_programt &	dest )

protected

◆ 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 locationt &	location,
		goto_programt &	dest )

protected

◆ generate_dynamic_size_vla()

void goto_convertt::generate_dynamic_size_vla	(	exprt &	var,
		const locationt &	loc,
		goto_programt &	dest,
		bool	allow_zero_size = false )

protected

◆ generate_ifthenelse()

void goto_convertt::generate_ifthenelse	(	const exprt &	cond,
		goto_programt &	true_case,
		goto_programt &	false_case,
		const locationt &	location,
		goto_programt &	dest )

protected

if(guard) true_case; else false_case;

◆ get_alloc_size()

void goto_convertt::get_alloc_size	(	typet &	alloc_type,
		exprt &	alloc_size )

protected

◆ goto_convert()

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

◆ goto_convert_rec()

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

protected

◆ guard_arm_destructors()

void goto_convertt::guard_arm_destructors	(	exprt &	cond,
		std::size_t	true_size,
		std::size_t	false_size,
		const locationt &	location,
		goto_programt &	dest )

protected

◆ guard_program()

void goto_convertt::guard_program	(	const guard2tc &	guard,
		goto_programt &	dest )

protected

◆ has_atomic_read()

bool goto_convertt::has_atomic_read	(	const exprt &	expr,
		const namespacet &	ns )

static

Returns true iff expr contains a direct read of any C11 _Atomic variable (does not recurse into address_of).

Returns true if expr contains a direct read of any C11 _Atomic variable (stops early at the first match; does not recurse into address_of).

Shared with the IREP2-native body dispatcher so it gates an assignment exactly as convert_assign does.

◆ has_destructible_sideeffect()

bool goto_convertt::has_destructible_sideeffect ( const exprt & expr )

protected

True if lowering expr may create a temporary with a destructor.

◆ has_sideeffect() [1/2]

bool goto_convertt::has_sideeffect ( const expr2tc & expr )

protected

◆ has_sideeffect() [2/2]

bool goto_convertt::has_sideeffect ( const exprt & expr )

protected

◆ inline_calls_in_quantifier_body()

void goto_convertt::inline_calls_in_quantifier_body	(	exprt &	expr,
		unsigned	depth )

protected

Inline calls to pure single-return functions occurring under a quantifier binder, so that the bound variable stays visible in the body for replace_name_in_body() in smt_solver.cpp.

Hoisting such a call to a temp would freeze the bound variable at its pre-quantifier value, detaching the body from the binder (GitHub discussion #6100). Nested quantifier intrinsic calls are recursed into but left intact; calls that cannot be inlined are left in place.

◆ is_atomic_symbol()

bool goto_convertt::is_atomic_symbol	(	const exprt &	expr,
		const namespacet &	ns )

static

Returns true iff expr is a direct reference to a C11 _Atomic variable.

Returns true if expr is a direct reference to a C11 _Atomic-qualified variable (symbol with the "#atomic" flag set on its type).

◆ is_destructor_entry()

bool goto_convertt::is_destructor_entry ( const codet & entry )

staticprotected

A destructor call on the destructor stack, possibly guarded by guard_arm_destructors; the other entries are DEADs.

◆ keep_reference_member_temporaries()

std::size_t goto_convertt::keep_reference_member_temporaries	(	const exprt &	initializer,
		std::size_t	stack_size )

protected

A temporary bound to a reference member of a declared aggregate lives as long as the aggregate ([class.temporary]/6).

Moves its scope-exit entries to the bottom of those pushed above stack_size and returns the stack size the full-expression's other temporaries are destroyed down to.

◆ kill_condition_temporaries()

void goto_convertt::kill_condition_temporaries	(	std::size_t	stack_size,
		const locationt &	location,
		goto_programt &	branch,
		goto_programt &	exit )

protected

End a loop condition's temporaries, pushed since stack_size, on both edges of its branch, so each iteration's instance dies in that iteration (#9150): after branch, and ahead of the break target that starts exit, where the branch's jumps to it now land.

Leaves everything alone if one of them has a destructor.

◆ lower_discarded_short_circuit()

bool goto_convertt::lower_discarded_short_circuit	(	exprt &	expr,
		goto_programt &	dest,
		bool	result_is_used )

protected

Lower a value-discarding A && B as if (A) B;, A || B as if (!A) B;.

The ternary rebuild encodes the same control flow but materialises the discarded boolean, hiding the lone-assert(false) branch body that generate_ifthenelse folds. MSVC's <assert.h> spells an assertion that way – (void)((!!(e)) || (_wassert(...), 0)) – so unfolded it stays ASSERT 0 under !e rather than the ASSERT e glibc and Darwin produce, and a constant-false claim holds on no path, defeating any consumer that asks whether it can (#7585).

False, expr untouched, where the rewrite does not apply: value used, tail side-effect-free (its evaluation may still raise a claim the ternary keeps), or condition coverage / witness validation needs the original operands – the gates generate_ifthenelse applies to its own folds.

◆ make_temp_symbol()

void goto_convertt::make_temp_symbol	(	exprt &	expr,
		goto_programt &	dest )

protected

◆ new_cftest_symbol()

symbolt & goto_convertt::new_cftest_symbol ( const typet & type )

protected

◆ new_name()

void goto_convertt::new_name ( symbolt & symbol )

protected

◆ new_tmp_symbol()

symbolt & goto_convertt::new_tmp_symbol ( const typet & type )

protected

◆ 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

◆ record_exception_unwind()

void goto_convertt::record_exception_unwind ( goto_programt::instructiont & call )

protected

Attach to call the cleanup an exception leaving it runs: the automatic objects constructed since the nearest enclosing try, newest first ([except.ctor]/1), as convert_throw unwinds for a throw in this function.

remove_exceptions emits it on the call's exceptional edge. The object a constructor call builds is left out: it was never constructed.

◆ remove_assignment()

void goto_convertt::remove_assignment	(	exprt &	expr,
		goto_programt &	dest,
		bool	result_is_used )

protected

◆ remove_comma_operand()

void goto_convertt::remove_comma_operand	(	exprt &	operand,
		goto_programt &	dest )

protected

A comma's operand is a discarded-value expression ([expr.comma]/1), but a temporary object it creates lives until the end of the enclosing full-expression ([class.temporary]/4).

Lowering it as a used value leaves its scope-exit entries for the full-expression to emit.

◆ remove_condition_sideeffects()

void goto_convertt::remove_condition_sideeffects	(	exprt &	cond,
		goto_programt &	dest )

protected

Lowers the condition of an if, loop, for or switch statement, a full-expression whose temporaries are destroyed before the branch ([class.temporary]/4).

◆ remove_cpp_delete()

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

protected

◆ remove_cpp_new()

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

protected

◆ remove_function_call()

void goto_convertt::remove_function_call	(	exprt &	expr,
		goto_programt &	dest,
		bool	result_is_used )

protected

◆ remove_gcc_conditional_expression()

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

protected

◆ remove_initializer_sideeffects()

void goto_convertt::remove_initializer_sideeffects	(	const exprt &	object,
		exprt &	initializer,
		goto_programt &	dest )

protected

Remove the side effects of initializer, the value of object.

A class element of a braced list is a subobject of object and is initialised in place ([dcl.init.aggr]/4, [dcl.init]/17.6.1).

◆ remove_operand_sideeffects()

void goto_convertt::remove_operand_sideeffects	(	exprt &	expr,
		goto_programt &	dest )

protected

Remove the side effects of expr's operands.

A temporary initialising an aggregate's element is that element ([dcl.init.aggr]/4), destroyed with the aggregate rather than on its own.

◆ remove_post()

void goto_convertt::remove_post	(	exprt &	expr,
		goto_programt &	dest,
		bool	result_is_used )

protected

◆ remove_pre()

void goto_convertt::remove_pre	(	exprt &	expr,
		goto_programt &	dest,
		bool	result_is_used )

protected

◆ remove_return_value_sideeffects()

void goto_convertt::remove_return_value_sideeffects	(	exprt &	value,
		goto_programt &	dest )

protected

◆ remove_sideeffects() [1/2]

void goto_convertt::remove_sideeffects	(	expr2tc &	expr,
		goto_programt &	dest,
		bool	result_is_used = true )

protected

◆ remove_sideeffects() [2/2]

void goto_convertt::remove_sideeffects	(	exprt &	expr,
		goto_programt &	dest,
		bool	result_is_used = true )

protected

◆ remove_sideeffects_for_quantifier_body()

void goto_convertt::remove_sideeffects_for_quantifier_body	(	exprt &	body,
		const std::set< irep_idt > &	bound_vars,
		goto_programt &	dest )

protected

◆ remove_statement_expression()

void goto_convertt::remove_statement_expression	(	exprt &	expr,
		goto_programt &	dest,
		bool	result_is_used )

protected

◆ remove_temporary_object()

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

protected

◆ replace_new_object()

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

staticprotected

◆ rewrite_short_circuit_as_ternary()

void goto_convertt::rewrite_short_circuit_as_ternary ( exprt & expr )

protected

Rebuild A && B as A ?

B : false and A || B as A ? true : B, right to left over the operands, so the generic lowering below handles it.

◆ rewrite_vla_decl()

bool goto_convertt::rewrite_vla_decl	(	typet &	var_type,
		goto_programt &	dest )

protected

◆ rewrite_vla_decl_size()

bool goto_convertt::rewrite_vla_decl_size	(	exprt &	size,
		goto_programt &	dest )

protected

◆ schedule_array_element_destructors()

void goto_convertt::schedule_array_element_destructors	(	const exprt &	base,
		const typet &	type )

protected

Push a destructor call for every element of an array of class objects, recursing through nested array types so a multi-dimensional array reaches its leaves.

Does nothing for a non-array, an element type without a destructor, or an extent that is not a constant.

◆ skolemize_asserted_foralls()

void goto_convertt::skolemize_asserted_foralls	(	exprt &	expr,
		goto_programt &	dest )

protected

In an assertion, a __ESBMC_forall in positive polarity is equivalent to its body over a fresh unconstrained variable: assert(forall x.

B) fails exactly when some x violates B. When the body keeps a side effect on the bound variable that inlining cannot remove (e.g. a call to a libc model whose body is only linked at the GOTO level), rewrite the binder away so the call is hoisted as an ordinary call on the fresh variable. Bodies the binder path can model are left alone, as are __ESBMC_exists and quantifiers in negative positions (!, ==>, ?:, __ESBMC_assume).

◆ splits_and_condition()

bool goto_convertt::splits_and_condition ( const exprt & cond )

protected

◆ summarize_pure_call()

bool goto_convertt::summarize_pure_call	(	const symbolt &	fsym,
		const exprt &	call,
		exprt &	out )

protected

◆ try_inline_pure_call()

bool goto_convertt::try_inline_pure_call	(	const symbolt &	fsym,
		const exprt &	call,
		exprt &	out )

protected

Build the inlined form of call to fsym: the callee's body must be local declarations with initializers followed by a single return <expr>;.

The declarations and then the actual arguments are substituted into the return expression. Returns false when the callee does not have this shape.

◆ unwind_destructor_stack() [1/2]

void goto_convertt::unwind_destructor_stack	(	const locationt &	location,
		std::size_t	stack_size,
		goto_programt &	dest )

protected

◆ unwind_destructor_stack() [2/2]

void goto_convertt::unwind_destructor_stack	(	const locationt &	location,
		std::size_t	stack_size,
		goto_programt &	dest,
		destructor_stackt &	stack )

protected

◆ user_code_throws()

bool goto_convertt::user_code_throws ( )

protected

Member Data Documentation

◆ comma_operand_temporaries

std::set<irep_idt> goto_convertt::comma_operand_temporaries

protected

Temporaries created by a comma's discarded operands.

◆ context

contextt& goto_convertt::context

protected

◆ in_short_circuit

bool goto_convertt::in_short_circuit = false

protected

◆ ns

namespacet goto_convertt::ns

protected

◆ options

optionst& goto_convertt::options

protected

◆ summary_reject_reasons

std::map<std::string, std::string> goto_convertt::summary_reject_reasons

protected

◆ targets

struct goto_convertt::targetst goto_convertt::targets

protected

◆ tmp_symbol

symbol_generator goto_convertt::tmp_symbol

protected

◆ user_code_throws_cache

std::optional<bool> goto_convertt::user_code_throws_cache

protected

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

src/goto-programs/goto_convert_class.h
src/goto-programs/builtin_functions.cpp
src/goto-programs/goto_convert.cpp
src/goto-programs/goto_function.cpp
src/goto-programs/goto_main.cpp
src/goto-programs/goto_sideeffects.cpp

Classes

Public Member Functions

Static Public Member Functions

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Member Typedef Documentation

◆ case_stackst

◆ cases_mapt

◆ casest

◆ caset

◆ computed_gotost

◆ destructor_stackt

◆ gotost

◆ labelst

Constructor & Destructor Documentation

◆ goto_convertt()

Member Function Documentation

◆ address_of_replace_objects()

◆ assume_if_ends_path()

◆ case_entry()

◆ case_guard()

◆ case_label()

◆ collect_operands()

◆ construct_array_elements()

◆ construct_in_place()

◆ convert()

◆ convert_assert()

◆ convert_assign()

◆ convert_assign_atomic()

◆ convert_assign_rmw_atomic()

◆ convert_assume()

◆ convert_atomic_begin()

◆ convert_atomic_end()

◆ convert_block()

◆ convert_break()

◆ convert_catch()

◆ convert_continue()

◆ convert_controlled()

◆ convert_cpp_delete()

◆ convert_cpp_new_elements()

◆ convert_decl()

◆ convert_decl_block()

◆ convert_decl_initializer()

◆ convert_dowhile()

◆ convert_dynamic_static_init()

◆ convert_expression()

◆ convert_for()

◆ convert_full_expression()

◆ convert_function_call()

◆ convert_goto()

◆ convert_ifthenelse()

◆ convert_init()

◆ convert_label()

◆ convert_non_deterministic_goto()

◆ convert_quantifier_calls()

◆ convert_return()

◆ convert_skip()

◆ convert_switch()

◆ convert_switch_case()

◆ convert_throw()

◆ convert_while()

◆ copy()

◆ cpp_new_at()

◆ cpp_new_init_list()

◆ cpp_new_initializer()

◆ cpp_new_store_element()

◆ cpp_new_zero_fill()

◆ declare_skipped_locals()

◆ destroy_comma_operand_temporaries()

◆ destroy_full_expression_temporaries()

◆ discard_comma_operands()

◆ do_abort()

◆ do_alloca()

◆ do_assert_fail()

◆ do_atomic_begin()

◆ do_atomic_end()

◆ do_cpp_new()

◆ do_create_thread()