Skip to content

Commit 0099f74

Browse files
Daniel Kroeningtautschnig
Daniel Kroening
authored and
tautschnig
committed
remove unused member_exprt::symbol()
Reverts d47d503; the root operand of a member_exprt need not be a symbol_exprt. (It could be a struct_exprt, a dereference_exprt, and possibly something else.)
1 parent 425c2db commit 0099f74

File tree

6 files changed

+159
-84
lines changed

6 files changed

+159
-84
lines changed

‎jbmc/unit/java-testing-utils/require_goto_statements.cpp

Lines changed: 19 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -59,14 +59,16 @@ require_goto_statements::require_entry_point_statements(
5959
/// \param structure_name: The name of variable of type struct
6060
/// \param superclass_name: The name of the superclass (if given)
6161
/// \param component_name: The name of the component of the superclass that
62+
/// \param symbol_table: A symbol table to enable type lookups
6263
/// should be assigned
6364
/// \return: All the assignments to that component.
6465
require_goto_statements::pointer_assignment_locationt
6566
require_goto_statements::find_struct_component_assignments(
6667
const std::vector<codet> &statements,
6768
const irep_idt &structure_name,
6869
const optionalt<irep_idt> &superclass_name,
69-
const irep_idt &component_name)
70+
const irep_idt &component_name,
71+
const symbol_tablet &symbol_table)
7072
{
7173
pointer_assignment_locationt locations;
7274

@@ -97,9 +99,13 @@ require_goto_statements::find_struct_component_assignments(
9799
const irep_idt supercomponent_name =
98100
"@" + id2string(superclass_name.value());
99101

102+
object_descriptor_exprt ode;
103+
const namespacet ns(symbol_table);
104+
ode.build(superclass_expr, ns);
100105
if(
101106
superclass_expr.get_component_name() == supercomponent_name &&
102-
superclass_expr.symbol().get_identifier() == structure_name)
107+
to_symbol_expr(ode.root_object()).get_identifier() ==
108+
structure_name)
103109
{
104110
if(
105111
code_assign.rhs() ==
@@ -122,7 +128,7 @@ require_goto_statements::find_struct_component_assignments(
122128
// - operand (component of): symbol for \p structure_name
123129
if(
124130
member_expr.op().id() == ID_symbol &&
125-
member_expr.symbol().get_identifier() == structure_name &&
131+
to_symbol_expr(member_expr.op()).get_identifier() == structure_name &&
126132
member_expr.get_component_name() == component_name)
127133
{
128134
if(
@@ -291,14 +297,16 @@ const code_declt &require_goto_statements::require_declaration_of_name(
291297
/// \param typecast_name The name of the type to which the object is cast (if
292298
/// there is a typecast)
293299
/// \param entry_point_instructions The statements to look through
300+
/// \param symbol_table: A symbol table to enable type lookups
294301
/// \return The identifier of the variable assigned to the field
295302
const irep_idt &require_goto_statements::require_struct_component_assignment(
296303
const irep_idt &structure_name,
297304
const optionalt<irep_idt> &superclass_name,
298305
const irep_idt &component_name,
299306
const irep_idt &component_type_name,
300307
const optionalt<irep_idt> &typecast_name,
301-
const std::vector<codet> &entry_point_instructions)
308+
const std::vector<codet> &entry_point_instructions,
309+
const symbol_tablet &symbol_table)
302310
{
303311
// First we need to find the assignments to the component belonging to
304312
// the structure_name object
@@ -307,7 +315,8 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
307315
entry_point_instructions,
308316
structure_name,
309317
superclass_name,
310-
component_name);
318+
component_name,
319+
symbol_table);
311320
REQUIRE(component_assignments.non_null_assignments.size() == 1);
312321

313322
// We are expecting that the resulting statement can be of two forms:
@@ -376,6 +385,7 @@ const irep_idt &require_goto_statements::require_struct_component_assignment(
376385
/// \param array_type_name The type of the array, e.g., java::array[reference]
377386
/// \param array_component_element_type_name The element type of the array
378387
/// \param entry_point_instructions The statements to look through
388+
/// \param symbol_table: A symbol table to enable type lookups
379389
/// \return The identifier of the variable assigned to the field
380390
const irep_idt &
381391
require_goto_statements::require_struct_array_component_assignment(
@@ -384,7 +394,8 @@ require_goto_statements::require_struct_array_component_assignment(
384394
const irep_idt &array_component_name,
385395
const irep_idt &array_type_name,
386396
const irep_idt &array_component_element_type_name,
387-
const std::vector<codet> &entry_point_instructions)
397+
const std::vector<codet> &entry_point_instructions,
398+
const symbol_tablet &symbol_table)
388399
{
389400
// First we need to find the assignments to the component belonging to
390401
// the structure_name object
@@ -393,7 +404,8 @@ require_goto_statements::require_struct_array_component_assignment(
393404
entry_point_instructions,
394405
structure_name,
395406
superclass_name,
396-
array_component_name);
407+
array_component_name,
408+
symbol_table);
397409
REQUIRE(component_assignments.non_null_assignments.size() == 1);
398410

399411
// We are expecting that the resulting statement is of form:

‎jbmc/unit/java-testing-utils/require_goto_statements.h

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,8 @@ pointer_assignment_locationt find_struct_component_assignments(
5353
const std::vector<codet> &statements,
5454
const irep_idt &structure_name,
5555
const optionalt<irep_idt> &superclass_name,
56-
const irep_idt &component_name);
56+
const irep_idt &component_name,
57+
const symbol_tablet &symbol_table);
5758

5859
pointer_assignment_locationt find_this_component_assignment(
5960
const std::vector<codet> &statements,
@@ -82,15 +83,17 @@ const irep_idt &require_struct_component_assignment(
8283
const irep_idt &component_name,
8384
const irep_idt &component_type_name,
8485
const optionalt<irep_idt> &typecast_name,
85-
const std::vector<codet> &entry_point_instructions);
86+
const std::vector<codet> &entry_point_instructions,
87+
const symbol_tablet &symbol_table);
8688

8789
const irep_idt &require_struct_array_component_assignment(
8890
const irep_idt &structure_name,
8991
const optionalt<irep_idt> &superclass_name,
9092
const irep_idt &array_component_name,
9193
const irep_idt &array_type_name,
9294
const irep_idt &array_component_element_type_name,
93-
const std::vector<codet> &entry_point_instructions);
95+
const std::vector<codet> &entry_point_instructions,
96+
const symbol_tablet &symbol_table);
9497

9598
const irep_idt &require_entry_point_argument_assignment(
9699
const irep_idt &argument_name,

‎jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp

Lines changed: 46 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,8 @@ SCENARIO(
5858
"field",
5959
"java::java.lang.Integer",
6060
{"java::java.lang.Object"},
61-
entry_point_code);
61+
entry_point_code,
62+
symbol_table);
6263
}
6364
}
6465
}
@@ -90,7 +91,8 @@ SCENARIO(
9091
"field",
9192
"java::IWrapper",
9293
{"java::java.lang.Object"},
93-
entry_point_code);
94+
entry_point_code,
95+
symbol_table);
9496
}
9597
}
9698
}
@@ -122,7 +124,8 @@ SCENARIO(
122124
"field",
123125
"java::Wrapper",
124126
{"java::java.lang.Object"},
125-
entry_point_code);
127+
entry_point_code,
128+
symbol_table);
126129

