Skip to content

Commit 62f1d5a

Browse files
kroeningkroening
authored
Merge pull request #7110 from diffblue/add_subtype
Introduce typet::add_subtype
2 parents 21fa6a0 + 8b7b7a9 commit 62f1d5a

23 files changed

+174
-132
lines changed

‎jbmc/src/java_bytecode/remove_java_new.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -280,7 +280,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
280280
if(!rhs.get_bool(ID_skip_initialize))
281281
{
282282
const auto zero_element =
283-
zero_initializer(data.type().subtype(), location, ns);
283+
zero_initializer(to_pointer_type(data.type()).base_type(), location, ns);
284284
CHECK_RETURN(zero_element.has_value());
285285
codet array_set{ID_array_set, {new_array_data_symbol, *zero_element}};
286286
dest.insert_before(next, goto_programt::make_other(array_set, location));
@@ -316,7 +316,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
316316

317317
plus_exprt(tmp_i, from_integer(1, tmp_i.type()));
318318
dereference_exprt deref_expr(
319-
plus_exprt(data, tmp_i), data.type().subtype());
319+
plus_exprt(data, tmp_i), to_pointer_type(data.type()).base_type());
320320

321321
code_blockt for_body;
322322
symbol_exprt init_sym =

‎src/ansi-c/ansi_c_convert_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -673,7 +673,7 @@ void ansi_c_convert_typet::set_attributes(typet &type) const
673673
if(gcc_attribute_mode.is_not_nil())
674674
{
675675
typet new_type=gcc_attribute_mode;
676-
new_type.subtype()=type;
676+
new_type.add_subtype() = type;
677677
type.swap(new_type);
678678
}
679679

‎src/ansi-c/ansi_c_declaration.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ void ansi_c_declaratort::build(irept &src)
5353
p = &merged_type.last_type();
5454
}
5555
else
56-
p=&t.subtype();
56+
p = &t.add_subtype();
5757
}
5858

