#include <c_typecheck_base.h>

Inheritance diagram for c_typecheck_baset:

Collaboration diagram for c_typecheck_baset:

Public Member Functions
	c_typecheck_baset (symbol_table_baset &_symbol_table, const std::string &_module, message_handlert &_message_handler)

	c_typecheck_baset (symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2, const std::string &_module, message_handlert &_message_handler)

virtual	~c_typecheck_baset ()

virtual void	typecheck ()=0

virtual void	typecheck_expr (exprt &expr)

virtual void	typecheck_spec_assigns (exprt::operandst &targets)

Public Member Functions inherited from typecheckt
	typecheckt (message_handlert &_message_handler)

virtual	~typecheckt ()

virtual bool	typecheck_main ()

Public Member Functions inherited from messaget
virtual void	set_message_handler (message_handlert &_message_handler)

message_handlert &	get_message_handler ()

	messaget (const messaget &other)

messaget &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () const

void	conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
	Generate output to `message_stream` using `output_generator` if the configured verbosity is at least as high as that of `message_stream`.

Public Member Functions inherited from namespacet
	namespacet (const symbol_table_baset &_symbol_table)

	namespacet (const symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2)

	namespacet (const symbol_table_baset _symbol_table1, const symbol_table_baset _symbol_table2)

bool	lookup (const irep_idt &name, const symbolt *&symbol) const override
	See documentation for namespace_baset::lookup().

std::size_t	smallest_unused_suffix (const std::string &prefix) const override
	See documentation for namespace_baset::smallest_unused_suffix().

const symbol_table_baset &	get_symbol_table () const
	Return first symbol table registered with the namespace.

const symbolt &	lookup (const irep_idt &name) const
	Lookup a symbol in the namespace.

const symbolt &	lookup (const symbol_exprt &) const
	Generic lookup function for a symbol expression in a symbol table.

const symbolt &	lookup (const tag_typet &) const
	Generic lookup function for a tag type in a symbol table.

virtual bool	lookup (const irep_idt &name, const symbolt *&symbol) const=0
	Searches for a symbol named `name`.

Public Member Functions inherited from namespace_baset
const symbolt &	lookup (const irep_idt &name) const
	Lookup a symbol in the namespace.

const symbolt &	lookup (const symbol_exprt &) const
	Generic lookup function for a symbol expression in a symbol table.

const symbolt &	lookup (const tag_typet &) const
	Generic lookup function for a tag type in a symbol table.

virtual	~namespace_baset ()

void	follow_macros (exprt &) const
	Follow macros to their values in a given expression.

const union_typet &	follow_tag (const union_tag_typet &) const
	Follow type tag of union type.

const struct_typet &	follow_tag (const struct_tag_typet &) const
	Follow type tag of struct type.

const c_enum_typet &	follow_tag (const c_enum_tag_typet &) const
	Follow type tag of enum type.

const struct_union_typet &	follow_tag (const struct_or_union_tag_typet &) const
	Resolve a `struct_tag_typet` or `union_tag_typet` to the complete version.

Protected Types
typedef std::unordered_map< irep_idt, typet >	id_type_mapt

typedef std::unordered_map< irep_idt, irep_idt >	asm_label_mapt

Protected Member Functions
virtual std::string	to_string (const exprt &expr)

virtual std::string	to_string (const typet &type)

virtual void	do_initializer (exprt &initializer, const typet &type, bool force_constant)

virtual exprt	do_initializer_rec (const exprt &value, const typet &type, bool force_constant)
	initialize something of type ‘type’ with given value ‘value’

virtual exprt	do_initializer_list (const exprt &value, const typet &type, bool force_constant)

virtual exprt::operandst::const_iterator	do_designated_initializer (exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant)

designatort	make_designator (const typet &type, const exprt &src)

void	designator_enter (const typet &type, designatort &designator)

void	increment_designator (designatort &designator)

bool	gcc_vector_types_compatible (const vector_typet &, const vector_typet &)

virtual void	implicit_typecast (exprt &expr, const typet &type)

virtual void	implicit_typecast_arithmetic (exprt &expr)

virtual void	implicit_typecast_arithmetic (exprt &expr1, exprt &expr2)

virtual void	implicit_typecast_bool (exprt &expr)

virtual void	start_typecheck_code ()

virtual void	typecheck_code (codet &code)

virtual void	typecheck_assign (codet &expr)

virtual void	typecheck_asm (code_asmt &code)

virtual void	typecheck_block (code_blockt &code)

virtual void	typecheck_break (codet &code)

virtual void	typecheck_continue (codet &code)

virtual void	typecheck_decl (codet &code)

virtual void	typecheck_expression (codet &code)

virtual void	typecheck_for (codet &code)

virtual void	typecheck_goto (code_gotot &code)

virtual void	typecheck_ifthenelse (code_ifthenelset &code)

virtual void	typecheck_label (code_labelt &code)

virtual void	typecheck_switch_case (code_switch_caset &code)

virtual void	typecheck_gcc_computed_goto (codet &code)

virtual void	typecheck_gcc_switch_case_range (code_gcc_switch_case_ranget &)

virtual void	typecheck_gcc_local_label (codet &code)

virtual void	typecheck_return (code_frontend_returnt &)

virtual void	typecheck_switch (codet &code)

virtual void	typecheck_while (code_whilet &code)

virtual void	typecheck_dowhile (code_dowhilet &code)

virtual void	typecheck_start_thread (codet &code)

virtual void	typecheck_typed_target_call (side_effect_expr_function_callt &expr)

virtual void	typecheck_obeys_contract_call (side_effect_expr_function_callt &expr)
	Checks an obeys_contract predicate occurrence.

virtual void	check_history_expr_return_value (const exprt &expr, std::string &clause_type)
	Checks that no history expr or return_value exists in expr.

