diff --git a/unit/Makefile b/unit/Makefile index 8757d39c42b..eeff4e499fe 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -35,6 +35,7 @@ SRC += unit_tests.cpp \ util/irep_sharing.cpp \ util/message.cpp \ util/optional.cpp \ + util/replace_symbol.cpp \ util/sharing_node.cpp \ util/sharing_map.cpp \ util/small_map.cpp \ diff --git a/unit/util/replace_symbol.cpp b/unit/util/replace_symbol.cpp new file mode 100644 index 00000000000..ad5190c8353 --- /dev/null +++ b/unit/util/replace_symbol.cpp @@ -0,0 +1,66 @@ +/*******************************************************************\ + + Module: replace_symbolt unit tests + + Author: Michael Tautschnig + +\*******************************************************************/ + +#include + +#include +#include + +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")); + + exprt binary("binary", typet("some_type")); + binary.copy_to_operands(s1); + binary.copy_to_operands(s2); + + array_typet array_type(typet("sub-type"), s1); + REQUIRE(array_type.size() == s1); + + exprt other_expr("other"); + + replace_symbolt r; + r.insert("a", other_expr); + + REQUIRE(r.replace(binary) == false); + REQUIRE(binary.op0() == other_expr); + + REQUIRE(r.replace(s1) == false); + REQUIRE(s1 == other_expr); + + REQUIRE(r.replace(s2) == true); + REQUIRE(s2 == symbol_exprt("b", typet("some_type"))); + + REQUIRE(r.replace(array_type) == false); + REQUIRE(array_type.size() == other_expr); +} + +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); + + exprt binary("binary", typet("some_type")); + binary.copy_to_operands(address_of_exprt(s1)); + binary.copy_to_operands(address_of_exprt(index)); + + constant_exprt c("some_value", typet("some_type")); + + replace_symbolt r; + r.insert("a", c); + + REQUIRE(r.replace(binary) == false); + 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); +}