5959
type()=static_cast<const typet &>(src);
@@ -103,7 +103,9 @@ typet ansi_c_declarationt::full_type(
103103
if(p->id()==ID_frontend_pointer || p->id()==ID_array ||
104104
p->id()==ID_vector || p->id()==ID_c_bit_field ||
105105
p->id()==ID_block_pointer || p->id()==ID_code)
106-
p=&p->subtype();
106+
{
107+
p = &p->add_subtype();
108+
}
107109
else if(p->id()==ID_merged_type)
108110
{
109111
// we always go down on the right-most subtype

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1364,7 +1364,7 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
13641364
for(const auto &member : enum_members)
13651365
body.push_back(member);
13661366

1367-
enum_tag_symbol.type.subtype()=underlying_type;
1367+
enum_tag_symbol.type.add_subtype() = underlying_type;
13681368

13691369
// is it in the symbol table already?
13701370
symbol_tablet::symbolst::const_iterator s_it=

‎src/ansi-c/parser.y

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1340,7 +1340,7 @@ atomic_specifier:
13401340
{
13411341
$$=$1;
13421342
parser_stack($$).id(ID_atomic_type_specifier);
1343-
stack_type($$).subtype()=stack_type($3);
1343+
stack_type($$).add_subtype()=stack_type($3);
13441344
}
13451345
;
13461346

@@ -1530,7 +1530,7 @@ elaborated_type_name:
15301530

15311531
array_of_construct:
15321532
TOK_ARRAY_OF '<' type_name '>'
1533-
{ $$=$1; stack_type($$).subtype().swap(parser_stack($2)); }
1533+
{ $$=$1; stack_type($$).add_subtype().swap(parser_stack($2)); }
15341534
;
15351535

15361536
pragma_packed:
@@ -1787,7 +1787,7 @@ member_declarator:
17871787
| bit_field_size gcc_type_attribute_opt
17881788
{
17891789
$$=$1;
1790-
stack_type($$).subtype()=typet(ID_abstract);
1790+
stack_type($$).add_subtype()=typet(ID_abstract);
17911791

17921792
if(parser_stack($2).is_not_nil()) // type attribute
17931793
$$=merge($2, $$);
@@ -1807,7 +1807,7 @@ member_identifier_declarator:
18071807
| bit_field_size gcc_type_attribute_opt
18081808
{
18091809
$$=$1;
1810-
stack_type($$).subtype()=typet(ID_abstract);
1810+
stack_type($$).add_subtype()=typet(ID_abstract);
18111811

18121812
if(parser_stack($2).is_not_nil()) // type attribute
18131813
$$=merge($2, $$);
@@ -1828,7 +1828,7 @@ bit_field_size:
18281828
$$=$1;
18291829
set($$, ID_c_bit_field);
18301830
stack_type($$).set(ID_size, parser_stack($2));
1831-
stack_type($$).subtype().id(ID_abstract);
1831+
stack_type($$).add_subtype().id(ID_abstract);
18321832
}
18331833
;
18341834

@@ -3235,7 +3235,7 @@ unary_identifier_declarator:
32353235
// The below is deliberately not using pointer_type();
32363236
// the width is added during conversion.
32373237
stack_type($1).id(ID_frontend_pointer);
3238-
stack_type($1).subtype()=typet(ID_abstract);
3238+
stack_type($1).add_subtype()=typet(ID_abstract);
32393239
$2=merge($2, $1); // dest=$2
32403240
make_subtype($3, $2); // dest=$3
32413241
$$=$3;
@@ -3431,7 +3431,7 @@ postfixing_abstract_declarator:
34313431
{
34323432
$$=$1;
34333433
set($$, ID_code);
3434-
stack_type($$).subtype()=typet(ID_abstract);
3434+
stack_type($$).add_subtype()=typet(ID_abstract);
34353435
stack_type($$).add(ID_parameters);
34363436
stack_type($$).set(ID_C_KnR, true);
34373437
}
@@ -3448,7 +3448,7 @@ postfixing_abstract_declarator:
34483448
{
34493449
$$=$1;
34503450
set($$, ID_code);
3451-
stack_type($$).subtype()=typet(ID_abstract);
3451+
stack_type($$).add_subtype()=typet(ID_abstract);
34523452
stack_type($$).add(ID_parameters).get_sub().
34533453
swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes()));
34543454
PARSER.pop_scope();
@@ -3476,7 +3476,7 @@ parameter_postfixing_abstract_declarator:
34763476
{
34773477
set($1, ID_code);
34783478
stack_type($1).add(ID_parameters);
3479-
stack_type($1).subtype()=typet(ID_abstract);
3479+
stack_type($1).add_subtype()=typet(ID_abstract);
34803480
PARSER.pop_scope();
34813481

34823482
// Clear function name in source location after parsing if
@@ -3506,7 +3506,7 @@ parameter_postfixing_abstract_declarator:
35063506
cprover_function_contract_sequence_opt
35073507
{
35083508
set($1, ID_code);
3509-
stack_type($1).subtype()=typet(ID_abstract);
3509+
stack_type($1).add_subtype()=typet(ID_abstract);
35103510
stack_type($1).add(ID_parameters).get_sub().
35113511
swap((irept::subt &)(to_type_with_subtypes(stack_type($3)).subtypes()));
35123512
PARSER.pop_scope();
@@ -3532,7 +3532,7 @@ array_abstract_declarator:
35323532
{
35333533
$$=$1;
35343534
set($$, ID_array);
3535-
stack_type($$).subtype()=typet(ID_abstract);
3535+
stack_type($$).add_subtype()=typet(ID_abstract);
35363536
stack_type($$).add(ID_size).make_nil();
35373537
}
35383538
| '[' attribute_type_qualifier_storage_class_list ']'
@@ -3541,7 +3541,7 @@ array_abstract_declarator:
35413541
// The type qualifier belongs to the array, not the
35423542
// contents of the array, nor the size.
35433543
set($1, ID_array);
3544-
stack_type($1).subtype()=typet(ID_abstract);
3544+
stack_type($1).add_subtype()=typet(ID_abstract);
35453545
stack_type($1).add(ID_size).make_nil();
35463546
$$=merge($2, $1);
35473547
}
@@ -3550,23 +3550,23 @@ array_abstract_declarator:
35503550
// these should be allowed in prototypes only
35513551
$$=$1;
35523552
set($$, ID_array);
3553-
stack_type($$).subtype()=typet(ID_abstract);
3553+
stack_type($$).add_subtype()=typet(ID_abstract);
35543554
stack_type($$).add(ID_size).make_nil();
35553555
}
35563556
| '[' constant_expression ']'
35573557
{
35583558
$$=$1;
35593559
set($$, ID_array);
35603560
stack_type($$).add(ID_size).swap(parser_stack($2));
3561-
stack_type($$).subtype()=typet(ID_abstract);
3561+
stack_type($$).add_subtype()=typet(ID_abstract);
35623562
}
35633563
| '[' attribute_type_qualifier_storage_class_list constant_expression ']'
35643564
{
35653565
// The type qualifier belongs to the array, not the
35663566
// contents of the array, nor the size.
35673567
set($1, ID_array);
35683568
stack_type($1).add(ID_size).swap(parser_stack($3));
3569-
stack_type($1).subtype()=typet(ID_abstract);
3569+
stack_type($1).add_subtype()=typet(ID_abstract);
35703570
$$=merge($2, $1); // dest=$2
35713571
}
35723572
| array_abstract_declarator '[' constant_expression ']'
@@ -3575,7 +3575,7 @@ array_abstract_declarator:
35753575
$$=$1;
35763576
set($2, ID_array);
35773577
stack_type($2).add(ID_size).swap(parser_stack($3));
3578-
stack_type($2).subtype()=typet(ID_abstract);
3578+
stack_type($2).add_subtype()=typet(ID_abstract);
35793579
make_subtype($1, $2);
35803580
}
35813581
| array_abstract_declarator '[' '*' ']'
@@ -3585,7 +3585,7 @@ array_abstract_declarator:
35853585
$$=$1;
35863586
set($2, ID_array);
35873587
stack_type($2).add(ID_size).make_nil();
3588-
stack_type($2).subtype()=typet(ID_abstract);
3588+
stack_type($2).add_subtype()=typet(ID_abstract);
35893589
make_subtype($1, $2);
35903590
}
35913591
;
@@ -3597,7 +3597,7 @@ unary_abstract_declarator:
35973597
// The below is deliberately not using pointer_type();
35983598
// the width is added during conversion.
35993599
stack_type($$).id(ID_frontend_pointer);
3600-
stack_type($$).subtype()=typet(ID_abstract);
3600+
stack_type($$).add_subtype()=typet(ID_abstract);
36013601
}
36023602
| '*' attribute_type_qualifier_list
36033603
{
@@ -3606,7 +3606,7 @@ unary_abstract_declarator:
36063606
// The below is deliberately not using pointer_type();
36073607
// the width is added during conversion.
36083608
stack_type($1).id(ID_frontend_pointer);
3609-
stack_type($1).subtype()=typet(ID_abstract);
3609+
stack_type($1).add_subtype()=typet(ID_abstract);
36103610
$$=merge($2, $1);
36113611
}
36123612
| '*' abstract_declarator
@@ -3621,7 +3621,7 @@ unary_abstract_declarator:
36213621
// The below is deliberately not using pointer_type();
36223622
// the width is added during conversion.
36233623
stack_type($1).id(ID_frontend_pointer);
3624-
stack_type($1).subtype()=typet(ID_abstract);
3624+
stack_type($1).add_subtype()=typet(ID_abstract);
36253625
$2=merge($2, $1); // dest=$2
36263626
make_subtype($3, $2); // dest=$3
36273627
$$=$3;
@@ -3632,7 +3632,7 @@ unary_abstract_declarator:
36323632
// http://en.wikipedia.org/wiki/Blocks_(C_language_extension)
36333633
$$=$1;
36343634
set($$, ID_block_pointer);
3635-
stack_type($$).subtype()=typet(ID_abstract);
3635+
stack_type($$).add_subtype()=typet(ID_abstract);
36363636
}
36373637
;
36383638

