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