Skip to content

Commit 59693f6

Browse files
committed
Unit tests: use new symbolt constructors
To the extent possible, apply resource-acquisition-is-initialisation. The constructors ensure that at least the most essential fields (name, type, mode) are set.
1 parent 0e61c89 commit 59693f6

23 files changed

+84
-228
lines changed

unit/analyses/ai/ai.cpp

Lines changed: 10 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -146,28 +146,16 @@ SCENARIO(
146146

147147
// g:
148148

149-
symbolt gy;
150-
gy.name = "gy";
151-
gy.mode = ID_C;
152-
gy.type = signed_int_type();
153-
154-
symbolt g;
155-
g.name = "g";
156-
g.mode = ID_C;
157-
g.type = code_typet({}, empty_typet());
149+
symbolt gy{"gy", signed_int_type(), ID_C};
150+
151+
symbolt g{"g", code_typet({}, empty_typet()), ID_C};
158152
g.value = code_assignt(gy.symbol_expr(), from_integer(0, signed_int_type()));
159153

160154
// h:
161155

162-
symbolt hy;
163-
hy.name = "hy";
164-
hy.mode = ID_C;
165-
hy.type = signed_int_type();
156+
symbolt hy{"hy", signed_int_type(), ID_C};
166157

167-
symbolt h;
168-
h.name = "h";
169-
h.mode = ID_C;
170-
h.type = code_typet({}, empty_typet());
158+
symbolt h{"h", code_typet({}, empty_typet()), ID_C};
171159
h.value = code_assignt(hy.symbol_expr(), from_integer(0, signed_int_type()));
172160

173161
goto_model.symbol_table.add(g);
@@ -177,15 +165,9 @@ SCENARIO(
177165

178166
// f:
179167

180-
symbolt x;
181-
x.name = "x";
182-
x.mode = ID_C;
183-
x.type = signed_int_type();
168+
symbolt x{"x", signed_int_type(), ID_C};
184169

185-
symbolt y;
186-
y.name = "y";
187-
y.mode = ID_C;
188-
y.type = signed_int_type();
170+
symbolt y{"y", signed_int_type(), ID_C};
189171

190172
goto_model.symbol_table.add(x);
191173
goto_model.symbol_table.add(y);
@@ -221,21 +203,16 @@ SCENARIO(
221203

222204
f_body.copy_to_operands(make_void_call(g.symbol_expr()));
223205

224-
symbolt f;
225-
f.name = "f";
226-
f.mode = ID_C;
227-
f.type = code_typet({}, empty_typet());
206+
symbolt f{"f", code_typet({}, empty_typet()), ID_C};
228207
f.value = f_body;
229208

230209
goto_model.symbol_table.add(f);
231210

232211
// __CPROVER_start:
233212

234-
symbolt start;
235-
start.name = goto_functionst::entry_point();
213+
symbolt start{
214+
goto_functionst::entry_point(), code_typet{{}, empty_typet{}}, ID_C};
236215
start.base_name = goto_functionst::entry_point();
237-
start.mode = ID_C;
238-
start.type = code_typet({}, empty_typet());
239216
start.value = make_void_call(f.symbol_expr());
240217

241218
goto_model.symbol_table.add(start);

unit/analyses/constant_propagator.cpp

Lines changed: 10 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -36,14 +36,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
3636
// int x = 1;
3737
// int y = 2;
3838

39-
symbolt local_x;
40-
symbolt local_y;
41-
local_x.name = "x";
42-
local_x.type = integer_typet();
43-
local_x.mode = ID_C;
44-
local_y.name = "y";
45-
local_y.type = integer_typet();
46-
local_y.mode = ID_C;
39+
symbolt local_x{"x", integer_typet(), ID_C};
40+
symbolt local_y{"y", integer_typet(), ID_C};
4741

4842
code_blockt code(
4943
{code_declt(local_x.symbol_expr()),
@@ -53,11 +47,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
5347
code_assignt(
5448
local_y.symbol_expr(), constant_exprt("2", integer_typet()))});
5549

56-
symbolt main_function_symbol;
57-
main_function_symbol.name = "main";
58-
main_function_symbol.type = code_typet({}, empty_typet());
50+
symbolt main_function_symbol{"main", code_typet({}, empty_typet()), ID_C};
5951
main_function_symbol.value = code;
60-
main_function_symbol.mode = ID_C;
6152

6253
goto_model.symbol_table.add(local_x);
6354
goto_model.symbol_table.add(local_y);
@@ -120,14 +111,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
120111
goto_modelt goto_model;
121112
namespacet ns(goto_model.symbol_table);
122113

123-
symbolt bool_local;
124-
symbolt c_bool_local;
125-
bool_local.name = "bool_local";
126-
bool_local.type = bool_typet();
127-
bool_local.mode = ID_C;
128-
c_bool_local.name = "c_bool_local";
129-
c_bool_local.type = c_bool_typet(8);
130-
c_bool_local.mode = ID_C;
114+
symbolt bool_local{"bool_local", bool_typet(), ID_C};
115+
symbolt c_bool_local{"c_bool_local", c_bool_typet(8), ID_C};
131116

132117
code_blockt code({code_declt(bool_local.symbol_expr()),
133118
code_declt(c_bool_local.symbol_expr())});
@@ -144,11 +129,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
144129
code.add(std::move(bool_cond_block));
145130
code.add(std::move(c_bool_cond_block));
146131

147-
symbolt main_function_symbol;
148-
main_function_symbol.name = "main";
149-
main_function_symbol.type = code_typet({}, empty_typet());
132+
symbolt main_function_symbol{"main", code_typet({}, empty_typet()), ID_C};
150133
main_function_symbol.value = code;
151-
main_function_symbol.mode = ID_C;
152134

153135
goto_model.symbol_table.add(bool_local);
154136
goto_model.symbol_table.add(c_bool_local);
@@ -216,19 +198,13 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
216198

217199
for(size_t i = 0; i < n_bool_locals; ++i)
218200
{
219-
symbolt bool_local;
220-
bool_local.name = "b" + std::to_string(i);
221-
bool_local.type = bool_typet();
222-
bool_local.mode = ID_C;
201+
symbolt bool_local{"b" + std::to_string(i), bool_typet(), ID_C};
223202
bool_locals.push_back(bool_local);
224203
}
225204

226205
for(size_t i = 0; i < n_c_bool_locals; ++i)
227206
{
228-
symbolt c_bool_local;
229-
c_bool_local.name = "cb" + std::to_string(i);
230-
c_bool_local.type = c_bool_typet(8);
231-
c_bool_local.mode = ID_C;
207+
symbolt c_bool_local{"cb" + std::to_string(i), c_bool_typet(8), ID_C};
232208
c_bool_locals.push_back(c_bool_local);
233209
}
234210

@@ -272,10 +248,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
272248
const bool c_bool_expectations[n_c_bool_locals] = {
273249
true, true, true, false, false, true, false, true};
274250

275-
symbolt marker_symbol;
276-
marker_symbol.type = signedbv_typet(32);
277-
marker_symbol.name = "marker";
278-
marker_symbol.mode = ID_C;
251+
symbolt marker_symbol{"marker", signedbv_typet(32), ID_C};
279252

280253
codet program = code_assignt(
281254
marker_symbol.symbol_expr(), from_integer(1234, marker_symbol.type));
@@ -294,11 +267,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]")
294267
for(const symbolt &symbol : c_bool_locals)
295268
goto_model.symbol_table.add(symbol);
296269

297-
symbolt main_function_symbol;
298-
main_function_symbol.name = "main";
299-
main_function_symbol.type = code_typet({}, empty_typet());
270+
symbolt main_function_symbol{"main", code_typet({}, empty_typet()), ID_C};
300271
main_function_symbol.value = program;
301-
main_function_symbol.mode = ID_C;
302272

303273
goto_model.symbol_table.add(marker_symbol);
304274
goto_model.symbol_table.add(main_function_symbol);

unit/analyses/dependence_graph.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -53,10 +53,9 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]")
5353

5454
typet int_type = signed_int_type();
5555

56-
symbolt x_symbol;
57-
x_symbol.name = id2string(goto_functionst::entry_point()) + "::x";
56+
symbolt x_symbol{
57+
id2string(goto_functionst::entry_point()) + "::x", int_type, ID_C};
5858
x_symbol.base_name = "x";
59-
x_symbol.type = int_type;
6059
x_symbol.is_lvalue = true;
6160
x_symbol.is_state_var = true;
6261
x_symbol.is_thread_local = true;

unit/analyses/variable-sensitivity/eval.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,8 @@
1414

1515
static symbolt simple_symbol(const irep_idt &identifier, const typet &type)
1616
{
17-
symbolt b1;
18-
b1.name = b1.base_name = b1.pretty_name = identifier;
19-
b1.type = type;
17+
symbolt b1{identifier, type, irep_idt{}};
18+
b1.base_name = b1.pretty_name = identifier;
2019
return b1;
2120
}
2221

unit/goto-programs/goto_program_assume.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -23,21 +23,18 @@ SCENARIO(
2323
{
2424
symbol_tablet symbol_table;
2525
const typet type1 = signedbv_typet(32);
26-
symbolt symbol;
27-
symbolt fun_symbol;
26+
symbolt symbol{"a", type1, ID_C};
2827
irep_idt fun_name = "foo";
28+
symbolt fun_symbol;
2929
fun_symbol.name = fun_name;
30-
irep_idt symbol_name = "a";
31-
symbol.name = symbol_name;
32-
symbol_exprt varx(symbol_name, type1);
30+
symbol_exprt varx = symbol.symbol_expr();
3331
exprt val10 = from_integer(10, type1);
3432
binary_relation_exprt x_le_10(varx, ID_le, val10);
3533

3634
goto_functiont goto_function;
3735
auto assertion =
3836
goto_function.body.add(goto_programt::make_assertion(x_le_10));
3937

40-
symbol.type = type1;
4138
symbol_table.insert(symbol);
4239
symbol_table.insert(fun_symbol);
4340
namespacet ns(symbol_table);

unit/goto-programs/goto_program_dead.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,11 +27,8 @@ SCENARIO(
2727
irep_idt fun_name = "foo";
2828
fun_symbol.name = fun_name;
2929

30-
symbolt var_symbol;
31-
irep_idt var_symbol_name = "a";
32-
var_symbol.type = type1;
33-
var_symbol.name = var_symbol_name;
34-
symbol_exprt var_a(var_symbol_name, type1);
30+
symbolt var_symbol{"a", type1, irep_idt{}};
31+
symbol_exprt var_a = var_symbol.symbol_expr();
3532

3633
goto_functiont goto_function;
3734
auto &instructions = goto_function.body.instructions;

unit/goto-programs/goto_program_declaration.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,11 +27,8 @@ SCENARIO(
2727
irep_idt fun_name = "foo";
2828
fun_symbol.name = fun_name;
2929

30-
symbolt var_symbol;
31-
irep_idt var_symbol_name = "a";
32-
var_symbol.type = type1;
33-
var_symbol.name = var_symbol_name;
34-
symbol_exprt var_a(var_symbol_name, type1);
30+
symbolt var_symbol{"a", type1, irep_idt{}};
31+
symbol_exprt var_a = var_symbol.symbol_expr();
3532

3633
goto_functiont goto_function;
3734
goto_function.body.add(goto_programt::make_decl(var_a));

unit/goto-programs/goto_program_function_call.cpp

Lines changed: 8 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -25,28 +25,19 @@ SCENARIO(
2525
const signedbv_typet type2(64);
2626
const code_typet code_type({}, type1);
2727

28-
symbolt var_symbol;
29-
irep_idt var_symbol_name = "a";
30-
var_symbol.name = var_symbol_name;
31-
symbol_exprt var_a(var_symbol_name, type1);
32-
33-
symbolt var_symbol2;
34-
irep_idt var_symbol_name2 = "b";
35-
var_symbol2.name = var_symbol_name2;
36-
symbol_exprt var_b(var_symbol_name2, type2);
37-
38-
symbolt fun_symbol;
39-
irep_idt fun_symbol_name = "foo";
40-
fun_symbol.name = fun_symbol_name;
41-
fun_symbol.type = code_type;
42-
symbol_exprt fun_foo(fun_symbol_name, code_type);
28+
symbolt var_symbol{"a", type1, irep_idt{}};
29+
symbol_exprt var_a = var_symbol.symbol_expr();
30+
31+
symbolt var_symbol2{"b", type2, irep_idt{}};
32+
symbol_exprt var_b = var_symbol2.symbol_expr();
33+
34+
symbolt fun_symbol{"foo", code_type, irep_idt{}};
35+
symbol_exprt fun_foo = fun_symbol.symbol_expr();
4336

4437
goto_functiont goto_function;
4538
auto &instructions = goto_function.body.instructions;
4639
instructions.emplace_back(goto_program_instruction_typet::FUNCTION_CALL);
4740

48-
var_symbol.type = type1;
49-
var_symbol2.type = type2;
5041
symbol_table.insert(var_symbol);
5142
symbol_table.insert(var_symbol2);
5243
symbol_table.insert(fun_symbol);

unit/goto-programs/goto_program_goto_target.cpp

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -27,10 +27,8 @@ SCENARIO(
2727
irep_idt fun_name = "foo";
2828
fun_symbol.name = fun_name;
2929

30-
symbolt symbol;
31-
irep_idt symbol_name = "a";
32-
symbol.name = symbol_name;
33-
symbol_exprt varx(symbol_name, type1);
30+
symbolt symbol{"a", type1, irep_idt{}};
31+
symbol_exprt varx = symbol.symbol_expr();
3432
exprt val10 = from_integer(10, type1);
3533
binary_relation_exprt x_le_10(varx, ID_le, val10);
3634

@@ -41,7 +39,6 @@ SCENARIO(
4139
instructions.emplace_back(
4240
goto_programt::make_goto(instructions.begin(), true_exprt()));
4341

44-
symbol.type = type1;
4542
symbol_table.insert(symbol);
4643
symbol_table.insert(fun_symbol);
4744
namespacet ns(symbol_table);

unit/goto-programs/goto_program_validate.cpp

Lines changed: 10 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -28,60 +28,38 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
2828
goto_modelt goto_model;
2929

3030
// void f(){int x = 1;}
31-
symbolt x;
32-
x.name = "x";
33-
x.mode = ID_C;
34-
x.type = signed_int_type();
31+
symbolt x{"x", signed_int_type(), ID_C};
3532
goto_model.symbol_table.add(x);
3633

37-
symbolt f;
38-
f.name = "f";
39-
f.mode = ID_C;
40-
f.type = code_typet({}, empty_typet()); // void rtn, take no params
34+
// void rtn, take no params
35+
symbolt f{"f", code_typet({}, empty_typet()), ID_C};
4136
code_blockt f_body{
4237
{code_declt(x.symbol_expr()),
4338
code_assignt(x.symbol_expr(), from_integer(1, signed_int_type()))}};
44-
4539
f.value = f_body;
4640
goto_model.symbol_table.add(f);
4741

4842
// void g(){int y = 2;}
49-
symbolt y;
50-
y.name = "y";
51-
y.mode = ID_C;
52-
y.type = signed_int_type();
43+
symbolt y{"y", signed_int_type(), ID_C};
5344
goto_model.symbol_table.add(y);
5445

55-
symbolt g;
56-
g.name = "g";
57-
g.mode = ID_C;
58-
g.type = code_typet({}, empty_typet());
59-
46+
symbolt g{"g", code_typet({}, empty_typet()), ID_C};
6047
code_blockt g_body{
6148
{code_declt{y.symbol_expr()},
6249
code_assignt{y.symbol_expr(), from_integer(2, signed_int_type())}}};
63-
6450
g.value = g_body;
6551
goto_model.symbol_table.add(g);
6652

67-
symbolt z;
68-
z.name = "z";
69-
z.mode = ID_C;
70-
z.type = signed_int_type();
53+
symbolt z{"z", signed_int_type(), ID_C};
7154
goto_model.symbol_table.add(z);
7255

73-
symbolt fn_ptr;
74-
fn_ptr.name = "fn_ptr";
75-
fn_ptr.mode = ID_C;
76-
7756
// pointer to fn call
78-
fn_ptr.type = pointer_typet(code_typet{{}, empty_typet()}, 64);
57+
symbolt fn_ptr{
58+
"fn_ptr", pointer_typet(code_typet{{}, empty_typet()}, 64), ID_C};
7959
goto_model.symbol_table.add(fn_ptr);
8060

81-
symbolt entry_point;
82-
entry_point.name = goto_functionst::entry_point();
83-
entry_point.mode = ID_C;
84-
entry_point.type = code_typet({}, empty_typet{});
61+
symbolt entry_point{
62+
goto_functionst::entry_point(), code_typet({}, empty_typet{}), ID_C};
8563
code_blockt entry_point_body{
8664
{code_declt{z.symbol_expr()},
8765
code_assignt{z.symbol_expr(), from_integer(3, signed_int_type())},

0 commit comments

Comments
 (0)