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
|
/*******************************************************************\
Module: Unit tests for value_set_abstract_valuet
Author: Jez Higgins
\*******************************************************************/
#include <util/arith_tools.h>
#include <util/namespace.h>
#include <util/symbol_table.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
// NOLINTNEXTLINE(whitespace/line_length)
#include <analyses/variable-sensitivity/interval_abstract_value.h> // IWYU pragma: keep
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
#include <testing-utils/use_catch.h>
SCENARIO(
"value-sets spanning min-max go TOP",
"[core][analyses][variable-sensitivity][value_set_abstract_object][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("{FALSE, TRUE} goes TOP")
{
auto boolInterval =
make_value_set({false_exprt(), true_exprt()}, environment, ns);
EXPECT_TOP(boolInterval);
}
GIVEN("{min(bool), max(bool)} goes TOP")
{
auto boolInterval = make_value_set(
{min_value_exprt(bool_typet()), max_value_exprt(bool_typet())},
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_value_set(
{from_integer(0, c_bool_type), from_integer(1, c_bool_type)},
environment,
ns);
EXPECT_TOP(boolInterval);
}
GIVEN("{min(c_bool), max(c_bool)} goes TOP")
{
auto c_bool_type = bitvector_typet(ID_c_bool, 8);
auto boolInterval = make_value_set(
{min_value_exprt(c_bool_type), max_value_exprt(c_bool_type)},
environment,
ns);
EXPECT_TOP(boolInterval);
}
}
|
