require_expr Namespace Reference

Functions
index_exprt	require_index (const exprt &expr, int expected_index)
	Verify a given exprt is an index_exprt with a a constant value equal to the expected value. More...
index_exprt	require_top_index (const exprt &expr)
	Verify a given exprt is an index_exprt with a nil value as its index. More...
member_exprt	require_member (const exprt &expr, const irep_idt &component_identifier)
	Verify a given exprt is an member_exprt with a component name equal to the component_identifier. More...
symbol_exprt	require_symbol (const exprt &expr, const irep_idt &symbol_name)
	Verify a given exprt is an symbol_exprt with a identifier name equal to the symbol_name. More...
symbol_exprt	require_symbol (const exprt &expr)
	Verify a given exprt is a symbol_exprt. More...
typecast_exprt	require_typecast (const exprt &expr)
	Verify a given exprt is a typecast_expr. More...
side_effect_exprt	require_side_effect_expr (const exprt &expr, const irep_idt &side_effect_statement)
	Verify a given exprt is a side_effect_exprt with appropriate statement. More...

Function Documentation

require_index()

index_exprt require_expr::require_index	(	const exprt &	expr,
		int	expected_index
	)

Verify a given exprt is an index_exprt with a a constant value equal to the expected value.

Parameters

expr	The expression.
expected_index	The constant value that should be the index.

Returns

The expr cast to an index_exprt

Definition at line 26 of file require_expr.cpp.

require_member()

member_exprt require_expr::require_member	(	const exprt &	expr,
		const irep_idt &	component_identifier
	)

Verify a given exprt is an member_exprt with a component name equal to the component_identifier.

Parameters

expr	The expression.
component_identifier	The name of the component that should be being accessed.

Returns

The expr cast to a member_exprt.

Definition at line 55 of file require_expr.cpp.

require_side_effect_expr()

side_effect_exprt require_expr::require_side_effect_expr	(	const exprt &	expr,
		const irep_idt &	side_effect_statement
	)

Verify a given exprt is a side_effect_exprt with appropriate statement.

Parameters

expr	The expression.
side_effect_statement	The kind of side effect that is required

Returns

The expr cast to a side_effect_exprt

Definition at line 99 of file require_expr.cpp.

require_symbol() [1/2]

symbol_exprt require_expr::require_symbol

(

const exprt &

expr

)

Verify a given exprt is a symbol_exprt.

Parameters

expr	The expression.

Returns

The expr cast to a symbol_exprt

Definition at line 80 of file require_expr.cpp.

require_symbol() [2/2]

symbol_exprt require_expr::require_symbol	(	const exprt &	expr,
		const irep_idt &	symbol_name
	)

Verify a given exprt is an symbol_exprt with a identifier name equal to the symbol_name.

Parameters

expr	The expression.
symbol_name	The intended identifier of the symbol

Returns

The expr cast to a symbol_exprt

Definition at line 69 of file require_expr.cpp.

require_top_index()

index_exprt require_expr::require_top_index

(

const exprt &

expr

)

Verify a given exprt is an index_exprt with a nil value as its index.

Parameters

expr	The expression.

Returns

The expr cast to an index_exprt

Definition at line 41 of file require_expr.cpp.

require_typecast()

typecast_exprt require_expr::require_typecast

(

const exprt &

expr

)

Verify a given exprt is a typecast_expr.

Parameters

expr	The expression.

Returns

The expr cast to a typecast_exprt

Definition at line 89 of file require_expr.cpp.