Collaboration diagram for goto_check_ct:

Classes
struct	conditiont

Public Types
typedef goto_functionst::goto_functiont	goto_functiont

Public Member Functions
	goto_check_ct (const namespacet &_ns, const optionst &_options, message_handlert &_message_handler)

void	goto_check (const irep_idt &function_identifier, goto_functiont &goto_function)

void	collect_allocations (const goto_functionst &goto_functions)
	Fill the list of allocations allocationst with <address, size> for every allocation instruction. More...

Protected Types
enum	check_statust { ENABLE , DISABLE , CHECKED }
	activation statuses for named checks More...

using	guardt = std::function< exprt(exprt)>

using	conditionst = std::list< conditiont >

typedef std::set< std::pair< exprt, exprt > >	assertionst

typedef optionst::value_listt	error_labelst

typedef std::pair< exprt, exprt >	allocationt

typedef std::list< allocationt >	allocationst

using	named_check_statust = std::optional< std::pair< irep_idt, check_statust > >
	optional (named-check, status) pair More...

Protected Member Functions
void	check_shadow_memory_api_calls (const goto_programt::instructiont &)

void	check_rec_address (const exprt &expr, const guardt &guard)
	Check an address-of expression: if it is a dereference then check the pointer if it is an index then address-check the array and then check the index. More...

void	check_rec_logical_op (const exprt &expr, const guardt &guard)
	Check a logical operation: check each operand in separation while extending the guarding condition as follows. More...

void	check_rec_if (const if_exprt &if_expr, const guardt &guard)
	Check an if expression: check the if-condition alone, and then check the true/false-cases with the guard extended with if-condition and it's negation, respectively. More...

bool	check_rec_member (const member_exprt &member, const guardt &guard)
	Check that a member expression is valid: More...

void	check_rec_div (const div_exprt &div_expr, const guardt &guard)
	Check that a division is valid: check for division by zero, overflow and NaN (for floating point numbers). More...

void	check_rec_arithmetic_op (const exprt &expr, const guardt &guard)
	Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers), and pointer overflow check. More...

void	check_rec (const exprt &expr, const guardt &guard)
	Recursively descend into `expr` and run the appropriate check for each sub-expression, while collecting the condition for the check in `guard`. More...

void	check (const exprt &expr)
	Initiate the recursively analysis of `expr` with its ‘guard’ set to TRUE. More...

void	bounds_check (const exprt &, const guardt &)

void	bounds_check_index (const index_exprt &, const guardt &)

void	bounds_check_bit_count (const unary_exprt &, const guardt &)

void	div_by_zero_check (const div_exprt &, const guardt &)

void	float_div_by_zero_check (const div_exprt &, const guardt &)

void	mod_by_zero_check (const mod_exprt &, const guardt &)

void	mod_overflow_check (const mod_exprt &, const guardt &)
	check a mod expression for the case INT_MIN % -1 More...

void	enum_range_check (const exprt &, const guardt &)

void	undefined_shift_check (const shift_exprt &, const guardt &)

void	pointer_rel_check (const binary_exprt &, const guardt &)

void	pointer_overflow_check (const exprt &, const guardt &)

void	memory_leak_check (const irep_idt &function_id)

void	pointer_validity_check (const dereference_exprt &expr, const exprt &src_expr, const guardt &guard)
	Generates VCCs for the validity of the given dereferencing operation. More...

void	pointer_primitive_check (const exprt &expr, const guardt &guard)
	Generates VCCs to check that pointers passed to pointer primitives are either null or valid. More...

bool	requires_pointer_primitive_check (const exprt &expr)
	Returns true if the given expression is a pointer primitive that requires validation of the operand to guard against misuse. More...

std::optional< goto_check_ct::conditiont >	get_pointer_is_null_condition (const exprt &address, const exprt &size)

conditionst	get_pointer_points_to_valid_memory_conditions (const exprt &address, const exprt &size)

exprt	is_in_bounds_of_some_explicit_allocation (const exprt &pointer, const exprt &size)

conditionst	get_pointer_dereferenceable_conditions (const exprt &address, const exprt &size)

void	integer_overflow_check (const exprt &, const guardt &)

void	conversion_check (const exprt &, const guardt &)

void	float_overflow_check (const exprt &, const guardt &)

void	nan_check (const exprt &, const guardt &)

std::string	array_name (const exprt &)

