Skip to content

Commit 51b641d

Browse files
committed
Add unit test for conversion of address of code
1 parent 6a799ff commit 51b641d

File tree

1 file changed

+14
-0
lines changed

1 file changed

+14
-0
lines changed

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1503,6 +1503,20 @@ TEST_CASE(
15031503
smt_bit_vector_constant_termt{0, 48}));
15041504
}
15051505
}
1506+
SECTION("Code symbol")
1507+
{
1508+
config.bv_encoding.object_bits = 8;
1509+
const symbol_exprt function{"opaque", code_typet{{}, void_type()}};
1510+
const address_of_exprt function_pointer{function};
1511+
track_expression_objects(function_pointer, ns, test.object_map);
1512+
INFO("Expression " + function_pointer.pretty(1, 0));
1513+
const auto converted = test.convert(function_pointer);
1514+
CHECK(test.object_map.at(function).unique_id == 2);
1515+
CHECK(
1516+
converted == smt_bit_vector_theoryt::concat(
1517+
smt_bit_vector_constant_termt{2, 8},
1518+
smt_bit_vector_constant_termt{0, 56}));
1519+
}
15061520
}
15071521
SECTION("Invariant checks")
15081522
{

0 commit comments

Comments
 (0)