#include <dump_c_class.h>

Collaboration diagram for dump_ct:

Classes
struct	typedef_infot

Public Member Functions
	dump_ct (const goto_functionst &_goto_functions, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &_ns, const irep_idt &mode, const dump_c_configurationt config)

	dump_ct (const goto_functionst &_goto_functions, const bool use_system_headers, const bool use_all_headers, const bool include_harness, const namespacet &_ns, const irep_idt &mode)

virtual	~dump_ct ()=default

void	operator() (std::ostream &out)

Protected Types
typedef std::unordered_set< irep_idt >	convertedt

typedef std::unordered_map< irep_idt, irep_idt >	declared_enum_constants_mapt

typedef std::map< irep_idt, typedef_infot >	typedef_mapt

typedef std::unordered_map< typet, irep_idt, irep_hash >	typedef_typest

typedef std::unordered_map< irep_idt, code_frontend_declt >	local_static_declst

Protected Member Functions
std::string	type_to_string (const typet &type)

std::string	expr_to_string (const exprt &expr)

std::string	make_decl (const irep_idt &identifier, const typet &type)

void	collect_typedefs (const typet &type, bool early)
	Find any typedef names contained in the input type and store their declaration strings in typedef_map for eventual output. More...

void	collect_typedefs_rec (const typet &type, bool early, std::unordered_set< irep_idt > &dependencies)
	Find any typedef names contained in the input type and store their declaration strings in typedef_map for eventual output. More...

void	gather_global_typedefs ()
	Find all global typdefs in the symbol table and store them in typedef_types. More...

