cprover
Loading...
Searching...
No Matches
require_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unit test utilities
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
14
15#include "require_expr.h"
16
18#include <util/arith_tools.h>
19#include <util/std_code.h>
20
26index_exprt require_expr::require_index(const exprt &expr, int expected_index)
27{
28 REQUIRE(expr.id()==ID_index);
29 const index_exprt &index_expr=to_index_expr(expr);
30 REQUIRE(index_expr.index().is_constant());
31 const mp_integer index_integer_value =
33 REQUIRE(index_integer_value==expected_index);
34
35 return index_expr;
36}
37
42{
43 REQUIRE(expr.id()==ID_index);
44 const index_exprt &index_expr=to_index_expr(expr);
45 REQUIRE(index_expr.index().id()==ID_nil);
46 return index_expr;
47}
48
56 const exprt &expr, const irep_idt &component_identifier)
57{
58 REQUIRE(expr.id()==ID_member);
59 const member_exprt &member_expr=to_member_expr(expr);
60 REQUIRE(member_expr.get_component_name()==component_identifier);
61 return member_expr;
62}
63
70 const exprt &expr, const irep_idt &symbol_name)
71{
72 const symbol_exprt &symbol_expr = require_symbol(expr);
73 REQUIRE(symbol_expr.get_identifier()==symbol_name);
74 return symbol_expr;
75}
76
81{
82 REQUIRE(expr.id() == ID_symbol);
83 return to_symbol_expr(expr);
84}
85
90{
91 REQUIRE(expr.id() == ID_typecast);
92 return to_typecast_expr(expr);
93}
94
100 const exprt &expr,
101 const irep_idt &side_effect_statement)
102{
103 REQUIRE(expr.id() == ID_side_effect);
104 const side_effect_exprt &side_effect_expr = to_side_effect_expr(expr);
105 REQUIRE(side_effect_expr.get_statement() == side_effect_statement);
106 return side_effect_expr;
107}
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
Base class for all expressions.
Definition expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
const irep_idt & id() const
Definition irep.h:388
Extract member of struct or union.
Definition std_expr.h:2972
irep_idt get_component_name() const
Definition std_expr.h:2994
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
Semantic type conversion.
Definition std_expr.h:2073
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.
typecast_exprt require_typecast(const exprt &expr)
Verify a given exprt is a typecast_expr.
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.
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.
index_exprt require_top_index(const exprt &expr)
Verify a given exprt is an index_exprt with a nil value as its index.
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.
Helper functions for requiring specific expressions If the expression is of the wrong type,...
BigInt mp_integer
Definition smt_terms.h:17
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3064
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3173
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
dstringt irep_idt