#include <goto_program2code.h>

Collaboration diagram for goto_program2codet:

Classes
struct	caset

Public Member Functions
	goto_program2codet (const irep_idt &identifier, const goto_programt &_goto_program, symbol_tablet &_symbol_table, code_blockt &_dest, id_listt &_local_static, id_listt &_type_names, const std::unordered_set< irep_idt > &_typedef_names, std::set< std::string > &_system_headers)

void	operator() ()

Protected Member Functions
void	copy_source_location (goto_programt::const_targett, codet &dst)

void	build_loop_map ()

void	build_dead_map ()

void	scan_for_varargs ()

void	cleanup_code (codet &code, const irep_idt parent_stmt)

void	cleanup_function_call (const exprt &function, code_function_callt::argumentst &arguments)

void	cleanup_code_block (codet &code, const irep_idt parent_stmt)

void	cleanup_code_ifthenelse (codet &code, const irep_idt parent_stmt)

void	cleanup_expr (exprt &expr, bool no_typecast)

void	add_local_types (const typet &type)

void	remove_const (typet &type)

goto_programt::const_targett	convert_instruction (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

void	convert_labels (goto_programt::const_targett target, code_blockt &dest)

goto_programt::const_targett	convert_assign (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

goto_programt::const_targett	convert_assign_varargs (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

void	convert_assign_rec (const code_assignt &assign, code_blockt &dest)

goto_programt::const_targett	convert_set_return_value (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

goto_programt::const_targett	convert_decl (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

goto_programt::const_targett	convert_do_while (goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)

goto_programt::const_targett	convert_goto (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

goto_programt::const_targett	convert_goto_while (goto_programt::const_targett target, goto_programt::const_targett loop_end, code_blockt &dest)

goto_programt::const_targett	convert_goto_switch (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

goto_programt::const_targett	get_cases (goto_programt::const_targett target, goto_programt::const_targett upper_bound, const exprt &switch_var, cases_listt &cases, goto_programt::const_targett &first_target, goto_programt::const_targett &default_target)

bool	set_block_end_points (goto_programt::const_targett upper_bound, const cfg_dominatorst &dominators, cases_listt &cases, std::set< unsigned > &processed_locations)

bool	remove_default (const cfg_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target)

goto_programt::const_targett	convert_goto_if (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

goto_programt::const_targett	convert_goto_break_continue (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

goto_programt::const_targett	convert_goto_goto (goto_programt::const_targett target, code_blockt &dest)

goto_programt::const_targett	convert_start_thread (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

goto_programt::const_targett	convert_throw (goto_programt::const_targett target, code_blockt &dest)

goto_programt::const_targett	convert_catch (goto_programt::const_targett target, goto_programt::const_targett upper_bound, code_blockt &dest)

Protected Attributes
const irep_idt &	func_name

const goto_programt &	goto_program

symbol_tablet &	symbol_table

const namespacet	ns

code_blockt &	toplevel_block

id_listt &	local_static

id_listt &	type_names

const std::unordered_set< irep_idt > &	typedef_names

std::set< std::string > &	system_headers

std::unordered_set< exprt, irep_hash >	va_list_expr

natural_loopst	loops

loopt	loop_map

std::unordered_set< irep_idt >	labels_in_use

dead_mapt	dead_map

loop_last_stackt	loop_last_stack

std::unordered_set< irep_idt >	local_static_set

std::unordered_set< irep_idt >	type_names_set

std::unordered_set< irep_idt >	const_removed

Private Types
typedef std::list< irep_idt >	id_listt

typedef std::map< goto_programt::const_targett, goto_programt::const_targett, goto_programt::target_less_than >	loopt

typedef std::unordered_map< irep_idt, unsigned >	dead_mapt

typedef std::list< std::pair< goto_programt::const_targett, bool > >	loop_last_stackt

typedef std::list< caset >	cases_listt

Detailed Description

Definition at line 22 of file goto_program2code.h.

Member Typedef Documentation

◆ cases_listt

typedef std::list<caset> goto_program2codet::cases_listt

private

Definition at line 50 of file goto_program2code.h.

◆ dead_mapt

typedef std::unordered_map<irep_idt, unsigned> goto_program2codet::dead_mapt

private

Definition at line 30 of file goto_program2code.h.

◆ id_listt

typedef std::list<irep_idt> goto_program2codet::id_listt

private

Definition at line 24 of file goto_program2code.h.

◆ loop_last_stackt

typedef std::list<std::pair<goto_programt::const_targett, bool> > goto_program2codet::loop_last_stackt

private

Definition at line 32 of file goto_program2code.h.

◆ loopt

typedef std::map< goto_programt::const_targett, goto_programt::const_targett, goto_programt::target_less_than> goto_program2codet::loopt

private

Definition at line 29 of file goto_program2code.h.

Constructor & Destructor Documentation

◆ goto_program2codet()

goto_program2codet::goto_program2codet	(	const irep_idt &	identifier,
		const goto_programt &	_goto_program,
		symbol_tablet &	_symbol_table,
		code_blockt &	_dest,
		id_listt &	_local_static,
		id_listt &	_type_names,
		const std::unordered_set< irep_idt > &	_typedef_names,
		std::set< std::string > &	_system_headers
	)

inline

Definition at line 53 of file goto_program2code.h.

Member Function Documentation

◆ add_local_types()

void goto_program2codet::add_local_types ( const typet & type )

protected

Definition at line 1379 of file goto_program2code.cpp.

◆ build_dead_map()

void goto_program2codet::build_dead_map ( )

protected

Definition at line 89 of file goto_program2code.cpp.

◆ build_loop_map()

void goto_program2codet::build_loop_map ( )

protected

Definition at line 53 of file goto_program2code.cpp.

◆ cleanup_code()

void goto_program2codet::cleanup_code	(	codet &	code,
		const irep_idt	parent_stmt
	)

protected

Definition at line 1417 of file goto_program2code.cpp.

◆ cleanup_code_block()

void goto_program2codet::cleanup_code_block	(	codet &	code,
		const irep_idt	parent_stmt
	)

protected

Definition at line 1551 of file goto_program2code.cpp.

◆ cleanup_code_ifthenelse()

void goto_program2codet::cleanup_code_ifthenelse	(	codet &	code,
		const irep_idt	parent_stmt
	)

protected

Definition at line 1685 of file goto_program2code.cpp.

◆ cleanup_expr()

void goto_program2codet::cleanup_expr	(	exprt &	expr,
		bool	no_typecast
	)

protected

Definition at line 1775 of file goto_program2code.cpp.

◆ cleanup_function_call()

void goto_program2codet::cleanup_function_call	(	const exprt &	function,
		code_function_callt::argumentst &	arguments
	)

protected

Definition at line 1517 of file goto_program2code.cpp.

◆ convert_assign()

goto_programt::const_targett goto_program2codet::convert_assign	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 291 of file goto_program2code.cpp.

◆ convert_assign_rec()

void goto_program2codet::convert_assign_rec	(	const code_assignt &	assign,
		code_blockt &	dest
	)

protected

Definition at line 398 of file goto_program2code.cpp.

◆ convert_assign_varargs()

goto_programt::const_targett goto_program2codet::convert_assign_varargs	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 306 of file goto_program2code.cpp.

◆ convert_catch()

goto_programt::const_targett goto_program2codet::convert_catch	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 1369 of file goto_program2code.cpp.

◆ convert_decl()

goto_programt::const_targett goto_program2codet::convert_decl	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 450 of file goto_program2code.cpp.

◆ convert_do_while()

goto_programt::const_targett goto_program2codet::convert_do_while	(	goto_programt::const_targett	target,
		goto_programt::const_targett	loop_end,
		code_blockt &	dest
	)

protected

Definition at line 513 of file goto_program2code.cpp.

◆ convert_goto()

goto_programt::const_targett goto_program2codet::convert_goto	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 538 of file goto_program2code.cpp.

◆ convert_goto_break_continue()

goto_programt::const_targett goto_program2codet::convert_goto_break_continue	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 1112 of file goto_program2code.cpp.

◆ convert_goto_goto()

goto_programt::const_targett goto_program2codet::convert_goto_goto	(	goto_programt::const_targett	target,
		code_blockt &	dest
	)

protected

Definition at line 1183 of file goto_program2code.cpp.

◆ convert_goto_if()

goto_programt::const_targett goto_program2codet::convert_goto_if	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 1035 of file goto_program2code.cpp.

◆ convert_goto_switch()

goto_programt::const_targett goto_program2codet::convert_goto_switch	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 862 of file goto_program2code.cpp.

◆ convert_goto_while()

goto_programt::const_targett goto_program2codet::convert_goto_while	(	goto_programt::const_targett	target,
		goto_programt::const_targett	loop_end,
		code_blockt &	dest
	)

protected

Definition at line 561 of file goto_program2code.cpp.

◆ convert_instruction()

goto_programt::const_targett goto_program2codet::convert_instruction	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 136 of file goto_program2code.cpp.

◆ convert_labels()

void goto_program2codet::convert_labels	(	goto_programt::const_targett	target,
		code_blockt &	dest
	)

protected

Definition at line 246 of file goto_program2code.cpp.

◆ convert_set_return_value()

goto_programt::const_targett goto_program2codet::convert_set_return_value	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 420 of file goto_program2code.cpp.

◆ convert_start_thread()

goto_programt::const_targett goto_program2codet::convert_start_thread	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		code_blockt &	dest
	)

protected

Definition at line 1238 of file goto_program2code.cpp.

◆ convert_throw()

goto_programt::const_targett goto_program2codet::convert_throw	(	goto_programt::const_targett	target,
		code_blockt &	dest
	)

protected

Definition at line 1360 of file goto_program2code.cpp.

◆ copy_source_location()

void goto_program2codet::copy_source_location	(	goto_programt::const_targett	src,
		codet &	dst
	)

protected

Definition at line 1981 of file goto_program2code.cpp.

◆ get_cases()

goto_programt::const_targett goto_program2codet::get_cases	(	goto_programt::const_targett	target,
		goto_programt::const_targett	upper_bound,
		const exprt &	switch_var,
		cases_listt &	cases,
		goto_programt::const_targett &	first_target,
		goto_programt::const_targett &	default_target
	)

protected

Definition at line 651 of file goto_program2code.cpp.

◆ operator()()

void goto_program2codet::operator() ( void )

Definition at line 26 of file goto_program2code.cpp.

◆ remove_const()

void goto_program2codet::remove_const ( typet & type )

protected

Definition at line 1605 of file goto_program2code.cpp.

◆ remove_default()

bool goto_program2codet::remove_default	(	const cfg_dominatorst &	dominators,
		const cases_listt &	cases,
		goto_programt::const_targett	default_target
	)

protected

Definition at line 805 of file goto_program2code.cpp.

◆ scan_for_varargs()

void goto_program2codet::scan_for_varargs ( )

protected

Definition at line 104 of file goto_program2code.cpp.

◆ set_block_end_points()

bool goto_program2codet::set_block_end_points	(	goto_programt::const_targett	upper_bound,
		const cfg_dominatorst &	dominators,
		cases_listt &	cases,
		std::set< unsigned > &	processed_locations
	)

protected

Definition at line 754 of file goto_program2code.cpp.

Member Data Documentation

◆ const_removed

std::unordered_set<irep_idt> goto_program2codet::const_removed

protected

Definition at line 102 of file goto_program2code.h.

◆ dead_map

dead_mapt goto_program2codet::dead_map

protected

Definition at line 98 of file goto_program2code.h.

◆ func_name

const irep_idt& goto_program2codet::func_name

protected

Definition at line 84 of file goto_program2code.h.

◆ goto_program

const goto_programt& goto_program2codet::goto_program

protected

Definition at line 85 of file goto_program2code.h.

◆ labels_in_use

std::unordered_set<irep_idt> goto_program2codet::labels_in_use

protected

Definition at line 97 of file goto_program2code.h.

◆ local_static

id_listt& goto_program2codet::local_static

protected

Definition at line 89 of file goto_program2code.h.

◆ local_static_set

std::unordered_set<irep_idt> goto_program2codet::local_static_set

protected

Definition at line 100 of file goto_program2code.h.

◆ loop_last_stack

loop_last_stackt goto_program2codet::loop_last_stack

protected

Definition at line 99 of file goto_program2code.h.

◆ loop_map

loopt goto_program2codet::loop_map

protected

Definition at line 96 of file goto_program2code.h.

◆ loops

natural_loopst goto_program2codet::loops

protected

Definition at line 95 of file goto_program2code.h.

◆ ns

const namespacet goto_program2codet::ns

protected

Definition at line 87 of file goto_program2code.h.

◆ symbol_table

symbol_tablet& goto_program2codet::symbol_table

protected

Definition at line 86 of file goto_program2code.h.

◆ system_headers

std::set<std::string>& goto_program2codet::system_headers

protected

Definition at line 92 of file goto_program2code.h.

◆ toplevel_block

code_blockt& goto_program2codet::toplevel_block

protected

Definition at line 88 of file goto_program2code.h.

◆ type_names

id_listt& goto_program2codet::type_names

protected

Definition at line 90 of file goto_program2code.h.

◆ type_names_set

std::unordered_set<irep_idt> goto_program2codet::type_names_set

protected

Definition at line 101 of file goto_program2code.h.

◆ typedef_names

const std::unordered_set<irep_idt>& goto_program2codet::typedef_names

protected

Definition at line 91 of file goto_program2code.h.

◆ va_list_expr

std::unordered_set<exprt, irep_hash> goto_program2codet::va_list_expr

protected

Definition at line 93 of file goto_program2code.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/goto_program2code.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/goto_program2code.cpp

Classes

Public Member Functions

Protected Member Functions

Protected Attributes

Private Types

Detailed Description

Member Typedef Documentation

◆ cases_listt

◆ dead_mapt

◆ id_listt

◆ loop_last_stackt

◆ loopt

Constructor & Destructor Documentation

◆ goto_program2codet()

Member Function Documentation

◆ add_local_types()

◆ build_dead_map()

◆ build_loop_map()

◆ cleanup_code()

◆ cleanup_code_block()

◆ cleanup_code_ifthenelse()

◆ cleanup_expr()

◆ cleanup_function_call()

◆ convert_assign()

◆ convert_assign_rec()

◆ convert_assign_varargs()

◆ convert_catch()

◆ convert_decl()

◆ convert_do_while()

◆ convert_goto()

◆ convert_goto_break_continue()

◆ convert_goto_goto()

◆ convert_goto_if()

◆ convert_goto_switch()

◆ convert_goto_while()

◆ convert_instruction()

◆ convert_labels()

◆ convert_set_return_value()

◆ convert_start_thread()

◆ convert_throw()

◆ copy_source_location()

◆ get_cases()

◆ operator()()

◆ remove_const()

◆ remove_default()

◆ scan_for_varargs()

◆ set_block_end_points()

Member Data Documentation

◆ const_removed

◆ dead_map

◆ func_name

◆ goto_program

◆ labels_in_use

◆ local_static

◆ local_static_set

◆ loop_last_stack

◆ loop_map

◆ loops

◆ ns

◆ symbol_table

◆ system_headers

◆ toplevel_block

◆ type_names

◆ type_names_set

◆ typedef_names

◆ va_list_expr