cprover
Loading...
Searching...
No Matches
require_expr.h File Reference

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

namespace  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.
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.
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.
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.
symbol_exprt require_expr::require_symbol (const exprt &expr)
 Verify a given exprt is a symbol_exprt.
typecast_exprt require_expr::require_typecast (const exprt &expr)
 Verify a given exprt is a typecast_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.

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.