Skip to content

Commit b5ed1f8

Browse files
Unit test the symex_level1t::has method
Add condition in the unit test to check the result is as expected.
1 parent 79c3ef5 commit b5ed1f8

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

unit/goto-symex/symex_level1.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]")
3838
{
3939
THEN("Renaming leaves it unchanged")
4040
{
41+
REQUIRE(!symex_level1.has(l0_symbol));
4142
auto renamed = symex_level1(l0_symbol);
4243
REQUIRE(renamed.get().get_identifier() == "foo!50");
4344
}
@@ -48,6 +49,7 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]")
4849
symex_level1.insert(l0_symbol, 12134);
4950
THEN("The symbol is renamed to the index inserted")
5051
{
52+
REQUIRE(symex_level1.has(l0_symbol));
5153
auto renamed = symex_level1(l0_symbol);
5254
REQUIRE(renamed.get().get_identifier() == "foo!50@12134");
5355
}
@@ -63,6 +65,7 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]")
6365
auto renamed2 = symex_level1(l0_symbol);
6466
REQUIRE(renamed2.get().get_identifier() == "foo!50@43950");
6567
}
68+
REQUIRE(symex_level1.has(l0_symbol));
6669
}
6770

6871
WHEN("insert_or_replace is called with a symbol not already inserted")
@@ -74,6 +77,7 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]")
7477
}
7578
THEN("The symbol is renamed to the index inserted")
7679
{
80+
REQUIRE(symex_level1.has(l0_symbol));
7781
auto renamed = symex_level1(l0_symbol);
7882
REQUIRE(renamed.get().get_identifier() == "foo!50@20051");
7983
}

0 commit comments

Comments
 (0)