-
Notifications
You must be signed in to change notification settings - Fork 287
Expand file tree
/
Copy pathrequire_expr.cpp
More file actions
107 lines (93 loc) · 3.58 KB
/
require_expr.cpp
File metadata and controls
107 lines (93 loc) · 3.58 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
/*******************************************************************\
Module: Unit test utilities
Author: Diffblue Ltd.
\*******************************************************************/
/// \file
/// 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.
#include "require_expr.h"
#include <testing-utils/use_catch.h>
#include <util/arith_tools.h>
#include <util/std_code.h>
/// Verify a given exprt is an index_exprt with a a constant value equal to the
/// expected value
/// \param expr: The expression.
/// \param expected_index: The constant value that should be the index.
/// \return The expr cast to an index_exprt
index_exprt require_expr::require_index(const exprt &expr, int expected_index)
{
REQUIRE(expr.id()==ID_index);
const index_exprt &index_expr=to_index_expr(expr);
REQUIRE(index_expr.index().is_constant());
const mp_integer index_integer_value =
numeric_cast_v<mp_integer>(to_constant_expr(index_expr.index()));
REQUIRE(index_integer_value==expected_index);
return index_expr;
}
/// Verify a given exprt is an index_exprt with a nil value as its index
/// \param expr: The expression.
/// \return The expr cast to an index_exprt
index_exprt require_expr::require_top_index(const exprt &expr)
{
REQUIRE(expr.id()==ID_index);
const index_exprt &index_expr=to_index_expr(expr);
REQUIRE(index_expr.index().id()==ID_nil);
return index_expr;
}
/// Verify a given exprt is an member_exprt with a component name equal to the
/// component_identifier
/// \param expr: The expression.
/// \param component_identifier: The name of the component that should be being
/// accessed.
/// \return The expr cast to a member_exprt.
member_exprt require_expr::require_member(
const exprt &expr, const irep_idt &component_identifier)
{
REQUIRE(expr.id()==ID_member);
const member_exprt &member_expr=to_member_expr(expr);
REQUIRE(member_expr.get_component_name()==component_identifier);
return member_expr;
}
/// Verify a given exprt is an symbol_exprt with a identifier name equal to the
/// symbol_name.
/// \param expr: The expression.
/// \param symbol_name: The intended identifier of the symbol
/// \return The expr cast to a symbol_exprt
symbol_exprt require_expr::require_symbol(
const exprt &expr, const irep_idt &symbol_name)
{
const symbol_exprt &symbol_expr = require_symbol(expr);
REQUIRE(symbol_expr.get_identifier()==symbol_name);
return symbol_expr;
}
/// Verify a given exprt is a symbol_exprt.
/// \param expr: The expression.
/// \return The expr cast to a symbol_exprt
symbol_exprt require_expr::require_symbol(const exprt &expr)
{
REQUIRE(expr.id() == ID_symbol);
return to_symbol_expr(expr);
}
/// Verify a given exprt is a typecast_expr.
/// \param expr: The expression.
/// \return The expr cast to a typecast_exprt
typecast_exprt require_expr::require_typecast(const exprt &expr)
{
REQUIRE(expr.id() == ID_typecast);
return to_typecast_expr(expr);
}
/// Verify a given exprt is a side_effect_exprt with appropriate statement.
/// \param expr: The expression.
/// \param side_effect_statement: The kind of side effect that is required
/// \return The expr cast to a side_effect_exprt
side_effect_exprt require_expr::require_side_effect_expr(
const exprt &expr,
const irep_idt &side_effect_statement)
{
REQUIRE(expr.id() == ID_side_effect);
const side_effect_exprt &side_effect_expr = to_side_effect_expr(expr);
REQUIRE(side_effect_expr.get_statement() == side_effect_statement);
return side_effect_expr;
}