127130
THEN("Object 'this.field' has correctly specialized field")
128131
{
@@ -132,7 +135,8 @@ SCENARIO(
132135
"field",
133136
"java::IWrapper",
134137
{},
135-
entry_point_code);
138+
entry_point_code,
139+
symbol_table);
136140
}
137141
}
138142
}
@@ -167,7 +171,8 @@ SCENARIO(
167171
"f",
168172
"java::SuperclassUninst",
169173
{},
170-
entry_point_code);
174+
entry_point_code,
175+
symbol_table);
171176

172177
THEN("The object for 'f' has correctly specialized inherited field")
173178
{
@@ -177,7 +182,8 @@ SCENARIO(
177182
"field",
178183
"java::java.lang.Integer",
179184
{"java::java.lang.Object"},
180-
entry_point_code);
185+
entry_point_code,
186+
symbol_table);
181187
}
182188
}
183189
}
@@ -210,7 +216,8 @@ SCENARIO(
210216
"f",
211217
"java::SuperclassMixed",
212218
{},
213-
entry_point_code);
219+
entry_point_code,
220+
symbol_table);
214221

215222
THEN("The object for 'f' has correctly specialized inherited fields")
216223
{
@@ -220,15 +227,17 @@ SCENARIO(
220227
"first",
221228
"java::java.lang.Boolean",
222229
{"java::java.lang.Object"},
223-
entry_point_code);
230+
entry_point_code,
231+
symbol_table);
224232

