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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
/*******************************************************************\
Module: Write Stack Unit Tests
Author: DiffBlue Limited.
\*******************************************************************/
/// \file
/// Unit tests for testing of correct tracking of
/// last written location by objects
#include <testing-utils/use_catch.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <util/arith_tools.h>
#include <util/mathematical_types.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/symbol.h>
#include <util/symbol_table.h>
// #include <src/ansi-c/c_to_expr.h>
SCENARIO(
"Constructing two environments to make sure we correctly identify modified "
"symbols",
"[core][analyses][variable-sensitivity][last-written-location]")
{
auto object_factory = variable_sensitivity_object_factoryt::configured_with(
vsd_configt::constant_domain());
GIVEN("Two identifiers that contain integer values")
{
const irep_idt identifier = "hello";
auto first_val = symbol_exprt(identifier, integer_typet());
symbolt first_sym;
first_sym.name = first_val.get_identifier();
auto rhs_val = from_integer(5, integer_typet());
const irep_idt second_identifier = "world";
auto second_val = symbol_exprt(second_identifier, integer_typet());
symbolt second_sym;
second_sym.name = second_val.get_identifier();
symbol_tablet symbol_table;
symbol_table.add(first_sym);
symbol_table.add(second_sym);
namespacet ns(symbol_table);
WHEN("The identifiers get inserted into two environments")
{
abstract_environmentt env(object_factory);
auto first_eval_rhs = env.eval(rhs_val, ns);
auto first_eval_res = env.eval(first_val, ns);
auto second_eval_res = env.eval(second_val, ns);
auto rhs_val_2 = from_integer(10, integer_typet());
auto second_eval_rhs = env.eval(rhs_val_2, ns);
env.assign(first_val, first_eval_rhs, ns);
env.assign(second_val, second_eval_rhs, ns);
abstract_environmentt second_env(object_factory);
second_env.assign(first_val, first_eval_rhs, ns);
second_env.assign(second_val, second_eval_rhs, ns);
THEN("The modified symbols between the two domains should be none")
{
auto changed_vals =
abstract_environmentt::modified_symbols(env, second_env);
REQUIRE(changed_vals.size() == 0);
}
}
}
GIVEN("Two identifiers that contain integer values")
{
const irep_idt identifier = "hello";
auto first_val = symbol_exprt(identifier, integer_typet());
symbolt first_sym;
first_sym.name = first_val.get_identifier();
auto rhs_val = from_integer(5, integer_typet());
const irep_idt second_identifier = "world";
auto second_val = symbol_exprt(second_identifier, integer_typet());
symbolt second_sym;
second_sym.name = second_val.get_identifier();
symbol_tablet symbol_table;
symbol_table.add(first_sym);
symbol_table.add(second_sym);
namespacet ns(symbol_table);
WHEN(
"The identifiers get inserted into two environments, but one of "
"them has a different value in one of the environments")
{
abstract_environmentt env(object_factory);
auto first_eval_rhs = env.eval(rhs_val, ns);
auto first_eval_res = env.eval(first_val, ns);
auto second_eval_res = env.eval(second_val, ns);
auto rhs_val_2 = from_integer(10, integer_typet());
auto second_eval_rhs = env.eval(rhs_val_2, ns);
env.assign(first_val, first_eval_rhs, ns);
env.assign(second_val, second_eval_rhs, ns);
auto rhs_val_3 = from_integer(20, integer_typet());
abstract_environmentt second_env(object_factory);
auto new_rhs_val = second_env.eval(rhs_val_3, ns);
second_env.assign(first_val, first_eval_rhs, ns);
second_env.assign(second_val, new_rhs_val, ns);
THEN("The modified symbols between the two domains should be none")
{
auto changed_vals =
abstract_environmentt::modified_symbols(env, second_env);
REQUIRE(changed_vals.size() == 0);
}
}
}
}
|
