|
| 1 | +/*******************************************************************\ |
| 2 | + Module: Unit tests for variable/sensitivity/abstract_object::merge |
| 3 | + Author: DiffBlue Limited |
| 4 | +\*******************************************************************/ |
| 5 | + |
| 6 | +#include <testing-utils/use_catch.h> |
| 7 | +#include <util/arith_tools.h> |
| 8 | +#include <util/interval.h> |
| 9 | +#include <util/std_types.h> |
| 10 | + |
| 11 | +TEST_CASE("interval::to_string", "[core][analyses][interval]") |
| 12 | +{ |
| 13 | + const signedbv_typet signed_int_type(32); |
| 14 | + const unsignedbv_typet unsigned_int_type(32); |
| 15 | + const auto signed_expr = [&](const int value) { |
| 16 | + return from_integer(value, signed_int_type); |
| 17 | + }; |
| 18 | + const auto unsigned_expr = [&](const int value) { |
| 19 | + return from_integer(value, unsigned_int_type); |
| 20 | + }; |
| 21 | + |
| 22 | + REQUIRE(constant_interval_exprt(signed_expr(1)).to_string() == "[1,1]"); |
| 23 | + REQUIRE( |
| 24 | + constant_interval_exprt(signed_expr(1), signed_expr(2)).to_string() == |
| 25 | + "[1,2]"); |
| 26 | + |
| 27 | + REQUIRE( |
| 28 | + constant_interval_exprt::top(signed_int_type).to_string() == "[MIN,MAX]"); |
| 29 | + |
| 30 | + REQUIRE( |
| 31 | + constant_interval_exprt::top(unsigned_int_type).to_string() == "[0,MAX]"); |
| 32 | + |
| 33 | + REQUIRE( |
| 34 | + constant_interval_exprt(signed_expr(1), max_exprt{signed_int_type}) |
| 35 | + .to_string() == "[1,MAX]"); |
| 36 | + |
| 37 | + REQUIRE( |
| 38 | + constant_interval_exprt(min_exprt{signed_int_type}, signed_expr(1)) |
| 39 | + .to_string() == "[MIN,1]"); |
| 40 | + REQUIRE( |
| 41 | + constant_interval_exprt(min_exprt{unsigned_int_type}, unsigned_expr(1)) |
| 42 | + .to_string() == "[0,1]"); |
| 43 | + |
| 44 | + REQUIRE( |
| 45 | + constant_interval_exprt( |
| 46 | + min_exprt{signed_int_type}, max_exprt{signed_int_type}) |
| 47 | + .to_string() == "[MIN,MAX]"); |
| 48 | + REQUIRE( |
| 49 | + constant_interval_exprt( |
| 50 | + min_exprt{unsigned_int_type}, max_exprt{unsigned_int_type}) |
| 51 | + .to_string() == "[0,MAX]"); |
| 52 | +} |
0 commit comments