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: replace_symbolt unit tests
Author: Michael Tautschnig
\*******************************************************************/
#include <testing-utils/use_catch.h>
#include <util/pointer_expr.h>
#include <util/replace_symbol.h>
#include <util/std_expr.h>
TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
{
symbol_exprt s1("a", typet("some_type"));
symbol_exprt s2("b", typet("some_type"));
binary_exprt binary(s1, "binary", s2, typet("some_type"));
array_typet array_type(typet("sub-type"), s1);
REQUIRE(array_type.size() == s1);
exprt other_expr("other", typet("some_type"));
replace_symbolt r;
REQUIRE(r.empty());
r.insert(s1, other_expr);
REQUIRE(r.replaces_symbol("a"));
REQUIRE(r.get_expr_map().size() == 1);
REQUIRE(!r.replace(binary));
REQUIRE(binary.op0() == other_expr);
REQUIRE(!r.replace(s1));
REQUIRE(s1 == other_expr);
REQUIRE(r.replace(s2));
REQUIRE(s2 == symbol_exprt("b", typet("some_type")));
REQUIRE(!r.replace(array_type));
REQUIRE(array_type.size() == other_expr);
REQUIRE(r.erase("a") == 1);
REQUIRE(r.empty());
}
TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
{
symbol_exprt s1("a", typet("some_type"));
array_typet array_type(typet("some_type"), s1);
symbol_exprt array("b", array_type);
index_exprt index(array, s1);
binary_exprt binary(
address_of_exprt(s1),
"binary",
address_of_exprt(index),
typet("some_type"));
constant_exprt c("some_value", typet("some_type"));
address_of_aware_replace_symbolt r;
r.insert(s1, c);
REQUIRE(!r.replace(binary));
REQUIRE(binary.op0() == address_of_exprt(s1));
const index_exprt &index_expr =
to_index_expr(to_address_of_expr(binary.op1()).object());
REQUIRE(to_array_type(index_expr.array().type()).size() == c);
REQUIRE(index_expr.index() == c);
address_of_exprt address_of(s1);
r.erase("a");
r.insert(s1, address_of);
REQUIRE(r.replace(binary));
REQUIRE(binary.op0() == address_of_exprt(s1));
}
TEST_CASE("Replace always", "[core][util][replace_symbol]")
{
symbol_exprt s1("a", typet("some_type"));
array_typet array_type(typet("some_type"), s1);
symbol_exprt array("b", array_type);
index_exprt index(array, s1);
binary_exprt binary(
address_of_exprt(s1),
"binary",
address_of_exprt(index),
typet("some_type"));
constant_exprt c("some_value", typet("some_type"));
unchecked_replace_symbolt r;
r.insert(s1, c);
REQUIRE(!r.replace(binary));
REQUIRE(binary.op0() == address_of_exprt(c));
const index_exprt &index_expr =
to_index_expr(to_address_of_expr(binary.op1()).object());
REQUIRE(to_array_type(index_expr.array().type()).size() == c);
REQUIRE(index_expr.index() == c);
}
|
