Helper functions for requiring specific expressions If the expression is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression. More...

#include <util/std_code.h>

Include dependency graph for require_expr.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces
	require_expr

Functions
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. More...

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. More...

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. More...

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. More...

symbol_exprt	require_expr::require_symbol (const exprt &expr)
	Verify a given exprt is a symbol_exprt. More...

typecast_exprt	require_expr::require_typecast (const exprt &expr)
	Verify a given exprt is a typecast_expr. More...

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. More...

Detailed Description

Helper functions for requiring specific expressions If the expression is of the wrong type, throw a CATCH exception Also checks associated properties and returns a casted version of the expression.

Definition in file require_expr.h.

Namespaces

Functions

Detailed Description