void	add_guarded_property (const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr, const guardt &guard)
	Include the `asserted_expr` in the code conditioned by the `guard`. More...

void	invalidate (const exprt &lhs)
	Remove all assertions containing the symbol in `lhs` as well as all assertions containing dereference. More...

void	add_active_named_check_pragmas (source_locationt &source_location) const
	Adds "checked" pragmas for all currently active named checks on the given source location. More...

void	add_all_checked_named_check_pragmas (source_locationt &source_location) const
	Adds "checked" pragmas for all named checks on the given source location (prevents any the instanciation of any ulterior check). More...

named_check_statust	match_named_check (const irep_idt &named_check) const
	Matches a named-check string of the form. More...

Protected Attributes
const namespacet &	ns

std::unique_ptr< local_bitvector_analysist >	local_bitvector_analysis

goto_programt::const_targett	current_target

messaget	log

const guardt	identity = [](exprt expr) { return expr; }

goto_programt	new_code

assertionst	assertions

bool	enable_bounds_check

bool	enable_pointer_check

bool	enable_memory_leak_check

bool	enable_memory_cleanup_check

bool	enable_div_by_zero_check

bool	enable_float_div_by_zero_check

bool	enable_enum_range_check

bool	enable_signed_overflow_check

bool	enable_unsigned_overflow_check

bool	enable_pointer_overflow_check

bool	enable_conversion_check

bool	enable_undefined_shift_check

bool	enable_float_overflow_check

bool	enable_simplify

bool	enable_nan_check

bool	retain_trivial

bool	enable_assert_to_assume

bool	enable_pointer_primitive_check

std::map< irep_idt, bool * >	name_to_flag
	Maps a named-check name to the corresponding boolean flag. More...

error_labelst	error_labels

allocationst	allocations

irep_idt	mode

Detailed Description

Definition at line 45 of file goto_check_c.cpp.

Member Typedef Documentation

◆ allocationst

typedef std::list<allocationt> goto_check_ct::allocationst

protected

Definition at line 305 of file goto_check_c.cpp.

◆ allocationt

typedef std::pair<exprt, exprt> goto_check_ct::allocationt

protected

Definition at line 304 of file goto_check_c.cpp.

◆ assertionst

typedef std::set<std::pair<exprt, exprt> > goto_check_ct::assertionst

protected

Definition at line 253 of file goto_check_c.cpp.

◆ conditionst

using goto_check_ct::conditionst = std::list<conditiont>

protected

Definition at line 177 of file goto_check_c.cpp.

◆ error_labelst

typedef optionst::value_listt goto_check_ct::error_labelst

protected

Definition at line 299 of file goto_check_c.cpp.

◆ goto_functiont

typedef goto_functionst::goto_functiont goto_check_ct::goto_functiont

Definition at line 83 of file goto_check_c.cpp.

◆ guardt

using goto_check_ct::guardt = std::function<exprt(exprt)>

protected

Definition at line 102 of file goto_check_c.cpp.

◆ named_check_statust

using goto_check_ct::named_check_statust = std::optional<std::pair<irep_idt, check_statust> >

protected

optional (named-check, status) pair

Definition at line 328 of file goto_check_c.cpp.

Member Enumeration Documentation

◆ check_statust

enum goto_check_ct::check_statust

protected

activation statuses for named checks

Enumerator
ENABLE
DISABLE
CHECKED

Definition at line 320 of file goto_check_c.cpp.

Constructor & Destructor Documentation

◆ goto_check_ct()

goto_check_ct::goto_check_ct	(	const namespacet &	_ns,
		const optionst &	_options,
		message_handlert &	_message_handler
	)

inline

Definition at line 48 of file goto_check_c.cpp.

Member Function Documentation

◆ add_active_named_check_pragmas()

void goto_check_ct::add_active_named_check_pragmas ( source_locationt & source_location ) const

protected

Adds "checked" pragmas for all currently active named checks on the given source location.

Definition at line 2466 of file goto_check_c.cpp.

◆ add_all_checked_named_check_pragmas()

void goto_check_ct::add_all_checked_named_check_pragmas ( source_locationt & source_location ) const

protected

Adds "checked" pragmas for all named checks on the given source location (prevents any the instanciation of any ulterior check).

Definition at line 2474 of file goto_check_c.cpp.

◆ add_guarded_property()