virtual void	check_was_freed (const exprt &expr, std::string &clause_type)
	Checks that no occurence of the `CPROVER_PREFIX was_freed` predicate is found in expr.

virtual void	typecheck_spec_frees (exprt::operandst &targets)

virtual void	typecheck_conditional_targets (exprt::operandst &targets, const std::function< void(exprt &)> typecheck_target, const std::string &clause_type)

virtual void	typecheck_spec_condition (exprt &condition)

virtual void	typecheck_spec_assigns_target (exprt &target)

virtual void	typecheck_spec_frees_target (exprt &target)

virtual void	typecheck_spec_loop_invariant (codet &code)

virtual void	typecheck_spec_decreases (codet &code)

virtual void	throw_on_side_effects (const exprt &expr)

virtual void	typecheck_expr_builtin_va_arg (exprt &expr)

virtual void	typecheck_expr_builtin_offsetof (exprt &expr)

virtual void	typecheck_expr_cw_va_arg_typeof (exprt &expr)

virtual void	typecheck_expr_main (exprt &expr)

virtual void	typecheck_expr_operands (exprt &expr)

virtual void	typecheck_expr_comma (exprt &expr)

virtual void	typecheck_expr_constant (exprt &expr)

virtual void	typecheck_expr_side_effect (side_effect_exprt &expr)

virtual void	typecheck_expr_unary_arithmetic (exprt &expr)

virtual void	typecheck_expr_unary_boolean (exprt &expr)

virtual void	typecheck_expr_binary_arithmetic (exprt &expr)

virtual void	typecheck_expr_shifts (shift_exprt &expr)

virtual void	typecheck_expr_pointer_arithmetic (exprt &expr)

virtual void	typecheck_arithmetic_pointer (exprt &expr)

virtual void	typecheck_expr_binary_boolean (exprt &expr)

virtual void	typecheck_expr_trinary (if_exprt &expr)

virtual void	typecheck_expr_address_of (exprt &expr)

virtual void	typecheck_expr_dereference (exprt &expr)

virtual void	typecheck_expr_member (exprt &expr)

virtual void	typecheck_expr_ptrmember (exprt &expr)

virtual void	typecheck_expr_rel (binary_relation_exprt &expr)

virtual void	typecheck_expr_rel_vector (binary_exprt &expr)

virtual void	adjust_float_rel (binary_relation_exprt &)

virtual void	typecheck_expr_index (exprt &expr)

virtual void	typecheck_expr_typecast (exprt &expr)

virtual void	typecheck_expr_symbol (exprt &expr)

virtual void	typecheck_expr_sizeof (exprt &expr)

virtual void	typecheck_expr_alignof (exprt &expr)

virtual void	typecheck_expr_function_identifier (exprt &expr)

virtual void	typecheck_side_effect_gcc_conditional_expression (side_effect_exprt &expr)

virtual void	typecheck_side_effect_function_call (side_effect_expr_function_callt &expr)

virtual void	typecheck_side_effect_assignment (side_effect_exprt &expr)

virtual void	typecheck_side_effect_statement_expression (side_effect_exprt &expr)

virtual void	typecheck_function_call_arguments (side_effect_expr_function_callt &expr)
	Typecheck the parameters in a function call expression, and where necessary, make implicit casts around parameters explicit.

virtual exprt	do_special_functions (side_effect_expr_function_callt &expr)

exprt	typecheck_builtin_overflow (side_effect_expr_function_callt &expr, const irep_idt &arith_op)

exprt	typecheck_saturating_arithmetic (const side_effect_expr_function_callt &expr)

virtual std::optional< symbol_exprt >	typecheck_gcc_polymorphic_builtin (const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)

virtual code_blockt	instantiate_gcc_polymorphic_builtin (const irep_idt &identifier, const symbol_exprt &function_symbol)

virtual std::optional< symbol_exprt >	typecheck_shadow_memory_builtin (const side_effect_expr_function_callt &expr)
	Typecheck the function if it is a shadow_memory builtin and return a symbol for it.

virtual exprt	typecheck_shuffle_vector (const side_effect_expr_function_callt &expr)

void	disallow_subexpr_by_id (const exprt &, const irep_idt &, const std::string &) const

virtual void	make_index_type (exprt &expr)

virtual void	make_constant (exprt &expr)

virtual void	make_constant_index (exprt &expr)

virtual bool	gcc_types_compatible_p (const typet &, const typet &)

virtual bool	builtin_factory (const irep_idt &)

virtual void	typecheck_type (typet &type)

virtual void	typecheck_compound_type (struct_union_typet &type)

virtual void	typecheck_compound_body (struct_union_typet &type)

virtual void	typecheck_c_enum_type (typet &type)

virtual void	typecheck_c_enum_tag_type (c_enum_tag_typet &type)

virtual void	typecheck_code_type (code_typet &type)

virtual void	typecheck_typedef_type (typet &type)

virtual void	typecheck_c_bit_field_type (c_bit_field_typet &type)

virtual void	typecheck_typeof_type (typet &type)

virtual void	typecheck_array_type (array_typet &type)

virtual void	typecheck_vector_type (typet &type)

virtual void	typecheck_custom_type (typet &type)

virtual void	typecheck_bitint_type (typet &)

virtual void	adjust_function_parameter (typet &type) const

virtual bool	is_complete_type (const typet &type) const

typet	enum_constant_type (const mp_integer &min, const mp_integer &max) const

bitvector_typet	enum_underlying_type (const mp_integer &min, const mp_integer &max, bool is_packed) const

void	move_symbol (symbolt &symbol, symbolt *&new_symbol)

void	move_symbol (symbolt &symbol)

void	typecheck_declaration (ansi_c_declarationt &)

void	typecheck_symbol (symbolt &symbol)

void	typecheck_new_symbol (symbolt &symbol)

