#include <expr2c_class.h>

Inheritance diagram for expr2ct:

Collaboration diagram for expr2ct:

Public Member Functions
	expr2ct (const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration)

virtual	~expr2ct ()

virtual std::string	convert (const typet &src)

virtual std::string	convert (const exprt &src)

void	get_shorthands (const exprt &expr)

std::string	convert_with_identifier (const typet &src, const std::string &identifier)
	Build a declaration string, which requires converting both a type and putting an identifier in the syntactically correct position. More...

Protected Member Functions
virtual std::string	convert_rec (const typet &src, const qualifierst &qualifiers, const std::string &declarator)

virtual std::string	convert_struct_type (const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
	To generate C-like string for defining the given struct. More...

std::string	convert_struct_type (const typet &src, const std::string &qualifer_str, const std::string &declarator_str, bool inc_struct_body, bool inc_padding_components)
	To generate C-like string for declaring (or defining) the given struct. More...

virtual std::string	convert_array_type (const typet &src, const qualifierst &qualifiers, const std::string &declarator_str)
	To generate a C-like type declaration of an array. More...

std::string	convert_array_type (const typet &src, const qualifierst &qualifiers, const std::string &declarator_str, bool inc_size_if_possible)
	To generate a C-like type declaration of an array. More...

irep_idt	id_shorthand (const irep_idt &identifier) const

std::string	convert_typecast (const typecast_exprt &src, unsigned &precedence)

std::string	convert_pointer_arithmetic (const exprt &src, unsigned &precedence)

std::string	convert_pointer_difference (const exprt &src, unsigned &precedence)

std::string	convert_binary (const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)

std::string	convert_multi_ary (const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)

std::string	convert_cond (const exprt &src, unsigned precedence)

std::string	convert_struct_member_value (const exprt &src, unsigned precedence)

std::string	convert_array_member_value (const exprt &src, unsigned precedence)

std::string	convert_member (const member_exprt &src, unsigned precedence)

std::string	convert_array_of (const exprt &src, unsigned precedence)

std::string	convert_trinary (const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)

std::string	convert_rox (const shift_exprt &src, unsigned precedence)
	Conversion function from rol/ror expressions to C code strings Note that this constructs a complex expression to do bit twiddling since rol/ror operations are not native to ANSI-C. More...

std::string	convert_overflow (const exprt &src, unsigned &precedence)

std::string	convert_binding (const binding_exprt &, const std::string &symbol, unsigned precedence)

std::string	convert_with (const exprt &src, unsigned precedence)

std::string	convert_update (const update_exprt &, unsigned precedence)

std::string	convert_member_designator (const exprt &src)

std::string	convert_index_designator (const exprt &src)

std::string	convert_index (const binary_exprt &, unsigned precedence)

std::string	convert_byte_extract (const byte_extract_exprt &, unsigned precedence)

std::string	convert_byte_update (const byte_update_exprt &, unsigned precedence)

std::string	convert_extractbit (const extractbit_exprt &, unsigned precedence)

std::string	convert_extractbits (const extractbits_exprt &src, unsigned precedence)

std::string	convert_unary (const unary_exprt &, const std::string &symbol, unsigned precedence)

std::string	convert_unary_post (const exprt &src, const std::string &symbol, unsigned precedence)

std::optional< std::string >	convert_function (const exprt &src)
	Returns a string if `src` is a function with a known conversion, else returns nullopt. More...

std::string	convert_function (const exprt &src, const std::string &symbol)

std::string	convert_complex (const exprt &src, unsigned precedence)

std::string	convert_comma (const exprt &src, unsigned precedence)

std::string	convert_Hoare (const exprt &src)

std::string	convert_code (const codet &src)

virtual std::string	convert_code (const codet &src, unsigned indent)

std::string	convert_code_label (const code_labelt &src, unsigned indent)

std::string	convert_code_switch_case (const code_switch_caset &src, unsigned indent)

std::string	convert_code_asm (const code_asmt &src, unsigned indent)

std::string	convert_code_frontend_assign (const code_frontend_assignt &, unsigned indent)

std::string	convert_code_ifthenelse (const code_ifthenelset &src, unsigned indent)

std::string	convert_code_for (const code_fort &src, unsigned indent)

std::string	convert_code_while (const code_whilet &src, unsigned indent)

std::string	convert_code_dowhile (const code_dowhilet &src, unsigned indent)

std::string	convert_code_block (const code_blockt &src, unsigned indent)

std::string	convert_code_expression (const codet &src, unsigned indent)

std::string	convert_code_return (const codet &src, unsigned indent)

std::string	convert_code_goto (const codet &src, unsigned indent)

std::string	convert_code_assume (const codet &src, unsigned indent)

std::string	convert_code_assert (const codet &src, unsigned indent)

std::string	convert_code_break (unsigned indent)

std::string	convert_code_switch (const codet &src, unsigned indent)

std::string	convert_code_continue (unsigned indent)

std::string	convert_code_frontend_decl (const codet &, unsigned indent)

std::string	convert_code_decl_block (const codet &src, unsigned indent)

std::string	convert_code_dead (const codet &src, unsigned indent)

std::string	convert_code_function_call (const code_function_callt &src, unsigned indent)

std::string	convert_code_lock (const codet &src, unsigned indent)

std::string	convert_code_unlock (const codet &src, unsigned indent)

std::string	convert_code_printf (const codet &src, unsigned indent)

std::string	convert_code_fence (const codet &src, unsigned indent)

std::string	convert_code_input (const codet &src, unsigned indent)

std::string	convert_code_output (const codet &src, unsigned indent)

std::string	convert_code_array_set (const codet &src, unsigned indent)

std::string	convert_code_array_copy (const codet &src, unsigned indent)

std::string	convert_code_array_replace (const codet &src, unsigned indent)

virtual std::string	convert_with_precedence (const exprt &src, unsigned &precedence)

std::string	convert_function_application (const function_application_exprt &src)

std::string	convert_side_effect_expr_function_call (const side_effect_expr_function_callt &src)

std::string	convert_allocate (const exprt &src, unsigned &precedence)

std::string	convert_nondet (const exprt &src, unsigned &precedence)

std::string	convert_prob_coin (const exprt &src, unsigned &precedence)

std::string	convert_prob_uniform (const exprt &src, unsigned &precedence)

std::string	convert_statement_expression (const exprt &src, unsigned &precendence)

virtual std::string	convert_symbol (const exprt &src)

std::string	convert_predicate_symbol (const exprt &src)

std::string	convert_predicate_next_symbol (const exprt &src)

std::string	convert_predicate_passive_symbol (const exprt &src)

std::string	convert_nondet_symbol (const nondet_symbol_exprt &)

std::string	convert_quantified_symbol (const exprt &src)

std::string	convert_nondet_bool ()

std::string	convert_object_descriptor (const exprt &src, unsigned &precedence)

std::string	convert_literal (const exprt &src)

virtual std::string	convert_constant (const constant_exprt &src, unsigned &precedence)

virtual std::string	convert_constant_bool (bool boolean_value)
	To get the C-like representation of a given boolean value. More...

virtual std::string	convert_annotated_pointer_constant (const annotated_pointer_constant_exprt &src, unsigned &precedence)

std::string	convert_norep (const exprt &src, unsigned &precedence)

virtual std::string	convert_struct (const exprt &src, unsigned &precedence)

std::string	convert_union (const exprt &src, unsigned &precedence)

std::string	convert_vector (const exprt &src, unsigned &precedence)

std::string	convert_array (const exprt &src)

std::string	convert_array_list (const exprt &src, unsigned &precedence)

std::string	convert_initializer_list (const exprt &src)

std::string	convert_designated_initializer (const exprt &src)

std::string	convert_concatenation (const exprt &src, unsigned &precedence)

std::string	convert_sizeof (const exprt &src, unsigned &precedence)

std::string	convert_let (const let_exprt &, unsigned precedence)

std::string	convert_struct (const exprt &src, unsigned &precedence, bool include_padding_components)
	To generate a C-like string representing a struct. More...

std::string	convert_conditional_target_group (const exprt &src)

std::string	convert_bitreverse (const bitreverse_exprt &src)

std::string	convert_r_or_w_ok (const r_or_w_ok_exprt &src)

std::string	convert_prophecy_r_or_w_ok (const prophecy_r_or_w_ok_exprt &src)

std::string	convert_pointer_in_range (const pointer_in_range_exprt &src)

std::string	convert_prophecy_pointer_in_range (const prophecy_pointer_in_range_exprt &src)

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

Protected Attributes
const namespacet &	ns

const expr2c_configurationt &	configuration

std::unordered_map< irep_idt, std::unordered_set< irep_idt > >	ns_collision

std::unordered_map< irep_idt, irep_idt >	shorthands

unsigned	sizeof_nesting

Detailed Description

Definition at line 34 of file expr2c_class.h.

Constructor & Destructor Documentation

◆ expr2ct()

expr2ct::expr2ct	(	const namespacet &	_ns,
		const expr2c_configurationt &	configuration = `expr2c_configurationt::default_configuration`
	)

inlineexplicit

Definition at line 37 of file expr2c_class.h.

◆ ~expr2ct()

virtual expr2ct::~expr2ct ( )

inlinevirtual

Definition at line 44 of file expr2c_class.h.

Member Function Documentation

◆ convert() [1/2]

std::string expr2ct::convert ( const exprt & src )

virtual

Reimplemented in expr2javat.

Definition at line 4128 of file expr2c.cpp.

◆ convert() [2/2]

std::string expr2ct::convert ( const typet & src )

virtual

Reimplemented in expr2javat.

Definition at line 214 of file expr2c.cpp.

◆ convert_allocate()

std::string expr2ct::convert_allocate	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 1146 of file expr2c.cpp.

◆ convert_annotated_pointer_constant()

std::string expr2ct::convert_annotated_pointer_constant	(	const annotated_pointer_constant_exprt &	src,
		unsigned &	precedence
	)

protectedvirtual

Definition at line 2017 of file expr2c.cpp.

◆ convert_array()

std::string expr2ct::convert_array ( const exprt & src )

protected

Definition at line 2193 of file expr2c.cpp.

◆ convert_array_list()

std::string expr2ct::convert_array_list	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 2296 of file expr2c.cpp.

◆ convert_array_member_value()

std::string expr2ct::convert_array_member_value	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1595 of file expr2c.cpp.

◆ convert_array_of()

std::string expr2ct::convert_array_of	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1320 of file expr2c.cpp.

◆ convert_array_type() [1/2]

std::string expr2ct::convert_array_type	(	const typet &	src,
		const qualifierst &	qualifiers,
		const std::string &	declarator_str
	)

protectedvirtual

To generate a C-like type declaration of an array.

Includes the size of the array in the []

Parameters

src	The array type to convert
qualifiers	Any qualifiers on the type
declarator_str	Previously computed string denoting the array symbol

Returns: A C-like type declaration of an array

Definition at line 716 of file expr2c.cpp.

◆ convert_array_type() [2/2]

std::string expr2ct::convert_array_type	(	const typet &	src,
		const qualifierst &	qualifiers,
		const std::string &	declarator_str,
		bool	inc_size_if_possible
	)

protected

To generate a C-like type declaration of an array.

Optionally can include or exclude the size of the array in the []

Parameters

src	The array type to convert
qualifiers	Any qualifiers on the type
declarator_str	Previously computed string denoting the array symbol
inc_size_if_possible	Should the generated string include the size of the array (if it is known).

Returns: A C-like type declaration of an array

Definition at line 733 of file expr2c.cpp.

◆ convert_binary()

std::string expr2ct::convert_binary	(	const binary_exprt &	src,
		const std::string &	symbol,
		unsigned	precedence,
		bool	full_parentheses
	)

protected

Definition at line 1026 of file expr2c.cpp.

◆ convert_binding()

std::string expr2ct::convert_binding	(	const binding_exprt &	src,
		const std::string &	symbol,
		unsigned	precedence
	)

protected

Definition at line 836 of file expr2c.cpp.

◆ convert_bitreverse()

std::string expr2ct::convert_bitreverse ( const bitreverse_exprt & src )

protected

Definition at line 3544 of file expr2c.cpp.

◆ convert_byte_extract()

std::string expr2ct::convert_byte_extract	(	const byte_extract_exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1330 of file expr2c.cpp.

◆ convert_byte_update()

std::string expr2ct::convert_byte_update	(	const byte_update_exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1356 of file expr2c.cpp.

◆ convert_code() [1/2]

std::string expr2ct::convert_code ( const codet & src )

protected

Definition at line 3433 of file expr2c.cpp.

◆ convert_code() [2/2]

std::string expr2ct::convert_code	(	const codet &	src,
		unsigned	indent
	)

protectedvirtual

Reimplemented in expr2cppt, and expr2javat.

Definition at line 2971 of file expr2c.cpp.

◆ convert_code_array_copy()

std::string expr2ct::convert_code_array_copy	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3315 of file expr2c.cpp.

◆ convert_code_array_replace()

std::string expr2ct::convert_code_array_replace	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3337 of file expr2c.cpp.

◆ convert_code_array_set()

std::string expr2ct::convert_code_array_set	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3293 of file expr2c.cpp.

◆ convert_code_asm()

std::string expr2ct::convert_code_asm	(	const code_asmt &	src,
		unsigned	indent
	)

protected

Definition at line 2552 of file expr2c.cpp.

◆ convert_code_assert()

std::string expr2ct::convert_code_assert	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3358 of file expr2c.cpp.

◆ convert_code_assume()

std::string expr2ct::convert_code_assume	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3371 of file expr2c.cpp.

◆ convert_code_block()

std::string expr2ct::convert_code_block	(	const code_blockt &	src,
		unsigned	indent
	)

protected

Definition at line 2911 of file expr2c.cpp.

◆ convert_code_break()

std::string expr2ct::convert_code_break ( unsigned indent )

protected

Definition at line 2755 of file expr2c.cpp.

◆ convert_code_continue()

std::string expr2ct::convert_code_continue ( unsigned indent )

protected

Definition at line 2807 of file expr2c.cpp.

◆ convert_code_dead()

std::string expr2ct::convert_code_dead	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 2860 of file expr2c.cpp.

◆ convert_code_decl_block()

std::string expr2ct::convert_code_decl_block	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 2934 of file expr2c.cpp.

◆ convert_code_dowhile()

std::string expr2ct::convert_code_dowhile	(	const code_dowhilet &	src,
		unsigned	indent
	)

protected

Definition at line 2656 of file expr2c.cpp.

◆ convert_code_expression()

std::string expr2ct::convert_code_expression	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 2949 of file expr2c.cpp.

◆ convert_code_fence()

std::string expr2ct::convert_code_fence	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3220 of file expr2c.cpp.

◆ convert_code_for()

std::string expr2ct::convert_code_for	(	const code_fort &	src,
		unsigned	indent
	)

protected

Definition at line 2874 of file expr2c.cpp.

◆ convert_code_frontend_assign()

std::string expr2ct::convert_code_frontend_assign	(	const code_frontend_assignt &	src,
		unsigned	indent
	)

protected

Definition at line 3116 of file expr2c.cpp.

◆ convert_code_frontend_decl()

std::string expr2ct::convert_code_frontend_decl	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 2817 of file expr2c.cpp.

◆ convert_code_function_call()

std::string expr2ct::convert_code_function_call	(	const code_function_callt &	src,
		unsigned	indent
	)

protected

Definition at line 3150 of file expr2c.cpp.

◆ convert_code_goto()

std::string expr2ct::convert_code_goto	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 2743 of file expr2c.cpp.

◆ convert_code_ifthenelse()

std::string expr2ct::convert_code_ifthenelse	(	const code_ifthenelset &	src,
		unsigned	indent
	)

protected

Definition at line 2685 of file expr2c.cpp.

◆ convert_code_input()

std::string expr2ct::convert_code_input	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3250 of file expr2c.cpp.

◆ convert_code_label()

std::string expr2ct::convert_code_label	(	const code_labelt &	src,
		unsigned	indent
	)

protected

Definition at line 3385 of file expr2c.cpp.

◆ convert_code_lock()

std::string expr2ct::convert_code_lock	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3124 of file expr2c.cpp.

◆ convert_code_output()

std::string expr2ct::convert_code_output	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3272 of file expr2c.cpp.

◆ convert_code_printf()

std::string expr2ct::convert_code_printf	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3198 of file expr2c.cpp.

◆ convert_code_return()

std::string expr2ct::convert_code_return	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 2722 of file expr2c.cpp.

◆ convert_code_switch()

std::string expr2ct::convert_code_switch	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 2764 of file expr2c.cpp.

◆ convert_code_switch_case()

std::string expr2ct::convert_code_switch_case	(	const code_switch_caset &	src,
		unsigned	indent
	)

protected

Definition at line 3403 of file expr2c.cpp.

◆ convert_code_unlock()

std::string expr2ct::convert_code_unlock	(	const codet &	src,
		unsigned	indent
	)

protected

Definition at line 3137 of file expr2c.cpp.

◆ convert_code_while()

std::string expr2ct::convert_code_while	(	const code_whilet &	src,
		unsigned	indent
	)

protected

Definition at line 2630 of file expr2c.cpp.

◆ convert_comma()

std::string expr2ct::convert_comma	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1246 of file expr2c.cpp.

◆ convert_complex()

std::string expr2ct::convert_complex	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1270 of file expr2c.cpp.

◆ convert_concatenation()

std::string expr2ct::convert_concatenation	(	const exprt &	src,
		unsigned &	precedence
	)

protected

◆ convert_cond()

std::string expr2ct::convert_cond	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 992 of file expr2c.cpp.

◆ convert_conditional_target_group()

std::string expr2ct::convert_conditional_target_group ( const exprt & src )

protected

Definition at line 3519 of file expr2c.cpp.

◆ convert_constant()

std::string expr2ct::convert_constant	(	const constant_exprt &	src,
		unsigned &	precedence
	)

protectedvirtual

Reimplemented in expr2cppt, and expr2javat.

Definition at line 1771 of file expr2c.cpp.

◆ convert_constant_bool()

std::string expr2ct::convert_constant_bool ( bool boolean_value )

protectedvirtual

To get the C-like representation of a given boolean value.

Parameters

boolean_value The value of the constant bool expression

Returns: Returns a C-like representation of the boolean value, e.g. TRUE or FALSE.

Definition at line 2030 of file expr2c.cpp.

◆ convert_designated_initializer()

std::string expr2ct::convert_designated_initializer ( const exprt & src )

protected

Definition at line 2416 of file expr2c.cpp.

◆ convert_extractbit()

std::string expr2ct::convert_extractbit	(	const extractbit_exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 3482 of file expr2c.cpp.

◆ convert_extractbits()

std::string expr2ct::convert_extractbits	(	const extractbits_exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 3493 of file expr2c.cpp.

◆ convert_function() [1/2]

std::optional< std::string > expr2ct::convert_function ( const exprt & src )

protected

Returns a string if src is a function with a known conversion, else returns nullopt.

Definition at line 4071 of file expr2c.cpp.

◆ convert_function() [2/2]

std::string expr2ct::convert_function	(	const exprt &	src,
		const std::string &	symbol
	)

protected

Definition at line 1225 of file expr2c.cpp.

◆ convert_function_application()

std::string expr2ct::convert_function_application ( const function_application_exprt & src )

protected

Definition at line 2459 of file expr2c.cpp.

◆ convert_Hoare()

std::string expr2ct::convert_Hoare ( const exprt & src )

protected

Definition at line 3438 of file expr2c.cpp.

◆ convert_index()

std::string expr2ct::convert_index	(	const binary_exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1403 of file expr2c.cpp.

◆ convert_index_designator()

std::string expr2ct::convert_index_designator ( const exprt & src )

protected

Definition at line 1508 of file expr2c.cpp.

◆ convert_initializer_list()

std::string expr2ct::convert_initializer_list ( const exprt & src )

protected

Definition at line 2330 of file expr2c.cpp.

◆ convert_let()

std::string expr2ct::convert_let	(	const let_exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 927 of file expr2c.cpp.

◆ convert_literal()

std::string expr2ct::convert_literal ( const exprt & src )

protected

Definition at line 1209 of file expr2c.cpp.

◆ convert_member()

std::string expr2ct::convert_member	(	const member_exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1518 of file expr2c.cpp.

◆ convert_member_designator()

std::string expr2ct::convert_member_designator ( const exprt & src )

protected

Definition at line 1498 of file expr2c.cpp.

◆ convert_multi_ary()

std::string expr2ct::convert_multi_ary	(	const exprt &	src,
		const std::string &	symbol,
		unsigned	precedence,
		bool	full_parentheses
	)

protected

Definition at line 1078 of file expr2c.cpp.

◆ convert_nondet()

std::string expr2ct::convert_nondet	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 1174 of file expr2c.cpp.

◆ convert_nondet_bool()

std::string expr2ct::convert_nondet_bool ( )

protected

Definition at line 1696 of file expr2c.cpp.

◆ convert_nondet_symbol()

std::string expr2ct::convert_nondet_symbol ( const nondet_symbol_exprt & src )

protected

Definition at line 1666 of file expr2c.cpp.

◆ convert_norep()

std::string expr2ct::convert_norep	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 1615 of file expr2c.cpp.

◆ convert_object_descriptor()

std::string expr2ct::convert_object_descriptor	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 1701 of file expr2c.cpp.

◆ convert_overflow()

std::string expr2ct::convert_overflow	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 2516 of file expr2c.cpp.

◆ convert_pointer_arithmetic()

std::string expr2ct::convert_pointer_arithmetic	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 1422 of file expr2c.cpp.

◆ convert_pointer_difference()

std::string expr2ct::convert_pointer_difference	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 1459 of file expr2c.cpp.

◆ convert_pointer_in_range()

std::string expr2ct::convert_pointer_in_range ( const pointer_in_range_exprt & src )

protected

Definition at line 3598 of file expr2c.cpp.

◆ convert_predicate_next_symbol()

std::string expr2ct::convert_predicate_next_symbol ( const exprt & src )

protected

Definition at line 1678 of file expr2c.cpp.

◆ convert_predicate_passive_symbol()

std::string expr2ct::convert_predicate_passive_symbol ( const exprt & src )

protected

Definition at line 1684 of file expr2c.cpp.

◆ convert_predicate_symbol()

std::string expr2ct::convert_predicate_symbol ( const exprt & src )

protected

Definition at line 1672 of file expr2c.cpp.

◆ convert_prob_coin()

std::string expr2ct::convert_prob_coin	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 1199 of file expr2c.cpp.

◆ convert_prob_uniform()

std::string expr2ct::convert_prob_uniform	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 1214 of file expr2c.cpp.

◆ convert_prophecy_pointer_in_range()

std::string expr2ct::convert_prophecy_pointer_in_range ( const prophecy_pointer_in_range_exprt & src )

protected

Definition at line 3616 of file expr2c.cpp.

◆ convert_prophecy_r_or_w_ok()

std::string expr2ct::convert_prophecy_r_or_w_ok ( const prophecy_r_or_w_ok_exprt & src )

protected

Definition at line 3579 of file expr2c.cpp.

◆ convert_quantified_symbol()

std::string expr2ct::convert_quantified_symbol ( const exprt & src )

protected

Definition at line 1690 of file expr2c.cpp.

◆ convert_r_or_w_ok()

std::string expr2ct::convert_r_or_w_ok ( const r_or_w_ok_exprt & src )

protected

Definition at line 3560 of file expr2c.cpp.

◆ convert_rec()

std::string expr2ct::convert_rec	(	const typet &	src,
		const qualifierst &	qualifiers,
		const std::string &	declarator
	)

protectedvirtual

Reimplemented in expr2cppt, and expr2javat.

Definition at line 219 of file expr2c.cpp.

◆ convert_rox()

std::string expr2ct::convert_rox	(	const shift_exprt &	src,
		unsigned	precedence
	)

protected

Conversion function from rol/ror expressions to C code strings Note that this constructs a complex expression to do bit twiddling since rol/ror operations are not native to ANSI-C.

The complex expression is then recursively converted.

Parameters

src	is an exprt that must be either an rol or ror
precedence	precedence for bracketing

Returns: string for performing rol/ror as bit twiddling with C

Definition at line 2356 of file expr2c.cpp.

◆ convert_side_effect_expr_function_call()

std::string expr2ct::convert_side_effect_expr_function_call ( const side_effect_expr_function_callt & src )

protected

Definition at line 2487 of file expr2c.cpp.

◆ convert_sizeof()

std::string expr2ct::convert_sizeof	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 3505 of file expr2c.cpp.

◆ convert_statement_expression()

std::string expr2ct::convert_statement_expression	(	const exprt &	src,
		unsigned &	precendence
	)

protected

Definition at line 1184 of file expr2c.cpp.

◆ convert_struct() [1/2]

std::string expr2ct::convert_struct	(	const exprt &	src,
		unsigned &	precedence
	)

protectedvirtual

Reimplemented in expr2cppt, and expr2javat.

Definition at line 2038 of file expr2c.cpp.

◆ convert_struct() [2/2]

std::string expr2ct::convert_struct	(	const exprt &	src,
		unsigned &	precedence,
		bool	include_padding_components
	)

protected

To generate a C-like string representing a struct.

Can optionally include the padding parameters.

Parameters

	src	The struct declaration expression
[out]	precedence	Precedence of the top level operator in the resulting string, used to decide about adding parentheses
	include_padding_components	Should the generated C code include the padding members added to structs for GOTOs benefit

Returns: A string representation of the struct expression

Definition at line 2054 of file expr2c.cpp.

◆ convert_struct_member_value()

std::string expr2ct::convert_struct_member_value	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 1605 of file expr2c.cpp.

◆ convert_struct_type() [1/2]

std::string expr2ct::convert_struct_type	(	const typet &	src,
		const std::string &	qualifiers,
		const std::string &	declarator,
		bool	inc_struct_body,
		bool	inc_padding_components
	)

protected

To generate C-like string for declaring (or defining) the given struct.

Parameters

src	the struct type being converted
qualifiers	any qualifiers on the type
declarator	the declarator on the type
inc_struct_body	when generating the code, should we include a complete definition of the struct
inc_padding_components	should the padding parameters be included Note this only makes sense if inc_struct_body

Returns: Returns a type declaration for a struct, optionally containing the body of the struct (and in that body, optionally the padding parameters).

Definition at line 661 of file expr2c.cpp.

◆ convert_struct_type() [2/2]

std::string expr2ct::convert_struct_type	(	const typet &	src,
		const std::string &	qualifiers_str,
		const std::string &	declarator_str
	)

protectedvirtual

To generate C-like string for defining the given struct.

Parameters

src	the struct type being converted
qualifiers_str	any qualifiers on the type
declarator_str	the declarator on the type

Returns: Returns a type declaration for a struct, containing the body of the struct and in that body the padding parameters.

Definition at line 638 of file expr2c.cpp.

◆ convert_symbol()

std::string expr2ct::convert_symbol ( const exprt & src )

protectedvirtual

Definition at line 1626 of file expr2c.cpp.

◆ convert_trinary()

std::string expr2ct::convert_trinary	(	const ternary_exprt &	src,
		const std::string &	symbol1,
		const std::string &	symbol2,
		unsigned	precedence
	)

protected

Definition at line 789 of file expr2c.cpp.

◆ convert_typecast()

std::string expr2ct::convert_typecast	(	const typecast_exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 755 of file expr2c.cpp.

◆ convert_unary()

std::string expr2ct::convert_unary	(	const unary_exprt &	src,
		const std::string &	symbol,
		unsigned	precedence
	)

protected

Definition at line 1126 of file expr2c.cpp.

◆ convert_unary_post()

std::string expr2ct::convert_unary_post	(	const exprt &	src,
		const std::string &	symbol,
		unsigned	precedence
	)

protected

Definition at line 1381 of file expr2c.cpp.

◆ convert_union()

std::string expr2ct::convert_union	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 2174 of file expr2c.cpp.

◆ convert_update()

std::string expr2ct::convert_update	(	const update_exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 954 of file expr2c.cpp.

◆ convert_vector()

std::string expr2ct::convert_vector	(	const exprt &	src,
		unsigned &	precedence
	)

protected

Definition at line 2127 of file expr2c.cpp.

◆ convert_with()

std::string expr2ct::convert_with	(	const exprt &	src,
		unsigned	precedence
	)

protected

Definition at line 859 of file expr2c.cpp.

◆ convert_with_identifier()

std::string expr2ct::convert_with_identifier	(	const typet &	src,
		const std::string &	identifier
	)

Build a declaration string, which requires converting both a type and putting an identifier in the syntactically correct position.

Parameters

src	the type to convert
identifier	the identifier to use as the type

Returns: A C declaration of the given type with the right identifier.

Definition at line 4139 of file expr2c.cpp.

◆ convert_with_precedence()

std::string expr2ct::convert_with_precedence	(	const exprt &	src,
		unsigned &	precedence
	)

protectedvirtual

Reimplemented in expr2cppt, and expr2javat.

Definition at line 3636 of file expr2c.cpp.

◆ get_shorthands()

void expr2ct::get_shorthands ( const exprt & expr )

Definition at line 117 of file expr2c.cpp.

◆ id_shorthand()

irep_idt expr2ct::id_shorthand ( const irep_idt & identifier ) const

protected

Definition at line 76 of file expr2c.cpp.

◆ indent_str()

std::string expr2ct::indent_str ( unsigned indent )

staticprotected

Definition at line 2547 of file expr2c.cpp.

Member Data Documentation

◆ configuration

const expr2c_configurationt& expr2ct::configuration

protected

Definition at line 56 of file expr2c_class.h.

◆ ns

const namespacet& expr2ct::ns

protected

Definition at line 55 of file expr2c_class.h.

◆ ns_collision

std::unordered_map<irep_idt, std::unordered_set<irep_idt> > expr2ct::ns_collision

protected

Definition at line 88 of file expr2c_class.h.

◆ shorthands

std::unordered_map<irep_idt, irep_idt> expr2ct::shorthands

protected

Definition at line 89 of file expr2c_class.h.

◆ sizeof_nesting

unsigned expr2ct::sizeof_nesting

protected

Definition at line 91 of file expr2c_class.h.

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

/home/runner/work/cbmc/cbmc/src/ansi-c/expr2c_class.h
/home/runner/work/cbmc/cbmc/src/ansi-c/expr2c.cpp

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ expr2ct()

◆ ~expr2ct()

Member Function Documentation

◆ convert() [1/2]

◆ convert() [2/2]

◆ convert_allocate()

◆ convert_annotated_pointer_constant()

◆ convert_array()

◆ convert_array_list()

◆ convert_array_member_value()

◆ convert_array_of()

◆ convert_array_type() [1/2]

◆ convert_array_type() [2/2]

◆ convert_binary()

◆ convert_binding()

◆ convert_bitreverse()

◆ convert_byte_extract()

◆ convert_byte_update()

◆ convert_code() [1/2]

◆ convert_code() [2/2]

◆ convert_code_array_copy()

◆ convert_code_array_replace()

◆ convert_code_array_set()

◆ convert_code_asm()

◆ convert_code_assert()

◆ convert_code_assume()

◆ convert_code_block()

◆ convert_code_break()

◆ convert_code_continue()

◆ convert_code_dead()

◆ convert_code_decl_block()

◆ convert_code_dowhile()

◆ convert_code_expression()

◆ convert_code_fence()

◆ convert_code_for()

◆ convert_code_frontend_assign()

◆ convert_code_frontend_decl()

◆ convert_code_function_call()

◆ convert_code_goto()

◆ convert_code_ifthenelse()

◆ convert_code_input()

◆ convert_code_label()

◆ convert_code_lock()

◆ convert_code_output()

◆ convert_code_printf()

◆ convert_code_return()

◆ convert_code_switch()

◆ convert_code_switch_case()

◆ convert_code_unlock()

◆ convert_code_while()

◆ convert_comma()

◆ convert_complex()

◆ convert_concatenation()

◆ convert_cond()

◆ convert_conditional_target_group()

◆ convert_constant()

◆ convert_constant_bool()

◆ convert_designated_initializer()

◆ convert_extractbit()

◆ convert_extractbits()

◆ convert_function() [1/2]

◆ convert_function() [2/2]

◆ convert_function_application()

◆ convert_Hoare()

◆ convert_index()

◆ convert_index_designator()

◆ convert_initializer_list()

◆ convert_let()

◆ convert_literal()

◆ convert_member()

◆ convert_member_designator()

◆ convert_multi_ary()

◆ convert_nondet()

◆ convert_nondet_bool()