@@ -3643,7 +3643,7 @@ parameter_unary_abstract_declarator:
36433643
// The below is deliberately not using pointer_type();
36443644
// the width is added during conversion.
36453645
stack_type($$).id(ID_frontend_pointer);
3646-
stack_type($$).subtype()=typet(ID_abstract);
3646+
stack_type($$).add_subtype()=typet(ID_abstract);
36473647
}
36483648
| '*' attribute_type_qualifier_list
36493649
{
@@ -3652,7 +3652,7 @@ parameter_unary_abstract_declarator:
36523652
// The below is deliberately not using pointer_type();
36533653
// the width is added during conversion.
36543654
stack_type($1).id(ID_frontend_pointer);
3655-
stack_type($1).subtype()=typet(ID_abstract);
3655+
stack_type($1).add_subtype()=typet(ID_abstract);
36563656
$$=merge($2, $1);
36573657
}
36583658
| '*' parameter_abstract_declarator
@@ -3667,7 +3667,7 @@ parameter_unary_abstract_declarator:
36673667
// The below is deliberately not using pointer_type();
36683668
// the width is added during conversion.
36693669
stack_type($1).id(ID_frontend_pointer);
3670-
stack_type($1).subtype()=typet(ID_abstract);
3670+
stack_type($1).add_subtype()=typet(ID_abstract);
36713671
$2=merge($2, $1); // dest=$2
36723672
make_subtype($3, $2); // dest=$3
36733673
$$=$3;
@@ -3678,7 +3678,7 @@ parameter_unary_abstract_declarator:
36783678
// http://en.wikipedia.org/wiki/Blocks_(C_language_extension)
36793679
$$=$1;
36803680
set($$, ID_block_pointer);
3681-
stack_type($$).subtype()=typet(ID_abstract);
3681+
stack_type($$).add_subtype()=typet(ID_abstract);
36823682
}
36833683
;
36843684