void goto_check_ct::add_guarded_property	(	const exprt &	asserted_expr,
		const std::string &	comment,
		const std::string &	property_class,
		const source_locationt &	source_location,
		const exprt &	src_expr,
		const guardt &	guard
	)

protected

Include the asserted_expr in the code conditioned by the guard.

Parameters

asserted_expr	expression to be asserted
comment	human readable comment
property_class	classification of the property
source_location	the source location of the original expression
src_expr	the original expression to be included in the comment
guard	the condition under which the asserted expression should be taken into account

Definition at line 1715 of file goto_check_c.cpp.

◆ array_name()

std::string goto_check_ct::array_name ( const exprt & expr )

protected

Definition at line 1518 of file goto_check_c.cpp.

◆ bounds_check()

void goto_check_ct::bounds_check	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 1523 of file goto_check_c.cpp.

◆ bounds_check_bit_count()

void goto_check_ct::bounds_check_bit_count	(	const unary_exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 1693 of file goto_check_c.cpp.

◆ bounds_check_index()

void goto_check_ct::bounds_check_index	(	const index_exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 1540 of file goto_check_c.cpp.

◆ check()

void goto_check_ct::check ( const exprt & expr )

protected

Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.

Parameters

expr	the expression to be checked

Definition at line 2021 of file goto_check_c.cpp.

◆ check_rec()

void goto_check_ct::check_rec	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Recursively descend into expr and run the appropriate check for each sub-expression, while collecting the condition for the check in guard.

Parameters

expr	the expression to be checked
guard	the condition for when the check should be made

Definition at line 1931 of file goto_check_c.cpp.

◆ check_rec_address()

void goto_check_ct::check_rec_address	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Check an address-of expression: if it is a dereference then check the pointer if it is an index then address-check the array and then check the index.

Parameters

expr	the expression to be checked
guard	the condition for the check

Definition at line 1761 of file goto_check_c.cpp.

◆ check_rec_arithmetic_op()

void goto_check_ct::check_rec_arithmetic_op	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers), and pointer overflow check.

Parameters

expr	the expression to be checked
guard	the condition for the check

Definition at line 1904 of file goto_check_c.cpp.

◆ check_rec_div()

void goto_check_ct::check_rec_div	(	const div_exprt &	div_expr,
		const guardt &	guard
	)

protected

Check that a division is valid: check for division by zero, overflow and NaN (for floating point numbers).

Parameters

div_expr	the expression to be checked
guard	the condition for the check

Definition at line 1875 of file goto_check_c.cpp.

◆ check_rec_if()

void goto_check_ct::check_rec_if	(	const if_exprt &	if_expr,
		const guardt &	guard
	)

protected

Check an if expression: check the if-condition alone, and then check the true/false-cases with the guard extended with if-condition and it's negation, respectively.

Parameters

if_expr	the expression to be checked
guard	the condition for the check (extended with the (negation of the) if-condition for recursively calls)

Definition at line 1811 of file goto_check_c.cpp.

◆ check_rec_logical_op()

void goto_check_ct::check_rec_logical_op	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Check a logical operation: check each operand in separation while extending the guarding condition as follows.

a /\ b /\ c ==> check(a, TRUE), check(b, a), check (c, a /\ b) a \/ b \/ c ==> check(a, TRUE), check(b, ~a), check (c, ~a /\ ~b)

Parameters

expr	the expression to be checked
guard	the condition for the check (extended with the previous operands (or their negations) for recursively calls)

Definition at line 1784 of file goto_check_c.cpp.

◆ check_rec_member()

bool goto_check_ct::check_rec_member	(	const member_exprt &	member,
		const guardt &	guard
	)

protected

Check that a member expression is valid:

check the structure this expression is a member of (via pointer of its dereference)
run pointer-validity check on ‘*(s+member_offset)’ instead of ‘s->member’ to avoid checking safety of ‘s’
check all operands of the expression
Parameters

member the expression to be checked

guard the condition for the check

Returns
true if no more checks are required for member or its sub-expressions

Definition at line 1834 of file goto_check_c.cpp.

◆ check_shadow_memory_api_calls()

void goto_check_ct::check_shadow_memory_api_calls ( const goto_programt::instructiont & i )

protected

Definition at line 2288 of file goto_check_c.cpp.

◆ collect_allocations()

void goto_check_ct::collect_allocations ( const goto_functionst & goto_functions )

Fill the list of allocations allocationst with <address, size> for every allocation instruction.

Also check that each allocation is well-formed.

Parameters

goto_functions goto functions from which the allocations are to be collected

Definition at line 432 of file goto_check_c.cpp.

◆ conversion_check()

void goto_check_ct::conversion_check	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 681 of file goto_check_c.cpp.

◆ div_by_zero_check()

void goto_check_ct::div_by_zero_check	(	const div_exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 494 of file goto_check_c.cpp.

◆ enum_range_check()

void goto_check_ct::enum_range_check	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 536 of file goto_check_c.cpp.

◆ float_div_by_zero_check()

void goto_check_ct::float_div_by_zero_check	(	const div_exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 515 of file goto_check_c.cpp.

◆ float_overflow_check()

void goto_check_ct::float_overflow_check	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 1089 of file goto_check_c.cpp.

◆ get_pointer_dereferenceable_conditions()

goto_check_ct::conditionst goto_check_ct::get_pointer_dereferenceable_conditions	(	const exprt &	address,
		const exprt &	size
	)

protected

Definition at line 1505 of file goto_check_c.cpp.

◆ get_pointer_is_null_condition()

std::optional< goto_check_ct::conditiont > goto_check_ct::get_pointer_is_null_condition	(	const exprt &	address,
		const exprt &	size
	)

protected

Definition at line 2386 of file goto_check_c.cpp.

◆ get_pointer_points_to_valid_memory_conditions()

goto_check_ct::conditionst goto_check_ct::get_pointer_points_to_valid_memory_conditions	(	const exprt &	address,
		const exprt &	size
	)

protected

Definition at line 2308 of file goto_check_c.cpp.

◆ goto_check()

void goto_check_ct::goto_check	(	const irep_idt &	function_identifier,
		goto_functiont &	goto_function
	)

Definition at line 2048 of file goto_check_c.cpp.

◆ integer_overflow_check()

void goto_check_ct::integer_overflow_check	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 844 of file goto_check_c.cpp.

◆ invalidate()

void goto_check_ct::invalidate ( const exprt & lhs )

protected

Remove all assertions containing the symbol in lhs as well as all assertions containing dereference.

Parameters

lhs	the left-hand-side expression whose symbol should be invalidated

Definition at line 464 of file goto_check_c.cpp.

◆ is_in_bounds_of_some_explicit_allocation()

exprt goto_check_ct::is_in_bounds_of_some_explicit_allocation	(	const exprt &	pointer,
		const exprt &	size
	)

protected

Definition at line 2407 of file goto_check_c.cpp.

◆ match_named_check()

goto_check_ct::named_check_statust goto_check_ct::match_named_check ( const irep_idt & named_check ) const

protected

Matches a named-check string of the form.

("enable"|"disable"|"checked") ":" <named-check>

goto_check_ct::check

void check(const exprt &expr)

Initiate the recursively analysis of expr with its ‘guard’ set to TRUE.

Definition: goto_check_c.cpp:2021

Returns: a pair (name, status) if the match succeeds and the name is known, nothing otherwise.

Definition at line 2482 of file goto_check_c.cpp.

◆ memory_leak_check()

void goto_check_ct::memory_leak_check ( const irep_idt & function_id )

protected

Definition at line 2026 of file goto_check_c.cpp.

◆ mod_by_zero_check()

void goto_check_ct::mod_by_zero_check	(	const mod_exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 627 of file goto_check_c.cpp.

◆ mod_overflow_check()

void goto_check_ct::mod_overflow_check	(	const mod_exprt &	expr,
		const guardt &	guard
	)

protected

check a mod expression for the case INT_MIN % -1

Definition at line 649 of file goto_check_c.cpp.

◆ nan_check()

void goto_check_ct::nan_check	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 1196 of file goto_check_c.cpp.

◆ pointer_overflow_check()

void goto_check_ct::pointer_overflow_check	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 1348 of file goto_check_c.cpp.

◆ pointer_primitive_check()

void goto_check_ct::pointer_primitive_check	(	const exprt &	expr,
		const guardt &	guard
	)

protected

Generates VCCs to check that pointers passed to pointer primitives are either null or valid.

Parameters

expr	the pointer primitive expression
guard	the condition under which the operation happens

Definition at line 1445 of file goto_check_c.cpp.

◆ pointer_rel_check()

void goto_check_ct::pointer_rel_check	(	const binary_exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 1304 of file goto_check_c.cpp.

◆ pointer_validity_check()

void goto_check_ct::pointer_validity_check	(	const dereference_exprt &	expr,
		const exprt &	src_expr,
		const guardt &	guard
	)

protected

Generates VCCs for the validity of the given dereferencing operation.

Parameters

expr	the expression to be checked
src_expr	The expression as found in the program, prior to any rewriting
guard	the condition under which the operation happens

Definition at line 1404 of file goto_check_c.cpp.

◆ requires_pointer_primitive_check()

bool goto_check_ct::requires_pointer_primitive_check ( const exprt & expr )

protected

Returns true if the given expression is a pointer primitive that requires validation of the operand to guard against misuse.

Parameters

expr	expression

Returns: true if the given expression is a pointer primitive that requires checking

Definition at line 1486 of file goto_check_c.cpp.

◆ undefined_shift_check()

void goto_check_ct::undefined_shift_check	(	const shift_exprt &	expr,
		const guardt &	guard
	)

protected

Definition at line 560 of file goto_check_c.cpp.

Member Data Documentation

◆ allocations

allocationst goto_check_ct::allocations

protected

Definition at line 306 of file goto_check_c.cpp.

◆ assertions

assertionst goto_check_ct::assertions

protected

Definition at line 254 of file goto_check_c.cpp.

◆ current_target

goto_programt::const_targett goto_check_ct::current_target

protected

Definition at line 99 of file goto_check_c.cpp.

◆ enable_assert_to_assume

bool goto_check_ct::enable_assert_to_assume

protected

Definition at line 278 of file goto_check_c.cpp.

◆ enable_bounds_check

bool goto_check_ct::enable_bounds_check

protected

Definition at line 262 of file goto_check_c.cpp.

◆ enable_conversion_check

bool goto_check_ct::enable_conversion_check

protected

Definition at line 272 of file goto_check_c.cpp.

◆ enable_div_by_zero_check

bool goto_check_ct::enable_div_by_zero_check

protected

Definition at line 266 of file goto_check_c.cpp.

◆ enable_enum_range_check

bool goto_check_ct::enable_enum_range_check

protected

Definition at line 268 of file goto_check_c.cpp.

◆ enable_float_div_by_zero_check

bool goto_check_ct::enable_float_div_by_zero_check

protected

Definition at line 267 of file goto_check_c.cpp.

◆ enable_float_overflow_check

bool goto_check_ct::enable_float_overflow_check

protected

Definition at line 274 of file goto_check_c.cpp.

◆ enable_memory_cleanup_check

bool goto_check_ct::enable_memory_cleanup_check

protected

Definition at line 265 of file goto_check_c.cpp.

◆ enable_memory_leak_check

bool goto_check_ct::enable_memory_leak_check

protected

Definition at line 264 of file goto_check_c.cpp.

◆ enable_nan_check

bool goto_check_ct::enable_nan_check

protected

Definition at line 276 of file goto_check_c.cpp.

◆ enable_pointer_check

bool goto_check_ct::enable_pointer_check

protected

Definition at line 263 of file goto_check_c.cpp.

◆ enable_pointer_overflow_check

bool goto_check_ct::enable_pointer_overflow_check

protected

Definition at line 271 of file goto_check_c.cpp.

◆ enable_pointer_primitive_check

bool goto_check_ct::enable_pointer_primitive_check

protected

Definition at line 279 of file goto_check_c.cpp.

◆ enable_signed_overflow_check

bool goto_check_ct::enable_signed_overflow_check

protected

Definition at line 269 of file goto_check_c.cpp.

◆ enable_simplify

bool goto_check_ct::enable_simplify

protected

Definition at line 275 of file goto_check_c.cpp.

◆ enable_undefined_shift_check

bool goto_check_ct::enable_undefined_shift_check

protected

Definition at line 273 of file goto_check_c.cpp.

◆ enable_unsigned_overflow_check

bool goto_check_ct::enable_unsigned_overflow_check

protected

Definition at line 270 of file goto_check_c.cpp.

◆ error_labels

error_labelst goto_check_ct::error_labels

protected

Definition at line 300 of file goto_check_c.cpp.

◆ identity

const guardt goto_check_ct::identity = [](exprt expr) { return expr; }

protected

Definition at line 103 of file goto_check_c.cpp.

◆ local_bitvector_analysis

std::unique_ptr<local_bitvector_analysist> goto_check_ct::local_bitvector_analysis

protected

Definition at line 98 of file goto_check_c.cpp.

◆ log

messaget goto_check_ct::log

protected

Definition at line 100 of file goto_check_c.cpp.

◆ mode

irep_idt goto_check_ct::mode

protected

Definition at line 308 of file goto_check_c.cpp.

◆ name_to_flag

std::map<irep_idt, bool *> goto_check_ct::name_to_flag

protected

Initial value:

{
    {"bounds-check", &enable_bounds_check},
    {"pointer-check", &enable_pointer_check},
    {"memory-leak-check", &enable_memory_leak_check},
    {"memory-cleanup-check", &enable_memory_cleanup_check},
    {"div-by-zero-check", &enable_div_by_zero_check},
    {"float-div-by-zero-check", &enable_float_div_by_zero_check},
    {"enum-range-check", &enable_enum_range_check},
    {"signed-overflow-check", &enable_signed_overflow_check},
    {"unsigned-overflow-check", &enable_unsigned_overflow_check},
    {"pointer-overflow-check", &enable_pointer_overflow_check},
    {"conversion-check", &enable_conversion_check},
    {"undefined-shift-check", &enable_undefined_shift_check},
    {"float-overflow-check", &enable_float_overflow_check},
    {"nan-check", &enable_nan_check},
    {"pointer-primitive-check", &enable_pointer_primitive_check}}

Maps a named-check name to the corresponding boolean flag.

Definition at line 282 of file goto_check_c.cpp.

◆ new_code

goto_programt goto_check_ct::new_code

protected

Definition at line 252 of file goto_check_c.cpp.

◆ ns

const namespacet& goto_check_ct::ns

protected

Definition at line 97 of file goto_check_c.cpp.

◆ retain_trivial

bool goto_check_ct::retain_trivial

protected

Definition at line 277 of file goto_check_c.cpp.

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

/home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/goto_check_c.cpp

member	the expression to be checked
guard	the condition for the check

Classes

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ allocationst

◆ allocationt

◆ assertionst

◆ conditionst

◆ error_labelst

◆ goto_functiont

◆ guardt

◆ named_check_statust

Member Enumeration Documentation

◆ check_statust

Constructor & Destructor Documentation

◆ goto_check_ct()

Member Function Documentation

◆ add_active_named_check_pragmas()

◆ add_all_checked_named_check_pragmas()

◆ add_guarded_property()

◆ array_name()

◆ bounds_check()

◆ bounds_check_bit_count()

◆ bounds_check_index()

◆ check()

◆ check_rec()

◆ check_rec_address()

◆ check_rec_arithmetic_op()

◆ check_rec_div()

◆ check_rec_if()

◆ check_rec_logical_op()

◆ check_rec_member()

◆ check_shadow_memory_api_calls()

◆ collect_allocations()

◆ conversion_check()

◆ div_by_zero_check()

◆ enum_range_check()

◆ float_div_by_zero_check()

◆ float_overflow_check()

◆ get_pointer_dereferenceable_conditions()

◆ get_pointer_is_null_condition()

◆ get_pointer_points_to_valid_memory_conditions()

◆ goto_check()

◆ integer_overflow_check()

◆ invalidate()

◆ is_in_bounds_of_some_explicit_allocation()

◆ match_named_check()

◆ memory_leak_check()

◆ mod_by_zero_check()

◆ mod_overflow_check()

◆ nan_check()

◆ pointer_overflow_check()

◆ pointer_primitive_check()

◆ pointer_rel_check()

◆ pointer_validity_check()

◆ requires_pointer_primitive_check()

◆ undefined_shift_check()

Member Data Documentation

◆ allocations

◆ assertions

◆ current_target

◆ enable_assert_to_assume

◆ enable_bounds_check

◆ enable_conversion_check

◆ enable_div_by_zero_check

◆ enable_enum_range_check

◆ enable_float_div_by_zero_check

◆ enable_float_overflow_check

◆ enable_memory_cleanup_check

◆ enable_memory_leak_check

◆ enable_nan_check

◆ enable_pointer_check

◆ enable_pointer_overflow_check

◆ enable_pointer_primitive_check

◆ enable_signed_overflow_check

◆ enable_simplify