diff --git a/unit/Makefile b/unit/Makefile index 5d241997937..57a8063867f 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -161,6 +161,7 @@ SRC += analyses/ai/ai.cpp \ util/optional_utils.cpp \ util/parse_options.cpp \ util/piped_process.cpp \ + util/pointer_expr.cpp \ util/pointer_offset_size.cpp \ util/prefix_filter.cpp \ util/range.cpp \ diff --git a/unit/util/pointer_expr.cpp b/unit/util/pointer_expr.cpp new file mode 100644 index 00000000000..91c8e0cbfa1 --- /dev/null +++ b/unit/util/pointer_expr.cpp @@ -0,0 +1,124 @@ +// Author: Diffblue Ltd. + +#include +#include +#include + +#include +#include + +TEST_CASE("pointer_offset_exprt", "[core][util]") +{ + const exprt pointer = symbol_exprt{"foo", pointer_type(void_type())}; + const pointer_offset_exprt pointer_offset{pointer, signed_size_type()}; + SECTION("Is equivalent to free function.") + { + CHECK(::pointer_offset(pointer) == pointer_offset); + } + SECTION("Result type") + { + CHECK(pointer_offset.type() == signed_size_type()); + } + SECTION("Pointer operand accessor") + { + CHECK(pointer_offset.pointer() == pointer); + } + SECTION("Downcasting") + { + const exprt &upcast = pointer_offset; + CHECK(expr_try_dynamic_cast(pointer_offset)); + CHECK_FALSE(expr_try_dynamic_cast(upcast)); + SECTION("Validation") + { + SECTION("Invalid operand") + { + unary_exprt invalid_type = pointer_offset; + invalid_type.op().type() = bool_typet{}; + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(invalid_type), + invariant_failedt, + invariant_failure_containing( + "pointer_offset must have pointer-typed operand")); + } + SECTION("Missing operand") + { + exprt missing_operand = pointer_offset; + missing_operand.operands().clear(); + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(missing_operand), + invariant_failedt, + invariant_failure_containing("pointer_offset must have one operand")); + } + SECTION("Too many operands") + { + exprt two_operands = pointer_offset; + two_operands.operands().push_back(pointer); + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(two_operands), + invariant_failedt, + invariant_failure_containing("pointer_offset must have one operand")); + } + } + } +} + +TEST_CASE("pointer_object_exprt", "[core][util]") +{ + const exprt pointer = symbol_exprt{"foo", pointer_type(void_type())}; + const pointer_object_exprt pointer_object{pointer, size_type()}; + SECTION("Is equivalent to free function.") + { + CHECK(::pointer_object(pointer) == pointer_object); + } + SECTION("Result type") + { + CHECK(pointer_object.type() == size_type()); + } + SECTION("Pointer operand accessor") + { + CHECK(pointer_object.pointer() == pointer); + } + SECTION("Downcasting") + { + const exprt &upcast = pointer_object; + CHECK(expr_try_dynamic_cast(pointer_object)); + CHECK_FALSE(expr_try_dynamic_cast(upcast)); + SECTION("Validation") + { + SECTION("Invalid operand") + { + unary_exprt invalid_type = pointer_object; + invalid_type.op().type() = bool_typet{}; + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(invalid_type), + invariant_failedt, + invariant_failure_containing( + "pointer_object must have pointer-typed operand")); + } + SECTION("Missing operand") + { + exprt missing_operand = pointer_object; + missing_operand.operands().clear(); + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(missing_operand), + invariant_failedt, + invariant_failure_containing("pointer_object must have one operand")); + } + SECTION("Too many operands") + { + exprt two_operands = pointer_object; + two_operands.operands().push_back(pointer); + const cbmc_invariants_should_throwt invariants_throw; + REQUIRE_THROWS_MATCHES( + expr_try_dynamic_cast(two_operands), + invariant_failedt, + invariant_failure_containing("pointer_object must have one operand")); + } + } + } +}