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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
/*******************************************************************\
Module: Unit tests for interval_abstract_valuet
Author: Jez Higgins
\*******************************************************************/
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
// NOLINTNEXTLINE(whitespace/line_length)
#include <analyses/variable-sensitivity/interval_abstract_value.h> // IWYU pragma: keep
#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
#include <testing-utils/use_catch.h>
static void
verify_extreme_interval(typet type, abstract_environmentt &env, namespacet &ns)
{
auto interval =
make_interval(min_value_exprt(type), max_value_exprt(type), env, ns);
EXPECT_TOP(interval);
}
SCENARIO(
"extreme intervals go TOP",
"[core][analyses][variable-sensitivity][interval_abstract_value][extreme]")
{
auto object_factory = variable_sensitivity_object_factoryt::configured_with(
vsd_configt::intervals());
auto environment = abstract_environmentt{object_factory};
environment.make_top();
auto symbol_table = symbol_tablet{};
auto ns = namespacet{symbol_table};
GIVEN("[min-max] signed goes TOP")
{
verify_extreme_interval(signedbv_typet(32), environment, ns);
}
GIVEN("[min-max] unsigned goes TOP")
{
verify_extreme_interval(unsignedbv_typet(32), environment, ns);
}
GIVEN("[min-max] bool goes TOP")
{
verify_extreme_interval(bool_typet(), environment, ns);
}
GIVEN("[min-max] c_bool goes TOP")
{
verify_extreme_interval(bitvector_typet(ID_c_bool, 8), environment, ns);
}
GIVEN("[FALSE, TRUE] goes TOP")
{
auto boolInterval =
make_interval(false_exprt(), true_exprt(), environment, ns);
EXPECT_TOP(boolInterval);
}
GIVEN("[0, 1] c_bool goes TOP")
{
auto c_bool_type = bitvector_typet(ID_c_bool, 8);
auto boolInterval = make_interval(
from_integer(0, c_bool_type),
from_integer(1, c_bool_type),
environment,
ns);
EXPECT_TOP(boolInterval);
}
}
|
