Skip to content

Commit 370dd9e

Browse files
committed
Add unit tests for bounded_size
This adds unit tests for the bounded_size function for exprs. Note that the pathological case is designed to break incorrect implementations of bounded size and is intentionally a malformed exprt.
1 parent 6f49723 commit 370dd9e

File tree

1 file changed

+32
-0
lines changed

1 file changed

+32
-0
lines changed

unit/util/expr.cpp

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,3 +36,35 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]")
3636
}
3737
}
3838
}
39+
40+
TEST_CASE("Bounded size is computer correctly", "[core][util][expr]")
41+
{
42+
// Helper types and functions for constructing test expressions.
43+
const typet type = signedbv_typet(32);
44+
std::function<exprt(size_t)> make_expression;
45+
make_expression = [&](size_t size) -> exprt {
46+
PRECONDITION(size != 0);
47+
if(size <= 1)
48+
return from_integer(1, type);
49+
if(size == 2)
50+
return unary_minus_exprt(from_integer(1, type));
51+
return plus_exprt(from_integer(1, type), make_expression(size - 2));
52+
};
53+
// Actual test cases.
54+
REQUIRE(make_expression(1).bounded_size(10) == 1);
55+
REQUIRE(make_expression(2).bounded_size(10) == 2);
56+
REQUIRE(make_expression(3).bounded_size(10) == 3);
57+
58+
REQUIRE(make_expression(30).bounded_size(10) < 13);
59+
REQUIRE(make_expression(30).bounded_size(10) >= 10);
60+
}
61+
62+
TEST_CASE("Bounded size versus pathological example", "[core][util][expr]")
63+
{
64+
const typet type = signedbv_typet(32);
65+
exprt pathology = plus_exprt(from_integer(1, type), from_integer(1, type));
66+
// Create an infinite exprt by self reference!
67+
pathology.add_to_operands(pathology);
68+
// If bounded size is not checking the bound this will never terminate.
69+
REQUIRE(pathology.bounded_size(10) < 13);
70+
}

0 commit comments

Comments
 (0)