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().id()==ID_constant);
31 const mp_integer index_integer_value =
32 numeric_cast_v<mp_integer>(to_constant_expr(index_expr.index()));
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}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
irep_idt get_component_name() const
Definition: std_expr.h:2681
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:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Semantic type conversion.
Definition: std_expr.h:1920
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:12
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:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189