void	typecheck_redefinition_type (symbolt &old_symbol, symbolt &new_symbol)

void	typecheck_redefinition_non_type (symbolt &old_symbol, symbolt &new_symbol)

void	typecheck_function_body (symbolt &symbol)

void	add_parameters_to_symbol_table (symbolt &symbol)
	Create symbols for parameter of the code-typed symbol `symbol`.

virtual void	do_initializer (symbolt &symbol)

void	apply_asm_label (const irep_idt &asm_label, symbolt &symbol)

Static Protected Member Functions
static void	add_rounding_mode (exprt &)

static bool	is_numeric_type (const typet &src)

Protected Attributes
symbol_table_baset &	symbol_table

const irep_idt const irep_idt	mode

symbolt	current_symbol

id_type_mapt	parameter_map

bool	break_is_allowed

bool	continue_is_allowed

bool	case_is_allowed

typet	switch_op_type

typet	return_type

std::map< irep_idt, source_locationt >	labels_defined

std::map< irep_idt, source_locationt >	labels_used

std::list< codet >	clean_code

asm_label_mapt	asm_label_map

Protected Attributes inherited from messaget
message_handlert *	message_handler

mstreamt	mstream

Protected Attributes inherited from namespacet
const symbol_table_baset *	symbol_table1

const symbol_table_baset *	symbol_table2

Additional Inherited Members
Public Types inherited from messaget
enum	message_levelt { M_ERROR =1 , M_WARNING =2 , M_RESULT =4 , M_STATUS =6 , M_STATISTICS =8 , M_PROGRESS =9 , M_DEBUG =10 }

Static Public Member Functions inherited from messaget
static unsigned	eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
	Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest.

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

Static Public Attributes inherited from messaget
static eomt	eom

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

static const commandt	red
	render text with red foreground color

static const commandt	green
	render text with green foreground color

static const commandt	yellow
	render text with yellow foreground color

static const commandt	blue
	render text with blue foreground color

static const commandt	magenta
	render text with magenta foreground color

static const commandt	cyan
	render text with cyan foreground color

static const commandt	bright_red
	render text with bright red foreground color

static const commandt	bright_green
	render text with bright green foreground color

static const commandt	bright_yellow
	render text with bright yellow foreground color

static const commandt	bright_blue
	render text with bright blue foreground color

static const commandt	bright_magenta
	render text with bright magenta foreground color

static const commandt	bright_cyan
	render text with bright cyan foreground color

static const commandt	bold
	render text with bold font

static const commandt	faint
	render text with faint font

static const commandt	italic
	render italic text

static const commandt	underline
	render underlined text

Detailed Description

Definition at line 28 of file c_typecheck_base.h.

Member Typedef Documentation

◆ asm_label_mapt

typedef std::unordered_map<irep_idt, irep_idt> c_typecheck_baset::asm_label_mapt

protected

Definition at line 317 of file c_typecheck_base.h.

◆ id_type_mapt

typedef std::unordered_map<irep_idt, typet> c_typecheck_baset::id_type_mapt

protected

Definition at line 76 of file c_typecheck_base.h.

Constructor & Destructor Documentation

◆ c_typecheck_baset() [1/2]

c_typecheck_baset::c_typecheck_baset	(	symbol_table_baset &	_symbol_table,
		const std::string &	_module,
		message_handlert &	_message_handler
	)

inline

Definition at line 33 of file c_typecheck_base.h.

◆ c_typecheck_baset() [2/2]

c_typecheck_baset::c_typecheck_baset	(	symbol_table_baset &	_symbol_table1,
		const symbol_table_baset &	_symbol_table2,
		const std::string &	_module,
		message_handlert &	_message_handler
	)

inline

Definition at line 48 of file c_typecheck_base.h.

◆ ~c_typecheck_baset()

virtual c_typecheck_baset::~c_typecheck_baset ( )

inlinevirtual

Definition at line 64 of file c_typecheck_base.h.

Member Function Documentation

◆ add_parameters_to_symbol_table()

void c_typecheck_baset::add_parameters_to_symbol_table ( symbolt & symbol )

protected

Create symbols for parameter of the code-typed symbol symbol.

Definition at line 996 of file c_typecheck_base.cpp.

◆ add_rounding_mode()

void c_typecheck_baset::add_rounding_mode ( exprt & expr )

staticprotected

Definition at line 61 of file c_typecheck_expr.cpp.

◆ adjust_float_rel()

void c_typecheck_baset::adjust_float_rel ( binary_relation_exprt & expr )

protectedvirtual

Definition at line 1387 of file c_typecheck_expr.cpp.

◆ adjust_function_parameter()

void c_typecheck_baset::adjust_function_parameter ( typet & type ) const

protectedvirtual

Definition at line 1691 of file c_typecheck_type.cpp.

◆ apply_asm_label()

void c_typecheck_baset::apply_asm_label	(	const irep_idt &	asm_label,
		symbolt &	symbol
	)

protected

Definition at line 656 of file c_typecheck_base.cpp.

◆ builtin_factory()

bool c_typecheck_baset::builtin_factory ( const irep_idt & identifier )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 2127 of file c_typecheck_expr.cpp.

◆ check_history_expr_return_value()

void c_typecheck_baset::check_history_expr_return_value	(	const exprt &	expr,
		std::string &	clause_type
	)

protectedvirtual

Checks that no history expr or return_value exists in expr.

Definition at line 722 of file c_typecheck_base.cpp.

◆ check_was_freed()

void c_typecheck_baset::check_was_freed	(	const exprt &	expr,
		std::string &	clause_type
	)

protectedvirtual

Checks that no occurence of the CPROVER_PREFIX was_freed predicate is found in expr.

Definition at line 749 of file c_typecheck_base.cpp.

◆ designator_enter()

