Skip to content

Commit 4866453

Browse files
smowtonsmowton
committed
Generic tests: check for matching tag, not completely matching type
Previously these relied on base_type_eq to hide differently-decorated tags; now they explicitly just check the tag name, rather than relying on base_type_eq, which will soon go away anyway, to hide generic qualifiers and/or array element types.
1 parent e3ff246 commit 4866453

10 files changed

+203
-244
lines changed

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -461,6 +461,14 @@ require_type::require_struct_tag(const typet &type, const irep_idt &identifier)
461461
return result;
462462
}
463463

464+
const pointer_typet
465+
require_type::require_pointer_to_tag(const typet &type, const irep_idt &tag)
466+
{
467+
const auto pointer_type = require_type::require_pointer(type, {});
468+
require_type::require_struct_tag(pointer_type.subtype(), tag);
469+
return pointer_type;
470+
}
471+
464472
/// Verify a given type is a java generic symbol type
465473
/// \param type: The type to check
466474
/// \param identifier: The identifier to match

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,10 @@ require_pointer(const typet &type, const optionalt<typet> &subtype);
2828
const struct_tag_typet &
2929
require_struct_tag(const typet &type, const irep_idt &identifier = "");
3030

31+
const pointer_typet
32+
require_pointer_to_tag(
33+
const typet &type, const irep_idt &identifier = irep_idt());
34+
3135
struct_typet::componentt require_component(
3236
const struct_typet &struct_type,
3337
const irep_idt &component_name);

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -91,8 +91,8 @@ SCENARIO(
9191
const struct_union_typet::componentt &belem_type =
9292
require_type::require_component(
9393
to_struct_type(class_symbol.type), "belem");
94-
require_type::require_pointer(
95-
belem_type.type(), struct_tag_typet(class_prefix + "$BoundedInner"));
94+
require_type::require_pointer_to_tag(
95+
belem_type.type(), class_prefix + "$BoundedInner");
9696
require_type::require_java_generic_type(
9797
belem_type.type(),
9898
{{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}});

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp

Lines changed: 13 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,7 @@ SCENARIO(
3939
{
4040
const java_method_typet::parametert &param_x =
4141
require_type::require_parameter(func_code, "x");
42-
require_type::require_pointer(
43-
param_x.type(), struct_tag_typet("java::Generic"));
42+
require_type::require_pointer_to_tag(param_x.type(), "java::Generic");
4443

4544
THEN("x is generic with parameter pointing to java.lang.Integer")
4645
{
@@ -54,8 +53,7 @@ SCENARIO(
5453
THEN("It has return type pointing to Generic")
5554
{
5655
const typet return_type = func_code.return_type();
57-
require_type::require_pointer(
58-
return_type, struct_tag_typet("java::Generic"));
56+
require_type::require_pointer_to_tag(return_type, "java::Generic");
5957

6058
THEN("It is generic with parameter pointing to java.lang.Integer")
6159
{
@@ -88,8 +86,7 @@ SCENARIO(
8886
{
8987
const java_method_typet::parametert &param_s =
9088
require_type::require_parameter(func_code, "s");
91-
require_type::require_pointer(
92-
param_s.type(), struct_tag_typet("java::Generic"));
89+
require_type::require_pointer_to_tag(param_s.type(), "java::Generic");
9390

9491
THEN("s is generic with parameter pointing to java.lang.String")
9592
{
@@ -103,8 +100,7 @@ SCENARIO(
103100
THEN("It has return type pointing to Generic")
104101
{
105102
const typet return_type = func_code.return_type();
106-
require_type::require_pointer(
107-
return_type, struct_tag_typet("java::Generic"));
103+
require_type::require_pointer_to_tag(return_type, "java::Generic");
108104

109105
THEN("It is generic with parameter pointing to java.lang.Integer")
110106
{
@@ -137,8 +133,7 @@ SCENARIO(
137133
{
138134
const java_method_typet::parametert &param_x =
139135
require_type::require_parameter(func_code, "x");
140-
require_type::require_pointer(
141-
param_x.type(), struct_tag_typet("java::Generic"));
136+
require_type::require_pointer_to_tag(param_x.type(), "java::Generic");
142137

143138
THEN("x is generic with parameter pointing to java.lang.Integer")
144139
{
@@ -153,8 +148,7 @@ SCENARIO(
153148
{
154149
const java_method_typet::parametert &param_y =
155150
require_type::require_parameter(func_code, "y");
156-
require_type::require_pointer(
157-
param_y.type(), struct_tag_typet("java::Generic"));
151+
require_type::require_pointer_to_tag(param_y.type(), "java::Generic");
158152

159153
THEN("y is generic with parameter pointing to java.lang.Integer")
160154
{
@@ -168,8 +162,7 @@ SCENARIO(
168162
THEN("It has return type pointing to Generic")
169163
{
170164
const typet return_type = func_code.return_type();
171-
require_type::require_pointer(
172-
return_type, struct_tag_typet("java::Generic"));
165+
require_type::require_pointer_to_tag(return_type, "java::Generic");
173166

174167
THEN("It is generic with parameter pointing to java.lang.Integer")
175168
{
@@ -202,8 +195,7 @@ SCENARIO(
202195
{
203196
const java_method_typet::parametert &param_s =
204197
require_type::require_parameter(func_code, "s");
205-
require_type::require_pointer(
206-
param_s.type(), struct_tag_typet("java::Generic"));
198+
require_type::require_pointer_to_tag(param_s.type(), "java::Generic");
207199

208200
THEN("s is generic with parameter pointing to java.lang.String")
209201
{
@@ -218,8 +210,7 @@ SCENARIO(
218210
{
219211
const java_method_typet::parametert &param_b =
220212
require_type::require_parameter(func_code, "b");
221-
require_type::require_pointer(
222-
param_b.type(), struct_tag_typet("java::Generic"));
213+
require_type::require_pointer_to_tag(param_b.type(), "java::Generic");
223214

224215
THEN("b is generic with parameter pointing to java.lang.Boolean")
225216
{
@@ -233,8 +224,7 @@ SCENARIO(
233224
THEN("It has return type pointing to Generic")
234225
{
235226
const typet return_type = func_code.return_type();
236-
require_type::require_pointer(
237-
return_type, struct_tag_typet("java::Generic"));
227+
require_type::require_pointer_to_tag(return_type, "java::Generic");
238228

239229
THEN("It is generic with parameter pointing to java.lang.Integer")
240230
{
@@ -268,15 +258,14 @@ SCENARIO(
268258
{
269259
const java_method_typet::parametert &param_inner =
270260
require_type::require_parameter(func_code, "inner");
271-
require_type::require_pointer(
272-
param_inner.type(), struct_tag_typet(class_prefix + "$Inner"));
261+
require_type::require_pointer_to_tag(
262+
param_inner.type(), class_prefix + "$Inner");
273263
}
274264

275265
THEN("It has return type pointing to Generic")
276266
{
277267
const typet return_type = func_code.return_type();
278-
require_type::require_pointer(
279-
return_type, struct_tag_typet("java::Generic"));
268+
require_type::require_pointer_to_tag(return_type, "java::Generic");
280269

281270
THEN("It is generic with parameter pointing to java.lang.Integer")
282271
{

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp

Lines changed: 11 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,9 @@ SCENARIO(
3232

3333
THEN("It is an array")
3434
{
35-
const pointer_typet &field_t_pointer = require_type::require_pointer(
36-
field_t.type(), struct_tag_typet("java::array[reference]"));
35+
const pointer_typet &field_t_pointer =
36+
require_type::require_pointer_to_tag(
37+
field_t.type(), "java::array[reference]");
3738

3839
const struct_tag_typet &field_t_subtype =
3940
to_struct_tag_type(field_t_pointer.subtype());
@@ -57,8 +58,9 @@ SCENARIO(
5758

5859
THEN("It is an array")
5960
{
60-
const pointer_typet &field_t2_pointer = require_type::require_pointer(
61-
field_t2.type(), struct_tag_typet("java::array[reference]"));
61+
const pointer_typet &field_t2_pointer =
62+
require_type::require_pointer_to_tag(
63+
field_t2.type(), "java::array[reference]");
6264

6365
const struct_tag_typet &field_t2_subtype =
6466
to_struct_tag_type(field_t2_pointer.subtype());
@@ -69,8 +71,7 @@ SCENARIO(
6971
THEN("The elements have type Generic<T>")
7072
{
7173
const typet &element = java_array_element_type(field_t2_subtype);
72-
require_type::require_pointer(
73-
element, struct_tag_typet("java::Generic"));
74+
require_type::require_pointer_to_tag(element, "java::Generic");
7475
require_type::require_java_generic_type(
7576
element,
7677
{{require_type::type_argument_kindt::Var, class_prefix + "::T"}});
@@ -85,8 +86,9 @@ SCENARIO(
8586

8687
THEN("It is an array")
8788
{
88-
const pointer_typet &field_t3_pointer = require_type::require_pointer(
89-
field_t3.type(), struct_tag_typet("java::array[reference]"));
89+
const pointer_typet &field_t3_pointer =
90+
require_type::require_pointer_to_tag(
91+
field_t3.type(), "java::array[reference]");
9092

9193
const struct_tag_typet &field_t3_subtype =
9294
to_struct_tag_type(field_t3_pointer.subtype());
@@ -97,8 +99,7 @@ SCENARIO(
9799
THEN("The elements have type Generic<Integer>")
98100
{
99101
const typet &element = java_array_element_type(field_t3_subtype);
100-
require_type::require_pointer(
101-
element, struct_tag_typet("java::Generic"));
102+
require_type::require_pointer_to_tag(element, "java::Generic");
102103
require_type::require_java_generic_type(
103104
element,
104105
{{require_type::type_argument_kindt::Inst,

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,7 @@ SCENARIO(
4646
{
4747
const struct_union_typet::componentt &field_g =
4848
require_type::require_component(class_struct, "g");
49-
require_type::require_pointer(
50-
field_g.type(), struct_tag_typet("java::Generic"));
49+
require_type::require_pointer_to_tag(field_g.type(), "java::Generic");
5150

5251
THEN("It is generic with parameter pointing to java.lang.Integer")
5352
{

0 commit comments

Comments
 (0)