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
semantic type conversion
Definition: std_expr.h:2111
Extract member of struct or union.
Definition: std_expr.h:3869
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.
API to expression classes.
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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.
index_exprt require_top_index(const exprt &expr)
Verify a given exprt is an index_exprt with a nil value as its index.
Base class for all expressions.
Definition: expr.h:42
Expression to hold a symbol (variable)
Definition: std_expr.h:90
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...
An expression containing a side effect.
Definition: std_code.h:1271
typecast_exprt require_typecast(const exprt &expr)
Verify a given exprt is a typecast_expr.
array index operator
Definition: std_expr.h:1462