void c_typecheck_baset::designator_enter	(	const typet &	type,
		designatort &	designator
	)

protected

Definition at line 250 of file c_typecheck_initializer.cpp.

◆ disallow_subexpr_by_id()

void c_typecheck_baset::disallow_subexpr_by_id	(	const exprt &	expr,
		const irep_idt &	id,
		const std::string &	message
	)		const

protected

Definition at line 4796 of file c_typecheck_expr.cpp.

◆ do_designated_initializer()

exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer	(	exprt &	result,
		designatort &	designator,
		const exprt &	initializer_list,
		exprt::operandst::const_iterator	init_it,
		bool	force_constant
	)

protectedvirtual

Definition at line 345 of file c_typecheck_initializer.cpp.

◆ do_initializer() [1/2]

void c_typecheck_baset::do_initializer	(	exprt &	initializer,
		const typet &	type,
		bool	force_constant
	)

protectedvirtual

Definition at line 26 of file c_typecheck_initializer.cpp.

◆ do_initializer() [2/2]

void c_typecheck_baset::do_initializer ( symbolt & symbol )

protectedvirtual

Definition at line 224 of file c_typecheck_initializer.cpp.

◆ do_initializer_list()

exprt c_typecheck_baset::do_initializer_list	(	const exprt &	value,
		const typet &	type,
		bool	force_constant
	)

protectedvirtual

Definition at line 909 of file c_typecheck_initializer.cpp.

◆ do_initializer_rec()

exprt c_typecheck_baset::do_initializer_rec	(	const exprt &	value,
		const typet &	type,
		bool	force_constant
	)

protectedvirtual

initialize something of type ‘type’ with given value ‘value’

Definition at line 56 of file c_typecheck_initializer.cpp.

◆ do_special_functions()

exprt c_typecheck_baset::do_special_functions ( side_effect_expr_function_callt & expr )

protectedvirtual

Definition at line 2604 of file c_typecheck_expr.cpp.

◆ enum_constant_type()

typet c_typecheck_baset::enum_constant_type	(	const mp_integer &	min,
		const mp_integer &	max
	)		const

protected

Definition at line 1159 of file c_typecheck_type.cpp.

◆ enum_underlying_type()

bitvector_typet c_typecheck_baset::enum_underlying_type	(	const mp_integer &	min,
		const mp_integer &	max,
		bool	is_packed
	)		const

protected

Definition at line 1191 of file c_typecheck_type.cpp.

◆ gcc_types_compatible_p()

bool c_typecheck_baset::gcc_types_compatible_p	(	const typet &	type1,
		const typet &	type2
	)

protectedvirtual

Definition at line 96 of file c_typecheck_expr.cpp.

◆ gcc_vector_types_compatible()

bool c_typecheck_baset::gcc_vector_types_compatible	(	const vector_typet &	type0,
		const vector_typet &	type1
	)

protected

Definition at line 4069 of file c_typecheck_expr.cpp.

◆ implicit_typecast()

void c_typecheck_baset::implicit_typecast	(	exprt &	expr,
		const typet &	type
	)

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 13 of file c_typecheck_typecast.cpp.

◆ implicit_typecast_arithmetic() [1/2]

void c_typecheck_baset::implicit_typecast_arithmetic ( exprt & expr )

protectedvirtual

Definition at line 68 of file c_typecheck_typecast.cpp.

◆ implicit_typecast_arithmetic() [2/2]

void c_typecheck_baset::implicit_typecast_arithmetic	(	exprt &	expr1,
		exprt &	expr2
	)

protectedvirtual

Definition at line 42 of file c_typecheck_typecast.cpp.

◆ implicit_typecast_bool()

virtual void c_typecheck_baset::implicit_typecast_bool ( exprt & expr )

inlineprotectedvirtual

Definition at line 121 of file c_typecheck_base.h.

◆ increment_designator()

void c_typecheck_baset::increment_designator ( designatort & designator )

protected

Definition at line 706 of file c_typecheck_initializer.cpp.

◆ instantiate_gcc_polymorphic_builtin()

code_blockt c_typecheck_baset::instantiate_gcc_polymorphic_builtin	(	const irep_idt &	identifier,
		const symbol_exprt &	function_symbol
	)

protectedvirtual

Definition at line 1238 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ is_complete_type()

bool c_typecheck_baset::is_complete_type ( const typet & type ) const

protectedvirtual

Definition at line 369 of file c_typecheck_code.cpp.

◆ is_numeric_type()

static bool c_typecheck_baset::is_numeric_type ( const typet & src )

inlinestaticprotected

Definition at line 302 of file c_typecheck_base.h.

◆ make_constant()

void c_typecheck_baset::make_constant ( exprt & expr )

protectedvirtual

Definition at line 4757 of file c_typecheck_expr.cpp.

◆ make_constant_index()

void c_typecheck_baset::make_constant_index ( exprt & expr )

protectedvirtual

Definition at line 4780 of file c_typecheck_expr.cpp.

◆ make_designator()

designatort c_typecheck_baset::make_designator	(	const typet &	type,
		const exprt &	src
	)

protected

Definition at line 756 of file c_typecheck_initializer.cpp.

◆ make_index_type()

void c_typecheck_baset::make_index_type ( exprt & expr )

protectedvirtual

Definition at line 1324 of file c_typecheck_expr.cpp.

◆ move_symbol() [1/2]

void c_typecheck_baset::move_symbol ( symbolt & symbol )

inlineprotected

Definition at line 285 of file c_typecheck_base.h.

◆ move_symbol() [2/2]

void c_typecheck_baset::move_symbol	(	symbolt &	symbol,
		symbolt *&	new_symbol
	)

protected

Definition at line 38 of file c_typecheck_base.cpp.

◆ start_typecheck_code()

void c_typecheck_baset::start_typecheck_code ( )

protectedvirtual

