Skip to content

Commit dbc4f1d

Browse files
author
Daniel Kroening
committed
fx
1 parent 42857bf commit dbc4f1d

25 files changed

+60
-60
lines changed

‎src/analyses/invariant_propagation.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,7 @@ bool invariant_propagationt::check_type(const typet &type) const
189189
return false;
190190
else if(type.id()==ID_array)
191191
return false;
192-
else if(type.id()==ID_symbol)
192+
else if(type.id()==ID_symbol_type)
193193
return check_type(ns.follow(type));
194194
else if(type.id()==ID_unsignedbv ||
195195
type.id()==ID_signedbv)

‎src/analyses/uncaught_exceptions_analysis.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,10 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type)
1919
{
2020
PRECONDITION(type.id()==ID_pointer);
2121

22-
if(type.subtype().id()==ID_symbol)
23-
{
22+
if(type.subtype().id()==ID_symbol_type)
2423
return to_symbol_type(type.subtype()).get_identifier();
25-
}
26-
return ID_empty;
24+
else
25+
return ID_empty;
2726
}
2827

2928
/// Returns the symbol corresponding to an exception

‎src/cpp/cpp_instantiate_template.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,8 @@ std::string cpp_typecheckt::template_suffix(
4646
if(expr.id()==ID_type)
4747
{
4848
const typet &type=expr.type();
49-
if(type.id()==ID_symbol)
50-
result+=type.get_string(ID_identifier);
49+
if(type.id()==ID_symbol_type)
50+
result+=id2string(to_symbol_type(type).get_identifier());
5151
else
5252
result+=cpp_type2name(type);
5353
}
@@ -186,7 +186,7 @@ const symbolt &cpp_typecheckt::class_template_symbol(
186186
void cpp_typecheckt::elaborate_class_template(
187187
const typet &type)
188188
{
189-
if(type.id()!=ID_symbol)
189+
if(type.id()!=ID_symbol_type)
190190
return;
191191

192192
const symbolt &symbol = lookup(to_symbol_type(type));

‎src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -170,9 +170,9 @@ void cpp_typecheck_resolvet::remove_duplicates(
170170
irep_idt id;
171171

172172
if(it->id()==ID_symbol)
173-
id=it->get(ID_identifier);
174-
else if(it->id()==ID_type && it->type().id()==ID_symbol)
175-
id=it->type().get(ID_identifier);
173+
id=to_symbol_expr(*it).get_identifier();
174+
else if(it->id()==ID_type && it->type().id()==ID_symbol_type)
175+
id=to_symbol_type(it->type()).get_identifier();
176176

177177
if(id=="")
178178
{
@@ -350,7 +350,7 @@ exprt cpp_typecheck_resolvet::convert_identifier(
350350
typet followed_type=symbol.type;
351351
bool constant=followed_type.get_bool(ID_C_constant);
352352

353-
while(followed_type.id()==ID_symbol)
353+
while(followed_type.id()==ID_symbol_type)
354354
{
355355
followed_type =
356356
cpp_typecheck.follow(to_symbol_type(followed_type));
@@ -2238,8 +2238,8 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
22382238
assert(pcomp.get_bool(ID_is_type));
22392239
const typet &type=pcomp.type();
22402240
assert(type.id()!=ID_struct);
2241-
if(type.id()==ID_symbol)
2242-
identifier=type.get(ID_identifier);
2241+
if(type.id()==ID_symbol_type)
2242+
identifier=to_symbol_type(type).get_identifier();
22432243
else
22442244
continue;
22452245
}
@@ -2260,8 +2260,8 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
22602260
new_set.insert(&class_id);
22612261
break;
22622262
}
2263-
else if(symbol.type.id()==ID_symbol)
2264-
identifier=symbol.type.get(ID_identifier);
2263+
else if(symbol.type.id()==ID_symbol_type)
2264+
identifier=to_symbol_type(symbol.type).get_identifier();
22652265
else
22662266
break;
22672267
}
@@ -2303,7 +2303,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
23032303
if(e.id()!=ID_type)
23042304
continue; // expressions are definitively not a scope
23052305

2306-
if(e.type().id()==ID_symbol)
2306+
if(e.type().id()==ID_symbol_type)
23072307
{
23082308
symbol_typet type=to_symbol_type(e.type());
23092309

@@ -2314,7 +2314,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
23142314
const symbolt &symbol=cpp_typecheck.lookup(identifier);
23152315
assert(symbol.is_type);
23162316

2317-
if(symbol.type.id()==ID_symbol)
2317+
if(symbol.type.id()==ID_symbol_type)
23182318
type=to_symbol_type(symbol.type);
23192319
else if(symbol.type.id()==ID_struct ||
23202320
symbol.type.id()==ID_incomplete_struct ||

‎src/cpp/cpp_typecheck_template.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -793,8 +793,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
793793
// is it a type or not?
794794
if(declaration.get_bool(ID_is_type))
795795
{
796-
parameter=exprt(ID_type, typet(ID_symbol));
797-
parameter.type().set(ID_identifier, identifier);
796+
parameter=exprt(ID_type, symbol_typet(identifier));
798797
parameter.type().add_source_location()=declaration.find_source_location();
799798
}
800799
else
@@ -829,8 +828,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
829828
830829
if(cpp_declarator_converter.is_typedef)
831830
{
832-
parameter=exprt(ID_type, typet(ID_symbol));
833-
parameter.type().set(ID_identifier, symbol.name);
831+
parameter=exprt(ID_type, symbol_typet(symbol.name));
834832
parameter.type().add_source_location()=declaration.find_location();
835833
}
836834
else

‎src/cpp/template_map.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
1414
#include <ostream>
1515

1616
#include <util/invariant.h>
17+
#include <util/std_expr.h>
18+
#include <util/std_types.h>
1719

1820
void template_mapt::apply(typet &type) const
1921
{
@@ -37,10 +39,10 @@ void template_mapt::apply(typet &type) const
3739
apply(subtype);
3840
}
3941
}
40-
else if(type.id()==ID_symbol)
42+
else if(type.id()==ID_symbol_type)
4143
{
4244
type_mapt::const_iterator m_it=
43-
type_map.find(type.get(ID_identifier));
45+
type_map.find(to_symbol_type(type).get_identifier());
4446

4547
if(m_it!=type_map.end())
4648
{
@@ -74,7 +76,7 @@ void template_mapt::apply(exprt &expr) const
7476
if(expr.id()==ID_symbol)
7577
{
7678
expr_mapt::const_iterator m_it=
77-
expr_map.find(expr.get(ID_identifier));
79+
expr_map.find(to_symbol_expr(expr).get_identifier());
7880

7981
if(m_it!=expr_map.end())
8082
{

‎src/goto-instrument/dump_c.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ void dump_ct::operator()(std::ostream &os)
6161
{
6262
typet &type=it2->type();
6363

64-
if(type.id()==ID_symbol &&
64+
if(type.id()==ID_symbol_type &&
6565
type.get_bool(ID_C_transparent_union))
6666
{
6767
symbolt new_type_sym=
@@ -314,7 +314,7 @@ void dump_ct::convert_compound(
314314
bool recursive,
315315
std::ostream &os)
316316
{
317-
if(type.id()==ID_symbol)
317+
if(type.id()==ID_symbol_type)
318318
{
319319
const symbolt &symbol=
320320
ns.lookup(to_symbol_type(type).get_identifier());
@@ -382,7 +382,7 @@ void dump_ct::convert_compound(
382382
UNREACHABLE;
383383
/*
384384
assert(parent_it->id() == ID_base);
385-
assert(parent_it->get(ID_type) == ID_symbol);
385+
assert(parent_it->get(ID_type) == ID_symbol_type);
386386
387387
const irep_idt &base_id=
388388
parent_it->find(ID_type).get(ID_identifier);
@@ -669,7 +669,7 @@ void dump_ct::collect_typedefs_rec(
669669
{
670670
collect_typedefs_rec(type.subtype(), early, local_deps);
671671
}
672-
else if(type.id()==ID_symbol)
672+
else if(type.id()==ID_symbol_type)
673673
{
674674
const symbolt &symbol=
675675
ns.lookup(to_symbol_type(type).get_identifier());

‎src/goto-instrument/goto_program2code.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1429,7 +1429,7 @@ goto_programt::const_targett goto_program2codet::convert_catch(
14291429

14301430
void goto_program2codet::add_local_types(const typet &type)
14311431
{
1432-
if(type.id()==ID_symbol)
1432+
if(type.id()==ID_symbol_type)
14331433
{
14341434
const typet &full_type=ns.follow(type);
14351435

@@ -1662,7 +1662,7 @@ void goto_program2codet::remove_const(typet &type)
16621662
if(type.get_bool(ID_C_constant))
16631663
type.remove(ID_C_constant);
16641664

1665-
if(type.id()==ID_symbol)
1665+
if(type.id()==ID_symbol_type)
16661666
{
16671667
const irep_idt &identifier=to_symbol_type(type).get_identifier();
16681668
if(!const_removed.insert(identifier).second)
@@ -1864,7 +1864,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
18641864
if(no_typecast)
18651865
return;
18661866

1867-
assert(expr.type().id()==ID_symbol);
1867+
assert(expr.type().id()==ID_symbol_type);
18681868

18691869
const typet &t=expr.type();
18701870

‎src/goto-programs/destructor.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ code_function_callt get_destructor(
1919
const namespacet &ns,
2020
const typet &type)
2121
{
22-
if(type.id()==ID_symbol)
22+
if(type.id()==ID_symbol_type)
2323
{
2424
return get_destructor(ns, ns.follow(type));
2525
}

‎src/goto-programs/interpreter.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1039,10 +1039,11 @@ mp_integer interpretert::get_size(const typet &type)
10391039
}
10401040
return subtype_size;
10411041
}
1042-
else if(type.id()==ID_symbol)
1042+
else if(type.id()==ID_symbol_type)
10431043
{
10441044
return get_size(ns.follow(type));
10451045
}
1046+
10461047
return 1;
10471048
}
10481049

‎src/goto-programs/string_abstraction.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ class string_abstractiont:public messaget
5252

5353
bool is_char_type(const typet &type) const
5454
{
55-
if(type.id()==ID_symbol)
55+
if(type.id()==ID_symbol_type)
5656
return is_char_type(ns.follow(type));
5757

5858
if(type.id()!=ID_signedbv &&

‎src/goto-symex/goto_symex_state.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -755,7 +755,7 @@ void goto_symex_statet::rename_address(
755755

756756
// type might not have been renamed in case of nesting of
757757
// structs and pointers/arrays
758-
if(member_expr.struct_op().type().id()!=ID_symbol)
758+
if(member_expr.struct_op().type().id()!=ID_symbol_type)
759759
{
760760
const struct_union_typet &su_type=
761761
to_struct_union_type(member_expr.struct_op().type());
@@ -838,7 +838,7 @@ void goto_symex_statet::rename(
838838
{
839839
rename(type.subtype(), irep_idt(), ns, level);
840840
}
841-
else if(type.id()==ID_symbol)
841+
else if(type.id()==ID_symbol_type)
842842
{
843843
const symbolt &symbol=
844844
ns.lookup(to_symbol_type(type).get_identifier());

‎src/linking/linking.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ static const typet &follow_tags_symbols(
4444
const namespacet &ns,
4545
const typet &type)
4646
{
47-
if(type.id()==ID_symbol)
47+
if(type.id()==ID_symbol_type)
4848
return ns.follow(type);
4949
else if(type.id()==ID_c_enum_tag)
5050
return ns.follow_tag(to_c_enum_tag_type(type));
@@ -779,7 +779,7 @@ bool linkingt::adjust_object_type_rec(
779779
if(base_type_eq(t1, t2, ns))
780780
return false;
781781

782-
if(t1.id()==ID_symbol ||
782+
if(t1.id()==ID_symbol_type ||
783783
t1.id()==ID_struct_tag ||
784784
t1.id()==ID_union_tag ||
785785
t1.id()==ID_c_enum_tag)
@@ -797,7 +797,7 @@ bool linkingt::adjust_object_type_rec(
797797

798798
return false;
799799
}
800-
else if(t2.id()==ID_symbol ||
800+
else if(t2.id()==ID_symbol_type ||
801801
t2.id()==ID_struct_tag ||
802802
t2.id()==ID_union_tag ||
803803
t2.id()==ID_c_enum_tag)

‎src/linking/zero_initializer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -262,7 +262,7 @@ exprt zero_initializert::zero_initializer_rec(
262262

263263
return value;
264264
}
265-
else if(type_id==ID_symbol)
265+
else if(type_id==ID_symbol_type)
266266
{
267267
exprt result=zero_initializer_rec(ns.follow(type), source_location);
268268
// we might have mangled the type for arrays, so keep that

‎src/solvers/refinement/string_refinement_util.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ bool is_char_type(const typet &type)
3636

3737
bool is_char_array_type(const typet &type, const namespacet &ns)
3838
{
39-
if(type.id() == ID_symbol)
39+
if(type.id() == ID_symbol_type)
4040
return is_char_array_type(ns.follow(type), ns);
4141
return type.id() == ID_array && is_char_type(type.subtype());
4242
}

‎src/util/base_type.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ class base_type_eqt
5353
void base_type_rec(
5454
typet &type, const namespacet &ns, std::set<irep_idt> &symb)
5555
{
56-
if(type.id()==ID_symbol ||
56+
if(type.id()==ID_symbol_type ||
5757
type.id()==ID_c_enum_tag ||
5858
type.id()==ID_struct_tag ||
5959
type.id()==ID_union_tag)
@@ -87,7 +87,7 @@ void base_type_rec(
8787
typet &subtype=to_pointer_type(type).subtype();
8888

8989
// we need to avoid running into an infinite loop
90-
if(subtype.id()==ID_symbol ||
90+
if(subtype.id()==ID_symbol_type ||
9191
subtype.id()==ID_c_enum_tag ||
9292
subtype.id()==ID_struct_tag ||
9393
subtype.id()==ID_union_tag)
@@ -135,7 +135,7 @@ bool base_type_eqt::base_type_eq_rec(
135135
#endif
136136

137137
// loop avoidance
138-
if((type1.id()==ID_symbol ||
138+
if((type1.id()==ID_symbol_type ||
139139
type1.id()==ID_c_enum_tag ||
140140
type1.id()==ID_struct_tag ||
141141
type1.id()==ID_union_tag) &&
@@ -148,7 +148,7 @@ bool base_type_eqt::base_type_eq_rec(
148148
return true;
149149
}
150150

151-
if(type1.id()==ID_symbol ||
151+
if(type1.id()==ID_symbol_type ||
152152
type1.id()==ID_c_enum_tag ||
153153
type1.id()==ID_struct_tag ||
154154
type1.id()==ID_union_tag)
@@ -162,7 +162,7 @@ bool base_type_eqt::base_type_eq_rec(
162162
return base_type_eq_rec(symbol.type, type2);
163163
}
164164

165-
if(type2.id()==ID_symbol ||
165+
if(type2.id()==ID_symbol_type ||
166166
type2.id()==ID_c_enum_tag ||
167167
type2.id()==ID_struct_tag ||
168168
type2.id()==ID_union_tag)

‎src/util/endianness_map.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ void endianness_mapt::build_little_endian(const typet &src)
5151

5252
void endianness_mapt::build_big_endian(const typet &src)
5353
{
54-
if(src.id()==ID_symbol)
54+
if(src.id()==ID_symbol_type)
5555
build_big_endian(ns.follow(src));
5656
else if(src.id()==ID_c_enum_tag)
5757
build_big_endian(ns.follow_tag(to_c_enum_tag_type(src)));

‎src/util/find_symbols.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -160,8 +160,8 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
160160
// dest.insert(identifier);
161161
}
162162
}
163-
else if(src.id()==ID_symbol)
164-
dest.insert(src.get(ID_identifier));
163+
else if(src.id()==ID_symbol_type)
164+
dest.insert(to_symbol_type(src).get_identifier());
165165
else if(src.id()==ID_array)
166166
{
167167
// do the size -- the subtype is already done

‎src/util/format_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
5151
}
5252
else if(id == ID_struct)
5353
return format_rec(os, to_struct_type(type));
54-
else if(id == ID_symbol)
54+
else if(id == ID_symbol_type)
5555
return os << "symbol_type " << to_symbol_type(type).get_identifier();
5656
else
5757
return os << id;

‎src/util/json_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ json_objectt json(
117117
const namespacet &ns,
118118
const irep_idt &mode)
119119
{
120-
if(type.id()==ID_symbol)
120+
if(type.id()==ID_symbol_type)
121121
return json(ns.follow(type), ns, mode);
122122

123123
json_objectt result;

0 commit comments

Comments
 (0)