cprover
require_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Unit test utilities
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
14 
15 #ifndef CPROVER_TESTING_UTILS_REQUIRE_EXPR_H
16 #define CPROVER_TESTING_UTILS_REQUIRE_EXPR_H
17 
18 #include <util/std_expr.h>
19 #include <util/std_code.h>
20 
21 // NOLINTNEXTLINE(readability/namespace)
22 namespace require_expr
23 {
24  index_exprt require_index(const exprt &expr, int expected_index);
25  index_exprt require_top_index(const exprt &expr);
26 
28  const exprt &expr, const irep_idt &component_identifier);
29 
31  const exprt &expr, const irep_idt &symbol_name);
32 
33  symbol_exprt require_symbol(const exprt &expr);
34 
36 
38  const exprt &expr,
39  const irep_idt &side_effect_statement);
40 }
41 
42 #endif // CPROVER_TESTING_UTILS_REQUIRE_EXPR_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
require_expr::require_typecast
typecast_exprt require_typecast(const exprt &expr)
Verify a given exprt is a typecast_expr.
Definition: require_expr.cpp:89
exprt
Base class for all expressions.
Definition: expr.h:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
require_expr
Definition: require_expr.h:23
require_expr::require_member
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.
Definition: require_expr.cpp:55
require_expr::require_side_effect_expr
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.
Definition: require_expr.cpp:99
require_expr::require_top_index
index_exprt require_top_index(const exprt &expr)
Verify a given exprt is an index_exprt with a nil value as its index.
Definition: require_expr.cpp:41
require_expr::require_symbol
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.
Definition: require_expr.cpp:69
std_code.h
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
index_exprt
Array index operator.
Definition: std_expr.h:1293
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
std_expr.h
API to expression classes.
require_expr::require_index
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.
Definition: require_expr.cpp:26
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866