Definition at line 24 of file c_typecheck_code.cpp.

◆ throw_on_side_effects()

void c_typecheck_baset::throw_on_side_effects ( const exprt & expr )

protectedvirtual

Definition at line 867 of file c_typecheck_code.cpp.

◆ to_string() [1/2]

std::string c_typecheck_baset::to_string ( const exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 28 of file c_typecheck_base.cpp.

◆ to_string() [2/2]

std::string c_typecheck_baset::to_string ( const typet & type )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 33 of file c_typecheck_base.cpp.

◆ typecheck()

virtual void c_typecheck_baset::typecheck ( )

pure virtual

Implements typecheckt.

Implemented in ansi_c_typecheckt, and cpp_typecheckt.

◆ typecheck_arithmetic_pointer()

void c_typecheck_baset::typecheck_arithmetic_pointer ( exprt & expr )

protectedvirtual

Definition at line 4298 of file c_typecheck_expr.cpp.

◆ typecheck_array_type()

void c_typecheck_baset::typecheck_array_type ( array_typet & type )

protectedvirtual

Definition at line 576 of file c_typecheck_type.cpp.

◆ typecheck_asm()

void c_typecheck_baset::typecheck_asm ( code_asmt & code )

protectedvirtual

Definition at line 158 of file c_typecheck_code.cpp.

◆ typecheck_assign()

void c_typecheck_baset::typecheck_assign ( codet & expr )

protectedvirtual

Definition at line 192 of file c_typecheck_code.cpp.

◆ typecheck_bitint_type()

void c_typecheck_baset::typecheck_bitint_type ( typet & type )

protectedvirtual

Definition at line 424 of file c_typecheck_type.cpp.

◆ typecheck_block()

void c_typecheck_baset::typecheck_block ( code_blockt & code )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 208 of file c_typecheck_code.cpp.

◆ typecheck_break()

void c_typecheck_baset::typecheck_break ( codet & code )

protectedvirtual

Definition at line 227 of file c_typecheck_code.cpp.

◆ typecheck_builtin_overflow()

exprt c_typecheck_baset::typecheck_builtin_overflow	(	side_effect_expr_function_callt &	expr,
		const irep_idt &	arith_op
	)

protected

Definition at line 3841 of file c_typecheck_expr.cpp.

◆ typecheck_c_bit_field_type()

void c_typecheck_baset::typecheck_c_bit_field_type ( c_bit_field_typet & type )

protectedvirtual

Definition at line 1535 of file c_typecheck_type.cpp.

◆ typecheck_c_enum_tag_type()

void c_typecheck_baset::typecheck_c_enum_tag_type ( c_enum_tag_typet & type )

protectedvirtual

Definition at line 1477 of file c_typecheck_type.cpp.

◆ typecheck_c_enum_type()

void c_typecheck_baset::typecheck_c_enum_type ( typet & type )

protectedvirtual

Definition at line 1249 of file c_typecheck_type.cpp.

◆ typecheck_code()

void c_typecheck_baset::typecheck_code ( codet & code )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 29 of file c_typecheck_code.cpp.

◆ typecheck_code_type()

void c_typecheck_baset::typecheck_code_type ( code_typet & type )

protectedvirtual

Definition at line 480 of file c_typecheck_type.cpp.

◆ typecheck_compound_body()

void c_typecheck_baset::typecheck_compound_body ( struct_union_typet & type )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 921 of file c_typecheck_type.cpp.

◆ typecheck_compound_type()

void c_typecheck_baset::typecheck_compound_type ( struct_union_typet & type )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 789 of file c_typecheck_type.cpp.

◆ typecheck_conditional_targets()

void c_typecheck_baset::typecheck_conditional_targets	(	exprt::operandst &	targets,
		const std::function< void(exprt &)>	typecheck_target,
		const std::string &	clause_type
	)

protectedvirtual

Definition at line 930 of file c_typecheck_code.cpp.

◆ typecheck_continue()

void c_typecheck_baset::typecheck_continue ( codet & code )

protectedvirtual

Definition at line 237 of file c_typecheck_code.cpp.

◆ typecheck_custom_type()

void c_typecheck_baset::typecheck_custom_type ( typet & type )

protectedvirtual

Definition at line 329 of file c_typecheck_type.cpp.

◆ typecheck_decl()

void c_typecheck_baset::typecheck_decl ( codet & code )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 247 of file c_typecheck_code.cpp.

◆ typecheck_declaration()

void c_typecheck_baset::typecheck_declaration ( ansi_c_declarationt & declaration )

protected

Definition at line 770 of file c_typecheck_base.cpp.

◆ typecheck_dowhile()

void c_typecheck_baset::typecheck_dowhile ( code_dowhilet & code )

protectedvirtual

Definition at line 821 of file c_typecheck_code.cpp.

◆ typecheck_expr()

void c_typecheck_baset::typecheck_expr ( exprt & expr )

virtual

Reimplemented in cpp_typecheckt.

Definition at line 46 of file c_typecheck_expr.cpp.

◆ typecheck_expr_address_of()

void c_typecheck_baset::typecheck_expr_address_of ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1798 of file c_typecheck_expr.cpp.

◆ typecheck_expr_alignof()

void c_typecheck_baset::typecheck_expr_alignof ( exprt & expr )

protectedvirtual

Definition at line 1113 of file c_typecheck_expr.cpp.

◆ typecheck_expr_binary_arithmetic()

void c_typecheck_baset::typecheck_expr_binary_arithmetic ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 4098 of file c_typecheck_expr.cpp.

◆ typecheck_expr_binary_boolean()

void c_typecheck_baset::typecheck_expr_binary_boolean ( exprt & expr )

protectedvirtual

Definition at line 4428 of file c_typecheck_expr.cpp.

◆ typecheck_expr_builtin_offsetof()

void c_typecheck_baset::typecheck_expr_builtin_offsetof ( exprt & expr )

protectedvirtual

Definition at line 612 of file c_typecheck_expr.cpp.

◆ typecheck_expr_builtin_va_arg()

void c_typecheck_baset::typecheck_expr_builtin_va_arg ( exprt & expr )

protectedvirtual

Definition at line 541 of file c_typecheck_expr.cpp.

◆ typecheck_expr_comma()

void c_typecheck_baset::typecheck_expr_comma ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 532 of file c_typecheck_expr.cpp.

◆ typecheck_expr_constant()

void c_typecheck_baset::typecheck_expr_constant ( exprt & expr )

protectedvirtual

Definition at line 4022 of file c_typecheck_expr.cpp.

◆ typecheck_expr_cw_va_arg_typeof()

void c_typecheck_baset::typecheck_expr_cw_va_arg_typeof ( exprt & expr )

protectedvirtual

Definition at line 595 of file c_typecheck_expr.cpp.

◆ typecheck_expr_dereference()

void c_typecheck_baset::typecheck_expr_dereference ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1858 of file c_typecheck_expr.cpp.

◆ typecheck_expr_function_identifier()

void c_typecheck_baset::typecheck_expr_function_identifier ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1903 of file c_typecheck_expr.cpp.

◆ typecheck_expr_index()

void c_typecheck_baset::typecheck_expr_index ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1329 of file c_typecheck_expr.cpp.

◆ typecheck_expr_main()

void c_typecheck_baset::typecheck_expr_main ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 175 of file c_typecheck_expr.cpp.

◆ typecheck_expr_member()

void c_typecheck_baset::typecheck_expr_member ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1566 of file c_typecheck_expr.cpp.

◆ typecheck_expr_operands()

void c_typecheck_baset::typecheck_expr_operands ( exprt & expr )

protectedvirtual

Definition at line 771 of file c_typecheck_expr.cpp.

◆ typecheck_expr_pointer_arithmetic()

void c_typecheck_baset::typecheck_expr_pointer_arithmetic ( exprt & expr )

protectedvirtual

Definition at line 4338 of file c_typecheck_expr.cpp.

◆ typecheck_expr_ptrmember()

void c_typecheck_baset::typecheck_expr_ptrmember ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1532 of file c_typecheck_expr.cpp.

◆ typecheck_expr_rel()

void c_typecheck_baset::typecheck_expr_rel ( binary_relation_exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1399 of file c_typecheck_expr.cpp.

◆ typecheck_expr_rel_vector()

void c_typecheck_baset::typecheck_expr_rel_vector ( binary_exprt & expr )

protectedvirtual

Definition at line 1501 of file c_typecheck_expr.cpp.

◆ typecheck_expr_shifts()

void c_typecheck_baset::typecheck_expr_shifts ( shift_exprt & expr )

protectedvirtual

Definition at line 4227 of file c_typecheck_expr.cpp.

◆ typecheck_expr_side_effect()

void c_typecheck_baset::typecheck_expr_side_effect ( side_effect_exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1914 of file c_typecheck_expr.cpp.

◆ typecheck_expr_sizeof()

void c_typecheck_baset::typecheck_expr_sizeof ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 981 of file c_typecheck_expr.cpp.

◆ typecheck_expr_symbol()

void c_typecheck_baset::typecheck_expr_symbol ( exprt & expr )

protectedvirtual

Definition at line 846 of file c_typecheck_expr.cpp.

◆ typecheck_expr_trinary()

void c_typecheck_baset::typecheck_expr_trinary ( if_exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1646 of file c_typecheck_expr.cpp.

◆ typecheck_expr_typecast()

void c_typecheck_baset::typecheck_expr_typecast ( exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 1135 of file c_typecheck_expr.cpp.

◆ typecheck_expr_unary_arithmetic()

void c_typecheck_baset::typecheck_expr_unary_arithmetic ( exprt & expr )

protectedvirtual

Definition at line 4027 of file c_typecheck_expr.cpp.

◆ typecheck_expr_unary_boolean()

void c_typecheck_baset::typecheck_expr_unary_boolean ( exprt & expr )

protectedvirtual

Definition at line 4057 of file c_typecheck_expr.cpp.

◆ typecheck_expression()

void c_typecheck_baset::typecheck_expression ( codet & code )

protectedvirtual

Definition at line 405 of file c_typecheck_code.cpp.

◆ typecheck_for()

void c_typecheck_baset::typecheck_for ( codet & code )

protectedvirtual

Definition at line 419 of file c_typecheck_code.cpp.

◆ typecheck_function_body()

void c_typecheck_baset::typecheck_function_body ( symbolt & symbol )

protected

Definition at line 609 of file c_typecheck_base.cpp.

◆ typecheck_function_call_arguments()

void c_typecheck_baset::typecheck_function_call_arguments ( side_effect_expr_function_callt & expr )

protectedvirtual

Typecheck the parameters in a function call expression, and where necessary, make implicit casts around parameters explicit.

Reimplemented in cpp_typecheckt.

Definition at line 3944 of file c_typecheck_expr.cpp.

◆ typecheck_gcc_computed_goto()

void c_typecheck_baset::typecheck_gcc_computed_goto ( codet & code )

protectedvirtual

Definition at line 603 of file c_typecheck_code.cpp.

◆ typecheck_gcc_local_label()

void c_typecheck_baset::typecheck_gcc_local_label ( codet & code )

protectedvirtual

Definition at line 591 of file c_typecheck_code.cpp.

◆ typecheck_gcc_polymorphic_builtin()

std::optional< symbol_exprt > c_typecheck_baset::typecheck_gcc_polymorphic_builtin	(	const irep_idt &	identifier,
		const exprt::operandst &	arguments,
		const source_locationt &	source_location
	)

protectedvirtual

Definition at line 494 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_gcc_switch_case_range()

void c_typecheck_baset::typecheck_gcc_switch_case_range ( code_gcc_switch_case_ranget & code )

protectedvirtual

Definition at line 572 of file c_typecheck_code.cpp.

◆ typecheck_goto()

void c_typecheck_baset::typecheck_goto ( code_gotot & code )

protectedvirtual

Definition at line 597 of file c_typecheck_code.cpp.

◆ typecheck_ifthenelse()

void c_typecheck_baset::typecheck_ifthenelse ( code_ifthenelset & code )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 626 of file c_typecheck_code.cpp.

◆ typecheck_label()

void c_typecheck_baset::typecheck_label ( code_labelt & code )

protectedvirtual

Definition at line 523 of file c_typecheck_code.cpp.

◆ typecheck_new_symbol()

void c_typecheck_baset::typecheck_new_symbol ( symbolt & symbol )

protected

Definition at line 158 of file c_typecheck_base.cpp.

◆ typecheck_obeys_contract_call()

void c_typecheck_baset::typecheck_obeys_contract_call ( side_effect_expr_function_callt & expr )

protectedvirtual

Checks an obeys_contract predicate occurrence.

Definition at line 2061 of file c_typecheck_expr.cpp.

◆ typecheck_redefinition_non_type()

void c_typecheck_baset::typecheck_redefinition_non_type	(	symbolt &	old_symbol,
		symbolt &	new_symbol
	)

protected

Definition at line 318 of file c_typecheck_base.cpp.

◆ typecheck_redefinition_type()

void c_typecheck_baset::typecheck_redefinition_type	(	symbolt &	old_symbol,
		symbolt &	new_symbol
	)

protected

Definition at line 188 of file c_typecheck_base.cpp.

◆ typecheck_return()

void c_typecheck_baset::typecheck_return ( code_frontend_returnt & code )

protectedvirtual

Definition at line 675 of file c_typecheck_code.cpp.

◆ typecheck_saturating_arithmetic()

exprt c_typecheck_baset::typecheck_saturating_arithmetic ( const side_effect_expr_function_callt & expr )

protected

Definition at line 3904 of file c_typecheck_expr.cpp.

◆ typecheck_shadow_memory_builtin()

std::optional< symbol_exprt > c_typecheck_baset::typecheck_shadow_memory_builtin ( const side_effect_expr_function_callt & expr )

protectedvirtual

Typecheck the function if it is a shadow_memory builtin and return a symbol for it.

Otherwise return empty.

Definition at line 226 of file c_typecheck_shadow_memory_builtin.cpp.

◆ typecheck_shuffle_vector()

exprt c_typecheck_baset::typecheck_shuffle_vector ( const side_effect_expr_function_callt & expr )

protectedvirtual

Definition at line 1403 of file c_typecheck_gcc_polymorphic_builtins.cpp.

◆ typecheck_side_effect_assignment()

void c_typecheck_baset::typecheck_side_effect_assignment ( side_effect_exprt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 4442 of file c_typecheck_expr.cpp.

◆ typecheck_side_effect_function_call()

void c_typecheck_baset::typecheck_side_effect_function_call ( side_effect_expr_function_callt & expr )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 2136 of file c_typecheck_expr.cpp.

◆ typecheck_side_effect_gcc_conditional_expression()

void c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression ( side_effect_exprt & expr )

protectedvirtual

Definition at line 1770 of file c_typecheck_expr.cpp.

◆ typecheck_side_effect_statement_expression()

void c_typecheck_baset::typecheck_side_effect_statement_expression ( side_effect_exprt & expr )

protectedvirtual

Definition at line 948 of file c_typecheck_expr.cpp.

◆ typecheck_spec_assigns()

void c_typecheck_baset::typecheck_spec_assigns ( exprt::operandst & targets )

virtual

Definition at line 983 of file c_typecheck_code.cpp.

◆ typecheck_spec_assigns_target()

void c_typecheck_baset::typecheck_spec_assigns_target ( exprt & target )

protectedvirtual

Definition at line 999 of file c_typecheck_code.cpp.

◆ typecheck_spec_condition()

void c_typecheck_baset::typecheck_spec_condition ( exprt & condition )

protectedvirtual

Definition at line 883 of file c_typecheck_code.cpp.

◆ typecheck_spec_decreases()

void c_typecheck_baset::typecheck_spec_decreases ( codet & code )

protectedvirtual

Definition at line 1109 of file c_typecheck_code.cpp.

◆ typecheck_spec_frees()

void c_typecheck_baset::typecheck_spec_frees ( exprt::operandst & targets )

protectedvirtual

Definition at line 991 of file c_typecheck_code.cpp.

◆ typecheck_spec_frees_target()

void c_typecheck_baset::typecheck_spec_frees_target ( exprt & target )

protectedvirtual

Definition at line 1047 of file c_typecheck_code.cpp.

◆ typecheck_spec_loop_invariant()

void c_typecheck_baset::typecheck_spec_loop_invariant ( codet & code )

protectedvirtual

Definition at line 1092 of file c_typecheck_code.cpp.

◆ typecheck_start_thread()

void c_typecheck_baset::typecheck_start_thread ( codet & code )

protectedvirtual

Definition at line 663 of file c_typecheck_code.cpp.

◆ typecheck_switch()

void c_typecheck_baset::typecheck_switch ( codet & code )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 712 of file c_typecheck_code.cpp.

◆ typecheck_switch_case()

void c_typecheck_baset::typecheck_switch_case ( code_switch_caset & code )

protectedvirtual

Definition at line 536 of file c_typecheck_code.cpp.

◆ typecheck_symbol()

void c_typecheck_baset::typecheck_symbol ( symbolt & symbol )

protected

Definition at line 52 of file c_typecheck_base.cpp.

◆ typecheck_type()

void c_typecheck_baset::typecheck_type ( typet & type )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 34 of file c_typecheck_type.cpp.

◆ typecheck_typed_target_call()

void c_typecheck_baset::typecheck_typed_target_call ( side_effect_expr_function_callt & expr )

protectedvirtual

Definition at line 2006 of file c_typecheck_expr.cpp.

◆ typecheck_typedef_type()

void c_typecheck_baset::typecheck_typedef_type ( typet & type )

protectedvirtual

Definition at line 1644 of file c_typecheck_type.cpp.

◆ typecheck_typeof_type()

void c_typecheck_baset::typecheck_typeof_type ( typet & type )

protectedvirtual

Definition at line 1608 of file c_typecheck_type.cpp.

◆ typecheck_vector_type()

void c_typecheck_baset::typecheck_vector_type ( typet & type )

protectedvirtual

Definition at line 703 of file c_typecheck_type.cpp.

◆ typecheck_while()

void c_typecheck_baset::typecheck_while ( code_whilet & code )

protectedvirtual

Reimplemented in cpp_typecheckt.

Definition at line 775 of file c_typecheck_code.cpp.

Member Data Documentation

◆ asm_label_map

asm_label_mapt c_typecheck_baset::asm_label_map

protected

Definition at line 318 of file c_typecheck_base.h.

◆ break_is_allowed

bool c_typecheck_baset::break_is_allowed

protected

Definition at line 176 of file c_typecheck_base.h.

◆ case_is_allowed

bool c_typecheck_baset::case_is_allowed

protected

Definition at line 178 of file c_typecheck_base.h.

◆ clean_code

std::list<codet> c_typecheck_baset::clean_code

protected

Definition at line 281 of file c_typecheck_base.h.

◆ continue_is_allowed

bool c_typecheck_baset::continue_is_allowed

protected

Definition at line 177 of file c_typecheck_base.h.

◆ current_symbol

symbolt c_typecheck_baset::current_symbol

protected

Definition at line 74 of file c_typecheck_base.h.

◆ labels_defined

std::map<irep_idt, source_locationt> c_typecheck_baset::labels_defined

protected

Definition at line 183 of file c_typecheck_base.h.

◆ labels_used

std::map<irep_idt, source_locationt> c_typecheck_baset::labels_used

protected

Definition at line 183 of file c_typecheck_base.h.

◆ mode

const irep_idt const irep_idt c_typecheck_baset::mode

protected

Definition at line 73 of file c_typecheck_base.h.

◆ parameter_map

id_type_mapt c_typecheck_baset::parameter_map

protected

Definition at line 77 of file c_typecheck_base.h.

◆ return_type

typet c_typecheck_baset::return_type

protected

Definition at line 180 of file c_typecheck_base.h.

◆ switch_op_type

typet c_typecheck_baset::switch_op_type

protected

Definition at line 179 of file c_typecheck_base.h.

◆ symbol_table

symbol_table_baset& c_typecheck_baset::symbol_table

protected

Definition at line 71 of file c_typecheck_base.h.

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

/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_base.h
/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_base.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_code.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_expr.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_initializer.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_type.cpp
/home/runner/work/cbmc/cbmc/src/ansi-c/c_typecheck_typecast.cpp

Public Member Functions

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ asm_label_mapt

◆ id_type_mapt

Constructor & Destructor Documentation

◆ c_typecheck_baset() [1/2]

◆ c_typecheck_baset() [2/2]

◆ ~c_typecheck_baset()

Member Function Documentation

◆ add_parameters_to_symbol_table()

◆ add_rounding_mode()

◆ adjust_float_rel()

◆ adjust_function_parameter()

◆ apply_asm_label()

◆ builtin_factory()

◆ check_history_expr_return_value()

◆ check_was_freed()

◆ designator_enter()

◆ disallow_subexpr_by_id()

◆ do_designated_initializer()

◆ do_initializer() [1/2]

◆ do_initializer() [2/2]

◆ do_initializer_list()

◆ do_initializer_rec()

◆ do_special_functions()

◆ enum_constant_type()

◆ enum_underlying_type()

◆ gcc_types_compatible_p()

◆ gcc_vector_types_compatible()

◆ implicit_typecast()

◆ implicit_typecast_arithmetic() [1/2]

◆ implicit_typecast_arithmetic() [2/2]

◆ implicit_typecast_bool()

◆ increment_designator()

◆ instantiate_gcc_polymorphic_builtin()

◆ is_complete_type()

◆ is_numeric_type()

◆ make_constant()

◆ make_constant_index()

◆ make_designator()

◆ make_index_type()

◆ move_symbol() [1/2]

◆ move_symbol() [2/2]

◆ start_typecheck_code()

◆ throw_on_side_effects()

◆ to_string() [1/2]

◆ to_string() [2/2]

◆ typecheck()

◆ typecheck_arithmetic_pointer()

◆ typecheck_array_type()

◆ typecheck_asm()

◆ typecheck_assign()

◆ typecheck_bitint_type()

◆ typecheck_block()

◆ typecheck_break()

◆ typecheck_builtin_overflow()

◆ typecheck_c_bit_field_type()

◆ typecheck_c_enum_tag_type()

◆ typecheck_c_enum_type()

◆ typecheck_code()

◆ typecheck_code_type()

◆ typecheck_compound_body()

◆ typecheck_compound_type()

◆ typecheck_conditional_targets()

◆ typecheck_continue()

◆ typecheck_custom_type()

◆ typecheck_decl()

◆ typecheck_declaration()

◆ typecheck_dowhile()

◆ typecheck_expr()

◆ typecheck_expr_address_of()

◆ typecheck_expr_alignof()

◆ typecheck_expr_binary_arithmetic()

◆ typecheck_expr_binary_boolean()