Skip to content

Commit b6d7987

Browse files
committed
Unit test of replace_symbolt
1 parent 18d08bf commit b6d7987

File tree

2 files changed

+55
-0
lines changed

2 files changed

+55
-0
lines changed

unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ SRC += unit_tests.cpp \
3535
util/irep_sharing.cpp \
3636
util/message.cpp \
3737
util/optional.cpp \
38+
util/replace_symbol.cpp \
3839
util/sharing_node.cpp \
3940
util/sharing_map.cpp \
4041
util/small_map.cpp \

unit/util/replace_symbol.cpp

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
/*******************************************************************\
2+
3+
Module: replace_symbolt unit tests
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
#include <testing-utils/catch.hpp>
10+
11+
#include <util/replace_symbol.h>
12+
#include <util/std_expr.h>
13+
14+
TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
15+
{
16+
symbol_exprt s1("a", typet("some_type"));
17+
symbol_exprt s2("b", typet("some_type"));
18+
19+
exprt binary("binary", typet("some_type"));
20+
binary.copy_to_operands(s1);
21+
binary.copy_to_operands(s2);
22+
23+
exprt other_expr("other");
24+
25+
replace_symbolt r;
26+
r.insert("a", other_expr);
27+
28+
REQUIRE(r.replace(binary) == false);
29+
REQUIRE(binary.op0() == other_expr);
30+
31+
REQUIRE(r.replace(s1) == false);
32+
REQUIRE(s1 == other_expr);
33+
34+
REQUIRE(r.replace(s2) == true);
35+
REQUIRE(s2 == symbol_exprt("b", typet("some_type")));
36+
}
37+
38+
TEST_CASE("Lvalue only", "[core][util][optional]")
39+
{
40+
symbol_exprt s1("a", typet("some_type"));
41+
symbol_exprt s2("b", typet("some_type"));
42+
43+
exprt binary("binary", typet("some_type"));
44+
binary.copy_to_operands(address_of_exprt(s1));
45+
binary.copy_to_operands(address_of_exprt(s2));
46+
47+
constant_exprt c("some_value", typet("some_type"));
48+
49+
replace_symbolt r;
50+
r.insert("a", c);
51+
52+
REQUIRE(r.replace(binary) == true);
53+
REQUIRE(binary.op0() == address_of_exprt(s1));
54+
}

0 commit comments

Comments
 (0)