Skip to content

Commit 2459be5

Browse files
martin-csmartin-cs
authored
Merge pull request #2 from chrisr-diffblue/variable-sensitivity-rebase-fixups
Fixup variable-sensitivity unit tests to build after the giant rebase.
2 parents 53063f1 + ca7a23b commit 2459be5

File tree

6 files changed

+121
-123
lines changed

6 files changed

+121
-123
lines changed

‎unit/analyses/variable-sensitivity/abstract_object/merge.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
77
\*******************************************************************/
88

9-
#include <catch.hpp>
9+
#include <testing-utils/catch.hpp>
1010

1111
#include <analyses/variable-sensitivity/abstract_object.h>
1212
#include <util/std_types.h>

‎unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp

+5-10
Original file line numberDiff line numberDiff line change
@@ -7,29 +7,24 @@
77
\*******************************************************************/
88

99
#include <typeinfo>
10-
#include <catch.hpp>
10+
#include <testing-utils/catch.hpp>
1111
#include <util/namespace.h>
1212
#include <util/symbol_table.h>
1313
#include <util/std_expr.h>
1414
#include <analyses/variable-sensitivity/abstract_enviroment.h>
1515
#include <analyses/variable-sensitivity/abstract_object.h>
1616
#include <analyses/variable-sensitivity/constant_abstract_value.h>
17+
#include <util/arith_tools.h>
18+
#include <util/c_types.h>
1719

1820