225233
require_goto_statements::require_struct_component_assignment(
226234
f_tmp_name,
227235
{"PairWrapper"},
228236
"second",
229237
"java::IWrapper",
230238
{"java::java.lang.Object"},
231-
entry_point_code);
239+
entry_point_code,
240+
symbol_table);
232241
}
233242
}
234243
}
@@ -265,7 +274,8 @@ SCENARIO(
265274
"inner",
266275
"java::SuperclassInnerInst$Inner",
267276
{},
268-
entry_point_code);
277+
entry_point_code,
278+
symbol_table);
269279
THEN(
270280
"The object of 'inner' has correctly specialized inherited "
271281
"field")
@@ -276,7 +286,8 @@ SCENARIO(
276286
"field",
277287
"java::java.lang.Integer",
278288
{},
279-
entry_point_code);
289+
entry_point_code,
290+
symbol_table);
280291
}
281292

282293
const irep_idt &inner_gen_tmp_name =
@@ -286,7 +297,8 @@ SCENARIO(
286297
"inner_gen",
287298
"java::SuperclassInnerInst$InnerGen",
288299
{},
289-
entry_point_code);
300+
entry_point_code,
301+
symbol_table);
290302
THEN(
291303
"The object of 'inner_gen' has correctly specialized inherited "
292304
"field")
@@ -297,7 +309,8 @@ SCENARIO(
297309
"field",
298310
"java::java.lang.Boolean",
299311
{"java::java.lang.Object"},
300-
entry_point_code);
312+
entry_point_code,
313+
symbol_table);
301314
}
302315
}
303316
}
@@ -334,7 +347,8 @@ SCENARIO(
334347
"f",
335348
"java::SuperclassInnerUninst",
336349
{},
337-
entry_point_code);
350+
entry_point_code,
351+
symbol_table);
338352

339353
THEN(
340354
"The object for 'f' has fields 'inner' and 'inner_gen' "
@@ -347,7 +361,8 @@ SCENARIO(
347361
"inner",
348362
"java::SuperclassInnerUninst$Inner",
349363
{},
350-
entry_point_code);
364+
entry_point_code,
365+
symbol_table);
351366
THEN(
352367
"The object of 'inner' has correctly specialized inherited "
353368
"field")
@@ -358,7 +373,8 @@ SCENARIO(
358373
"field",
359374
"java::IWrapper",
360375
{"java::java.lang.Object"},
361-
entry_point_code);
376+
entry_point_code,
377+
symbol_table);
362378
}
363379

364380
const irep_idt &inner_gen_tmp_name =
@@ -368,7 +384,8 @@ SCENARIO(
368384
"inner_gen",
369385
"java::SuperclassInnerUninst$InnerGen",
370386
{},
371-
entry_point_code);
387+
entry_point_code,
388+
symbol_table);
372389
THEN(
373390
"The object of 'inner_gen' has correctly specialized inherited "
374391
"fields")
@@ -379,14 +396,16 @@ SCENARIO(
379396
"first",
380397
"java::IWrapper",
381398
{"java::java.lang.Object"},
382-
entry_point_code);
399+
entry_point_code,
400+
symbol_table);
383401
require_goto_statements::require_struct_component_assignment(
384402
inner_gen_tmp_name,
385403
{"PairWrapper"},
386404
"second",
387405
"java::java.lang.Boolean",
388406
{"java::java.lang.Object"},
389-
entry_point_code);
407+
entry_point_code,
408+
symbol_table);
390409
}
391410

392411
const irep_idt &inner_three_tmp_name =
@@ -396,7 +415,8 @@ SCENARIO(
396415
"inner_three",
397416
"java::SuperclassInnerUninst$InnerThree",
398417
{},
399-
entry_point_code);
418+
entry_point_code,
419+
symbol_table);
400420
THEN(
401421
"The object of 'inner_three' has correctly specialized "
402422
"inherited fields")
@@ -407,7 +427,8 @@ SCENARIO(
407427
"field",
408428
"java::IWrapper",
409429
{"java::java.lang.Object"},
410-
entry_point_code);
430+
entry_point_code,
431+
symbol_table);
411432
}
412433
}
413434
}
@@ -463,7 +484,8 @@ SCENARIO(
463484
"field",
464485
"java::java.lang.Object",
465486
{},
466-
entry_point_code);
487+
entry_point_code,
488+
symbol_table);
467489
}
468490
}
469491
}
@@ -506,7 +528,8 @@ SCENARIO(
506528
"field",
507529
"java::java.lang.Object",
508530
{},
509-
entry_point_code);
531+
entry_point_code,
532+
symbol_table);
510533
}
511534
}
512535
}

0 commit comments

Comments
 (0)