void	dump_typedefs (std::ostream &os) const
	Print all typedefs that are not covered via typedef struct xyz { ... More...

void	convert_compound_declaration (const symbolt &symbol, std::ostream &os_body)
	declare compound types More...

void	convert_compound (const typet &type, const typet &unresolved, bool recursive, std::ostream &os)

void	convert_compound (const struct_union_typet &type, const typet &unresolved, bool recursive, std::ostream &os)

void	convert_compound_enum (const typet &type, std::ostream &os)

void	convert_global_variable (const symbolt &symbol, std::ostream &os, local_static_declst &local_static_decls)

void	convert_function_declaration (const symbolt &symbol, const bool skip_main, std::ostream &os_decl, std::ostream &os_body, local_static_declst &local_static_decls)

void	insert_local_static_decls (code_blockt &b, const std::list< irep_idt > &local_static, local_static_declst &local_static_decls, std::list< irep_idt > &type_decls)

void	insert_local_type_decls (code_blockt &b, const std::list< irep_idt > &type_decls)

void	cleanup_expr (exprt &expr)

void	cleanup_type (typet &type)

void	cleanup_decl (code_frontend_declt &decl, std::list< irep_idt > &local_static, std::list< irep_idt > &local_type_decls)

void	cleanup_harness (code_blockt &b)
	Replace CPROVER internal symbols in b by printable values and generate necessary declarations. More...

Static Protected Member Functions
static std::string	indent (const unsigned n)

Protected Attributes
const goto_functionst &	goto_functions

symbol_tablet	copied_symbol_table

const namespacet	ns

const dump_c_configurationt	dump_c_config

const irep_idt	mode

const bool	harness

convertedt	converted_compound

convertedt	converted_global

convertedt	converted_enum

std::set< std::string >	system_headers

system_library_symbolst	system_symbols

declared_enum_constants_mapt	declared_enum_constants

typedef_mapt	typedef_map

typedef_typest	typedef_types

Detailed Description

Definition at line 111 of file dump_c_class.h.

Member Typedef Documentation

◆ convertedt

typedef std::unordered_set<irep_idt> dump_ct::convertedt

protected

Definition at line 163 of file dump_c_class.h.

◆ declared_enum_constants_mapt

typedef std::unordered_map<irep_idt, irep_idt> dump_ct::declared_enum_constants_mapt

protected

Definition at line 170 of file dump_c_class.h.

◆ local_static_declst

typedef std::unordered_map<irep_idt, code_frontend_declt> dump_ct::local_static_declst

protected

Definition at line 238 of file dump_c_class.h.

◆ typedef_mapt

typedef std::map<irep_idt, typedef_infot> dump_ct::typedef_mapt

protected

Definition at line 186 of file dump_c_class.h.

◆ typedef_typest

typedef std::unordered_map<typet, irep_idt, irep_hash> dump_ct::typedef_typest

protected

Definition at line 188 of file dump_c_class.h.

Constructor & Destructor Documentation

◆ dump_ct() [1/2]

dump_ct::dump_ct	(	const goto_functionst &	_goto_functions,
		const bool	use_system_headers,
		const bool	use_all_headers,
		const bool	include_harness,
		const namespacet &	_ns,
		const irep_idt &	mode,
		const dump_c_configurationt	config
	)

inline

Definition at line 114 of file dump_c_class.h.

◆ dump_ct() [2/2]

dump_ct::dump_ct	(	const goto_functionst &	_goto_functions,
		const bool	use_system_headers,
		const bool	use_all_headers,
		const bool	include_harness,
		const namespacet &	_ns,
		const irep_idt &	mode
	)

inline

Definition at line 133 of file dump_c_class.h.

◆ ~dump_ct()

virtual dump_ct::~dump_ct ( )

virtualdefault

Member Function Documentation

◆ cleanup_decl()

void dump_ct::cleanup_decl	(	code_frontend_declt &	decl,
		std::list< irep_idt > &	local_static,
		std::list< irep_idt > &	local_type_decls
	)

protected

Definition at line 730 of file dump_c.cpp.

◆ cleanup_expr()

void dump_ct::cleanup_expr ( exprt & expr )

protected

Definition at line 1350 of file dump_c.cpp.

◆ cleanup_harness()

void dump_ct::cleanup_harness ( code_blockt & b )

protected

Replace CPROVER internal symbols in b by printable values and generate necessary declarations.

Parameters

b	Code block to be cleaned

Definition at line 1046 of file dump_c.cpp.

◆ cleanup_type()

void dump_ct::cleanup_type ( typet & type )

protected

Definition at line 1601 of file dump_c.cpp.

◆ collect_typedefs()

void dump_ct::collect_typedefs	(	const typet &	type,
		bool	early
	)

protected

Find any typedef names contained in the input type and store their declaration strings in typedef_map for eventual output.

Parameters

type	type to inspect for ID_C_typedef entry
early	set to true to enforce that typedef is dumped before any function declarations or struct definitions

Definition at line 774 of file dump_c.cpp.

◆ collect_typedefs_rec()

void dump_ct::collect_typedefs_rec	(	const typet &	type,
		bool	early,
		std::unordered_set< irep_idt > &	dependencies
	)

protected

Find any typedef names contained in the input type and store their declaration strings in typedef_map for eventual output.

Parameters

	type	type to inspect for ID_C_typedef entry
	early	set to true to enforce that typedef is dumped before any function declarations or struct definitions
[out]	dependencies	typedefs used in the declaration of a given typedef

Definition at line 787 of file dump_c.cpp.

◆ convert_compound() [1/2]

void dump_ct::convert_compound	(	const struct_union_typet &	type,
		const typet &	unresolved,
		bool	recursive,
		std::ostream &	os
	)

protected

Definition at line 482 of file dump_c.cpp.

◆ convert_compound() [2/2]

void dump_ct::convert_compound	(	const typet &	type,
		const typet &	unresolved,
		bool	recursive,
		std::ostream &	os
	)

protected

Definition at line 427 of file dump_c.cpp.

◆ convert_compound_declaration()

void dump_ct::convert_compound_declaration	(	const symbolt &	symbol,
		std::ostream &	os_body
	)

protected

declare compound types

Definition at line 395 of file dump_c.cpp.

◆ convert_compound_enum()

void dump_ct::convert_compound_enum	(	const typet &	type,
		std::ostream &	os
	)

protected

Definition at line 687 of file dump_c.cpp.

◆ convert_function_declaration()

void dump_ct::convert_function_declaration	(	const symbolt &	symbol,
		const bool	skip_main,
		std::ostream &	os_decl,
		std::ostream &	os_body,
		local_static_declst &	local_static_decls
	)

protected

Definition at line 1101 of file dump_c.cpp.

◆ convert_global_variable()

void dump_ct::convert_global_variable	(	const symbolt &	symbol,
		std::ostream &	os,
		local_static_declst &	local_static_decls
	)

protected

Definition at line 978 of file dump_c.cpp.

◆ dump_typedefs()

void dump_ct::dump_typedefs ( std::ostream & os ) const

protected

Print all typedefs that are not covered via typedef struct xyz { ...

} name;

Parameters

[out] os output stream

Definition at line 893 of file dump_c.cpp.

◆ expr_to_string()

std::string dump_ct::expr_to_string ( const exprt & expr )

protected

Definition at line 1654 of file dump_c.cpp.

◆ gather_global_typedefs()

void dump_ct::gather_global_typedefs ( )

protected

Find all global typdefs in the symbol table and store them in typedef_types.

Definition at line 862 of file dump_c.cpp.

◆ indent()

static std::string dump_ct::indent ( const unsigned n )

inlinestaticprotected

Definition at line 194 of file dump_c_class.h.

◆ insert_local_static_decls()

void dump_ct::insert_local_static_decls	(	code_blockt &	b,
		const std::list< irep_idt > &	local_static,
		local_static_declst &	local_static_decls,
		std::list< irep_idt > &	type_decls
	)

protected

Definition at line 1275 of file dump_c.cpp.

◆ insert_local_type_decls()

void dump_ct::insert_local_type_decls	(	code_blockt &	b,
		const std::list< irep_idt > &	type_decls
	)

protected

Definition at line 1309 of file dump_c.cpp.

◆ make_decl()

std::string dump_ct::make_decl	(	const irep_idt &	identifier,
		const typet &	type
	)

inlineprotected

Definition at line 199 of file dump_c_class.h.

◆ operator()()

void dump_ct::operator() ( std::ostream & out )

Definition at line 73 of file dump_c.cpp.

◆ type_to_string()

std::string dump_ct::type_to_string ( const typet & type )

protected

Definition at line 1640 of file dump_c.cpp.

Member Data Documentation

◆ converted_compound

convertedt dump_ct::converted_compound

protected

Definition at line 164 of file dump_c_class.h.

◆ converted_enum

convertedt dump_ct::converted_enum

protected

Definition at line 164 of file dump_c_class.h.

◆ converted_global

convertedt dump_ct::converted_global

protected

Definition at line 164 of file dump_c_class.h.

◆ copied_symbol_table

symbol_tablet dump_ct::copied_symbol_table

protected

Definition at line 157 of file dump_c_class.h.

◆ declared_enum_constants

declared_enum_constants_mapt dump_ct::declared_enum_constants

protected

Definition at line 171 of file dump_c_class.h.

◆ dump_c_config

const dump_c_configurationt dump_ct::dump_c_config

protected

Definition at line 159 of file dump_c_class.h.

◆ goto_functions

const goto_functionst& dump_ct::goto_functions

protected

Definition at line 156 of file dump_c_class.h.

◆ harness

const bool dump_ct::harness

protected

Definition at line 161 of file dump_c_class.h.

◆ mode

const irep_idt dump_ct::mode

protected

Definition at line 160 of file dump_c_class.h.

◆ ns

const namespacet dump_ct::ns

protected

Definition at line 158 of file dump_c_class.h.

◆ system_headers

std::set<std::string> dump_ct::system_headers

protected

Definition at line 166 of file dump_c_class.h.

◆ system_symbols

system_library_symbolst dump_ct::system_symbols

protected

Definition at line 168 of file dump_c_class.h.

◆ typedef_map

typedef_mapt dump_ct::typedef_map

protected

Definition at line 187 of file dump_c_class.h.

◆ typedef_types

typedef_typest dump_ct::typedef_types

protected

Definition at line 189 of file dump_c_class.h.

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

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

Classes

Public Member Functions

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ convertedt

◆ declared_enum_constants_mapt

◆ local_static_declst

◆ typedef_mapt

◆ typedef_typest

Constructor & Destructor Documentation

◆ dump_ct() [1/2]

◆ dump_ct() [2/2]

◆ ~dump_ct()

Member Function Documentation

◆ cleanup_decl()

◆ cleanup_expr()

◆ cleanup_harness()

◆ cleanup_type()

◆ collect_typedefs()

◆ collect_typedefs_rec()

◆ convert_compound() [1/2]

◆ convert_compound() [2/2]

◆ convert_compound_declaration()

◆ convert_compound_enum()

◆ convert_function_declaration()

◆ convert_global_variable()

◆ dump_typedefs()

◆ expr_to_string()

◆ gather_global_typedefs()

◆ indent()

◆ insert_local_static_decls()

◆ insert_local_type_decls()

◆ make_decl()

◆ operator()()

◆ type_to_string()

Member Data Documentation

◆ converted_compound

◆ converted_enum

◆ converted_global

◆ copied_symbol_table

◆ declared_enum_constants

◆ dump_c_config

◆ goto_functions

◆ harness

◆ mode

◆ ns

◆ system_headers

◆ system_symbols

◆ typedef_map

◆ typedef_types