19-
// Debug printer for irept
20-
std::ostream &operator<<(std::ostream &os, const irept &value)
21-
{
22-
os << value.pretty();
23-
return os;
24-
}
25-
2621
SCENARIO("merge_constant_abstract_value",
2722
"[core][analyses][variable-sensitivity][constant_abstract_value][merge]")
2823
{
2924
GIVEN("An environment with two values: 1 and 2")
3025
{
31-
const exprt val1=constant_exprt::integer_constant(1);
32-
const exprt val2=constant_exprt::integer_constant(2);
26+
const exprt val1=from_integer(1, integer_typet());
27+
const exprt val2=from_integer(2, integer_typet());
3328

3429
abstract_environmentt enviroment;
3530
enviroment.make_top();

‎unit/analyses/variable-sensitivity/constant_array_abstract_object/merge.cpp

+12-11
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
\*******************************************************************/
88

99
#include <typeinfo>
10-
#include <catch.hpp>
10+
#include <testing-utils/catch.hpp>
1111
#include <util/namespace.h>
1212
#include <util/options.h>
1313
#include <util/symbol_table.h>
@@ -20,6 +20,7 @@
2020
#include <analyses/variable-sensitivity/abstract_object.h>
2121
#include <analyses/variable-sensitivity/constant_array_abstract_object.h>
2222
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
23+
#include <util/arith_tools.h>
2324

2425
typedef constant_array_abstract_objectt::constant_array_pointert
2526
constant_array_abstract_object_pointert;
@@ -74,27 +75,27 @@ SCENARIO("merge_constant_array_abstract_object",
7475
GIVEN("Two arrays of size 3, whose first elements are the same")
7576
{
7677
const array_typet array_type(
77-
integer_typet(), constant_exprt::integer_constant(3));
78+
integer_typet(), from_integer(3, integer_typet()));
7879

7980
// int val1[3] = {1, 2, 3}
8081
exprt val1=array_exprt(array_type);
81-
val1.operands().push_back(constant_exprt::integer_constant(1));
82-
val1.operands().push_back(constant_exprt::integer_constant(2));
83-
val1.operands().push_back(constant_exprt::integer_constant(3));
82+
val1.operands().push_back(from_integer(1, integer_typet()));
83+
val1.operands().push_back(from_integer(2, integer_typet()));
84+
val1.operands().push_back(from_integer(3, integer_typet()));
8485

8586
// int val2[3] = {1, 4, 5}
8687
exprt val2=array_exprt(array_type);
87-
val2.operands().push_back(constant_exprt::integer_constant(1));
88-
val2.operands().push_back(constant_exprt::integer_constant(4));
89-
val2.operands().push_back(constant_exprt::integer_constant(5));
88+
val2.operands().push_back(from_integer(1, integer_typet()));
89+
val2.operands().push_back(from_integer(4, integer_typet()));
90+
val2.operands().push_back(from_integer(5, integer_typet()));
9091

9192
// index_exprt for reading from an array
9293
const index_exprt i0=
93-
index_exprt(nil_exprt(), constant_exprt::integer_constant(0));
94+
index_exprt(nil_exprt(), from_integer(0, integer_typet()));
9495
const index_exprt i1=
95-
index_exprt(nil_exprt(), constant_exprt::integer_constant(1));
96+
index_exprt(nil_exprt(), from_integer(1, integer_typet()));
9697
const index_exprt i2=
97-
index_exprt(nil_exprt(), constant_exprt::integer_constant(2));
98+
index_exprt(nil_exprt(), from_integer(2, integer_typet()));
9899

99100
abstract_environmentt enviroment;
100101
enviroment.make_top();

‎unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp

+12-11
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
\*******************************************************************/
88

99
#include <typeinfo>
10-
#include <catch.hpp>
10+
#include <testing-utils/catch.hpp>
1111
#include <util/namespace.h>
1212
#include <util/options.h>
1313
#include <util/symbol_table.h>
@@ -23,6 +23,7 @@
2323

2424

2525
#include <iostream>
26+
#include <util/arith_tools.h>
2627

2728
typedef constant_array_abstract_objectt::constant_array_pointert
2829
constant_array_abstract_object_pointert;
@@ -64,7 +65,7 @@ class struct_utilt
6465
enviroment,
6566
ns,
6667
std::stack<exprt>(),
67-
member_exprt(nil_exprt(), component.get_name()),
68+
member_exprt(nil_exprt(), component.get_name(), component.type()),
6869
enviroment.eval(op, ns),
6970
false);
7071
result=
@@ -112,20 +113,20 @@ SCENARIO("merge_full_struct_abstract_object",
112113
struct_type.components().push_back(comp_c);
113114

114115
struct_exprt val1(struct_type);
115-
val1.operands().push_back(constant_exprt::integer_constant(1));
116-
val1.operands().push_back(constant_exprt::integer_constant(2));
117-
val1.operands().push_back(constant_exprt::integer_constant(3));
116+
val1.operands().push_back(from_integer(1, integer_typet()));
117+
val1.operands().push_back(from_integer(2, integer_typet()));
118+
val1.operands().push_back(from_integer(3, integer_typet()));
118119

119120
// struct val1 = {.a = 1, .b = 4, .c = 5}
120121
struct_exprt val2(struct_type);
121-
val2.operands().push_back(constant_exprt::integer_constant(1));
122-
val2.operands().push_back(constant_exprt::integer_constant(4));
123-
val2.operands().push_back(constant_exprt::integer_constant(5));
122+
val2.operands().push_back(from_integer(1, integer_typet()));
123+
val2.operands().push_back(from_integer(4, integer_typet()));
124+
val2.operands().push_back(from_integer(5, integer_typet()));
124125

125126
// index_exprt for reading from an array
126-
const member_exprt a(nil_exprt(), "a");
127-
const member_exprt b(nil_exprt(), "b");
128-
const member_exprt c(nil_exprt(), "c");
127+
const member_exprt a(nil_exprt(), "a", integer_typet());
128+
const member_exprt b(nil_exprt(), "b", integer_typet());
129+
const member_exprt c(nil_exprt(), "c", integer_typet());
129130

130131
abstract_environmentt enviroment;
131132
enviroment.make_top();

‎unit/analyses/variable-sensitivity/last_written_location.cpp

+90-89
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
/// Unit tests for testing of correct tracking of
1111
/// last written location by objects
1212

13-
#include "catch.hpp"
13+
#include <testing-utils/catch.hpp>
1414

1515
#include <iostream>
1616
#include <string>
@@ -23,104 +23,105 @@
2323
#include <util/namespace.h>
2424
#include <util/type.h>
2525
#include <analyses/variable-sensitivity/abstract_enviroment.h>
26+
#include <util/arith_tools.h>
2627

2728
//#include <src/ansi-c/c_to_expr.h>
2829

2930
SCENARIO("Constructing two environments to make sure we correctly identify modified symbols",
3031
"[core][analyses][variable-sensitivity][last-written-location]")
3132
{
32-
GIVEN("Two identifiers that contain integer values")
33+
GIVEN("Two identifiers that contain integer values")
34+
{
35+
const irep_idt identifier = "hello";
36+
auto first_val = symbol_exprt(identifier, integer_typet());
37+
symbolt first_sym;
38+
first_sym.name = first_val.get_identifier();
39+
40+
auto rhs_val = from_integer(5, integer_typet());
41+
42+
const irep_idt second_identifier = "world";
43+
auto second_val = symbol_exprt(second_identifier, integer_typet());
44+
symbolt second_sym;
45+
second_sym.name = second_val.get_identifier();
46+
47+
symbol_tablet symbol_table;
48+
49+
symbol_table.add(first_sym);
50+
symbol_table.add(second_sym);
51+
namespacet ns(symbol_table);
52+
53+
WHEN("The identifiers get inserted into two environments")
3354
{
34-
const irep_idt identifier = "hello";
35-
auto first_val = symbol_exprt(identifier, integer_typet());
36-
symbolt first_sym;
37-
first_sym.name = first_val.get_identifier();
38-
39-
auto rhs_val = constant_exprt::integer_constant(5);
40-
41-
const irep_idt second_identifier = "world";
42-
auto second_val = symbol_exprt(second_identifier, integer_typet());
43-
symbolt second_sym;
44-
second_sym.name = second_val.get_identifier();
45-
46-
symbol_tablet symbol_table;
47-
48-
symbol_table.add(first_sym);
49-
symbol_table.add(second_sym);
50-
namespacet ns(symbol_table);
51-
52-
WHEN("The identifiers get inserted into two environments")
53-
{
54-
abstract_environmentt env;
55-
56-
auto first_eval_rhs = env.eval(rhs_val, ns);
57-
auto first_eval_res = env.eval(first_val, ns);
58-
59-
auto second_eval_res = env.eval(second_val, ns);
60-
auto rhs_val_2 = constant_exprt::integer_constant(10);
61-
auto second_eval_rhs = env.eval(rhs_val_2, ns);
62-
63-
env.assign(first_val, first_eval_rhs, ns);
64-
env.assign(second_val, second_eval_rhs, ns);
65-
66-
abstract_environmentt second_env;
67-
second_env.assign(first_val, first_eval_rhs, ns);
68-
second_env.assign(second_val, second_eval_rhs, ns);
69-
70-
THEN("The modified symbols between the two domains should be none") {
71-
auto changed_vals = abstract_environmentt::modified_symbols(
72-
env, second_env);
73-
REQUIRE(changed_vals.size() == 0);
74-
}
55+
abstract_environmentt env;
56+
57+
auto first_eval_rhs = env.eval(rhs_val, ns);
58+
auto first_eval_res = env.eval(first_val, ns);
59+
60+
auto second_eval_res = env.eval(second_val, ns);
61+
auto rhs_val_2 = from_integer(10, integer_typet());
62+
auto second_eval_rhs = env.eval(rhs_val_2, ns);
63+
64+
env.assign(first_val, first_eval_rhs, ns);
65+
env.assign(second_val, second_eval_rhs, ns);
66+
67+
abstract_environmentt second_env;
68+
second_env.assign(first_val, first_eval_rhs, ns);
69+
second_env.assign(second_val, second_eval_rhs, ns);
70+
71+
THEN("The modified symbols between the two domains should be none") {
72+
auto changed_vals = abstract_environmentt::modified_symbols(
73+
env, second_env);
74+
REQUIRE(changed_vals.size() == 0);
7575
}
7676
}
77-
GIVEN("Two identifiers that contain integer values")
77+
}
78+
GIVEN("Two identifiers that contain integer values")
79+
{
80+
const irep_idt identifier = "hello";
81+
auto first_val = symbol_exprt(identifier, integer_typet());
82+
symbolt first_sym;
83+
first_sym.name = first_val.get_identifier();
84+
85+
auto rhs_val = from_integer(5, integer_typet());
86+
87+
const irep_idt second_identifier = "world";
88+
auto second_val = symbol_exprt(second_identifier, integer_typet());
89+
symbolt second_sym;
90+
second_sym.name = second_val.get_identifier();
91+
92+
symbol_tablet symbol_table;
93+
94+
symbol_table.add(first_sym);
95+
symbol_table.add(second_sym);
96+
namespacet ns(symbol_table);
97+
98+
WHEN("The identifiers get inserted into two environments, but one of \
99+
them has a different value in one of the environments")
78100
{
79-
const irep_idt identifier = "hello";
80-
auto first_val = symbol_exprt(identifier, integer_typet());
81-
symbolt first_sym;
82-
first_sym.name = first_val.get_identifier();
83-
84-
auto rhs_val = constant_exprt::integer_constant(5);
85-
86-
const irep_idt second_identifier = "world";
87-
auto second_val = symbol_exprt(second_identifier, integer_typet());
88-
symbolt second_sym;
89-
second_sym.name = second_val.get_identifier();
90-
91-
symbol_tablet symbol_table;
92-
93-
symbol_table.add(first_sym);
94-
symbol_table.add(second_sym);
95-
namespacet ns(symbol_table);
96-
97-
WHEN("The identifiers get inserted into two environments, but one of \
98-
them has a different value in one of the environments")
99-
{
100-
abstract_environmentt env;
101-
102-
auto first_eval_rhs = env.eval(rhs_val, ns);
103-
auto first_eval_res = env.eval(first_val, ns);
104-
105-
auto second_eval_res = env.eval(second_val, ns);
106-
auto rhs_val_2 = constant_exprt::integer_constant(10);
107-
auto second_eval_rhs = env.eval(rhs_val_2, ns);
108-
109-
env.assign(first_val, first_eval_rhs, ns);
110-
env.assign(second_val, second_eval_rhs, ns);
111-
112-
auto rhs_val_3 = constant_exprt::integer_constant(20);
113-
114-
abstract_environmentt second_env;
115-
auto new_rhs_val = second_env.eval(rhs_val_3, ns);
116-
second_env.assign(first_val, first_eval_rhs, ns);
117-
second_env.assign(second_val, new_rhs_val, ns);
118-
119-
THEN("The modified symbols between the two domains should be none") {
120-
auto changed_vals = abstract_environmentt::modified_symbols(
121-
env, second_env);
122-
REQUIRE(changed_vals.size() == 0);
123-
}
101+
abstract_environmentt env;
102+
103+
auto first_eval_rhs = env.eval(rhs_val, ns);
104+
auto first_eval_res = env.eval(first_val, ns);
105+
106+
auto second_eval_res = env.eval(second_val, ns);
107+
auto rhs_val_2 = from_integer(10, integer_typet());
108+
auto second_eval_rhs = env.eval(rhs_val_2, ns);
109+
110+
env.assign(first_val, first_eval_rhs, ns);
111+
env.assign(second_val, second_eval_rhs, ns);
112+
113+
auto rhs_val_3 = from_integer(20, integer_typet());
114+
115+
abstract_environmentt second_env;
116+
auto new_rhs_val = second_env.eval(rhs_val_3, ns);
117+
second_env.assign(first_val, first_eval_rhs, ns);
118+
second_env.assign(second_val, new_rhs_val, ns);
119+
120+
THEN("The modified symbols between the two domains should be none") {
121+
auto changed_vals = abstract_environmentt::modified_symbols(
122+
env, second_env);
123+
REQUIRE(changed_vals.size() == 0);
124124
}
125125
}
126+
}
126127
}

‎unit/analyses/variable-sensitivity/write_stack.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
/// \file
1010
/// Unit tests for construction of write stack
1111

12-
#include "catch.hpp"
12+
#include <testing-utils/catch.hpp>
1313

1414
#include <stack>
1515
#include <iostream>

0 commit comments

Comments
 (0)