‎src/ansi-c/parser_static.inc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -211,7 +211,7 @@ static void make_subtype(typet &dest, typet &src)
211211
sub->id()==ID_code)
212212
{
213213
// walk down
214-
p=&sub->subtype();
214+
p=&sub->add_subtype();
215215
}
216216
else
217217
{
@@ -250,7 +250,7 @@ static void make_subtype(typet &dest, typet &src)
250250
else if(p->is_nil())
251251
assert(false);
252252
else
253-
p=&p->subtype();
253+
p=&p->add_subtype();
254254
}
255255
break;
256256
}
@@ -292,7 +292,7 @@ static void make_pointer(const YYSTYPE dest)
292292
// The below deliberately avoids pointer_type().
293293
// The width is set during conversion.
294294
stack_type(dest).id(ID_frontend_pointer);
295-
stack_type(dest).subtype()=typet(ID_abstract);
295+
stack_type(dest).add_subtype()=typet(ID_abstract);
296296
}
297297

298298
/*******************************************************************\

‎src/cpp/cpp_convert_type.cpp

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,8 @@ void cpp_convert_typet::read_rec(const typet &type)
8585
else if(type.id()==ID_array)
8686
{
8787
other.push_back(type);
88-
cpp_convert_plain_type(other.back().subtype(), get_message_handler());
88+
cpp_convert_plain_type(
89+
to_array_type(other.back()).element_type(), get_message_handler());
8990
}
9091
else if(type.id()==ID_template)
9192
{
@@ -124,7 +125,8 @@ void cpp_convert_typet::read_template(const typet &type)
124125
other.push_back(type);
125126
typet &t=other.back();
126127

127-
cpp_convert_plain_type(t.subtype(), get_message_handler());
128+
cpp_convert_plain_type(
129+
to_type_with_subtype(t).subtype(), get_message_handler());
128130

129131
irept &arguments=t.add(ID_arguments);
130132

@@ -157,7 +159,7 @@ void cpp_convert_typet::read_function_type(const typet &type)
157159
// change subtype to return_type
158160
typet &return_type = t.return_type();
159161

160-
return_type.swap(t.subtype());
162+
return_type.swap(to_type_with_subtype(t).subtype());
161163
t.remove_subtype();
162164

163165
if(return_type.is_not_nil())
@@ -203,7 +205,7 @@ void cpp_convert_typet::read_function_type(const typet &type)
203205
if(final_type.id()==ID_array)
204206
{
205207
// turn into pointer type
206-
final_type=pointer_type(final_type.subtype());
208+
final_type = pointer_type(to_array_type(final_type).element_type());
207209
}
208210

209211
code_typet::parametert new_parameter(final_type);
@@ -352,7 +354,8 @@ void cpp_convert_auto(
352354
{
353355
if(dest.id() != ID_merged_type && dest.has_subtype())
354356
{
355-
cpp_convert_auto(dest.subtype(), src, message_handler);
357+
cpp_convert_auto(
358+
to_type_with_subtype(dest).subtype(), src, message_handler);
356359
return;
357360
}
358361

‎src/cpp/cpp_declarator.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ typet cpp_declaratort::merge_type(const typet &declaration_type) const
5151
else
5252
{
5353
assert(!t.id().empty());
54-
p=&t.subtype();
54+
p = &t.add_subtype();
5555
}
5656
}
5757

‎src/cpp/cpp_declarator_converter.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ symbolt &cpp_declarator_convertert::convert(
4444
{
4545
typet type;
4646
type.swap(declarator.name().get_sub().back());
47-
declarator.type().subtype()=type;
47+
declarator.type().add_subtype() = type;
4848
cpp_typecheck.typecheck_type(type);
4949
cpp_namet::namet name("(" + cpp_type2name(type) + ")");
5050
declarator.name().get_sub().back().swap(name);
@@ -110,7 +110,7 @@ symbolt &cpp_declarator_convertert::convert(
110110
{
111111
UNREACHABLE;
112112
typet tmp;
113-
tmp.swap(final_type.subtype());
113+
tmp.swap(to_template_type(final_type).subtype());
114114
final_type.swap(tmp);
115115
}
116116

0 commit comments

Comments
 (0)