Skip to content

Commit 9a680f7

Browse files
author
Daniel Kroening
committed
remove symbol_typet
1 parent 744c6f3 commit 9a680f7

29 files changed

+22
-272
lines changed

src/analyses/invariant_propagation.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -191,8 +191,6 @@ bool invariant_propagationt::check_type(const typet &type) const
191191
return false;
192192
else if(type.id()==ID_array)
193193
return false;
194-
else if(type.id() == ID_symbol_type)
195-
return check_type(ns.follow(type));
196194
else if(type.id()==ID_unsignedbv ||
197195
type.id()==ID_signedbv)
198196
return true;

src/ansi-c/c_typecheck_base.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -415,8 +415,6 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
415415
to_array_type(final_new).size().is_not_nil() &&
416416
final_old.subtype()==final_new.subtype())
417417
{
418-
// we don't do symbol types for arrays anymore
419-
PRECONDITION(old_symbol.type.id() != ID_symbol_type);
420418
old_symbol.type=new_symbol.type;
421419
}
422420
else if(

src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -504,7 +504,6 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
504504

505505
const typet &type=designator.back().subtype;
506506
const typet &full_type=follow(type);
507-
CHECK_RETURN(full_type.id() != ID_symbol_type);
508507

509508
// do we initialize a scalar?
510509
if(full_type.id()!=ID_struct &&

src/ansi-c/expr2c.cpp

Lines changed: 0 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -439,43 +439,6 @@ std::string expr2ct::convert_rec(
439439
{
440440
return convert_array_type(src, qualifiers, declarator);
441441
}
442-
else if(src.id() == ID_symbol_type)
443-
{
444-
symbol_typet symbolic_type=to_symbol_type(src);
445-
const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
446-
447-
// Providing we have a valid identifer, we can just use that rather than
448-
// trying to find the concrete type
449-
if(typedef_identifer!="")
450-
{
451-
return q+id2string(typedef_identifer)+d;
452-
}
453-
else
454-
{
455-
const typet &followed=ns.follow(src);
456-
457-
if(followed.id()==ID_struct)
458-
{
459-
std::string dest=q+"struct";
460-
const irep_idt &tag=to_struct_type(followed).get_tag();
461-
if(tag!="")
462-
dest+=" "+id2string(tag);
463-
dest+=d;
464-
return dest;
465-
}
466-
else if(followed.id()==ID_union)
467-
{
468-
std::string dest=q+"union";
469-
const irep_idt &tag=to_union_type(followed).get_tag();
470-
if(tag!="")
471-
dest+=" "+id2string(tag);
472-
dest+=d;
473-
return dest;
474-
}
475-
else
476-
return convert_rec(followed, new_qualifiers, declarator);
477-
}
478-
}
479442
else if(src.id()==ID_struct_tag)
480443
{
481444
const struct_tag_typet &struct_tag_type=

src/goto-programs/destructor.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,7 @@ code_function_callt get_destructor(
1919
const namespacet &ns,
2020
const typet &type)
2121
{
22-
if(type.id() == ID_symbol_type)
23-
{
24-
return get_destructor(ns, ns.follow(type));
25-
}
26-
else if(type.id()==ID_struct)
22+
if(type.id() == ID_struct)
2723
{
2824
const exprt &methods=static_cast<const exprt&>(type.find(ID_methods));
2925

src/goto-programs/interpreter.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1030,9 +1030,9 @@ mp_integer interpretert::get_size(const typet &type)
10301030
}
10311031
return subtype_size;
10321032
}
1033-
else if(type.id() == ID_symbol_type || type.id() == ID_struct_tag)
1033+
else if(type.id() == ID_struct_tag)
10341034
{
1035-
return get_size(ns.follow(type));
1035+
return get_size(ns.follow_tag(to_struct_tag_type(type)));
10361036
}
10371037

10381038
return 1;

src/goto-programs/json_expr.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -97,9 +97,6 @@ static exprt simplify_json_expr(const exprt &src)
9797
/// \return a json object
9898
json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
9999
{
100-
if(type.id() == ID_symbol_type)
101-
return json(ns.follow(type), ns, mode);
102-
103100
json_objectt result;
104101

105102
if(type.id() == ID_unsignedbv)

src/goto-programs/xml_expr.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,9 +25,6 @@ Author: Daniel Kroening
2525

2626
xmlt xml(const typet &type, const namespacet &ns)
2727
{
28-
if(type.id() == ID_symbol_type)
29-
return xml(ns.follow(type), ns);
30-
3128
xmlt result;
3229

3330
if(type.id() == ID_unsignedbv)

src/goto-symex/goto_symex_state.cpp

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -584,7 +584,6 @@ void goto_symex_statet::rename_address(
584584
// type might not have been renamed in case of nesting of
585585
// structs and pointers/arrays
586586
if(
587-
member_expr.struct_op().type().id() != ID_symbol_type &&
588587
member_expr.struct_op().type().id() != ID_struct_tag &&
589588
member_expr.struct_op().type().id() != ID_union_tag)
590589
{
@@ -645,11 +644,6 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
645644
{
646645
return requires_renaming(to_pointer_type(type).subtype(), ns);
647646
}
648-
else if(type.id() == ID_symbol_type)
649-
{
650-
const symbolt &symbol = ns.lookup(to_symbol_type(type));
651-
return requires_renaming(symbol.type, ns);
652-
}
653647
else if(type.id() == ID_union_tag)
654648
{
655649
const symbolt &symbol = ns.lookup(to_union_tag_type(type));

src/linking/linking.cpp

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -58,9 +58,7 @@ static const typet &follow_tags_symbols(
5858
const namespacet &ns,
5959
const typet &type)
6060
{
61-
if(type.id() == ID_symbol_type)
62-
return ns.follow(type);
63-
else if(type.id()==ID_c_enum_tag)
61+
if(type.id() == ID_c_enum_tag)
6462
return ns.follow_tag(to_c_enum_tag_type(type));
6563
else if(type.id()==ID_struct_tag)
6664
return ns.follow_tag(to_struct_tag_type(type));
@@ -796,10 +794,10 @@ bool linkingt::adjust_object_type_rec(
796794
return false;
797795

798796
if(
799-
t1.id() == ID_symbol_type || t1.id() == ID_struct_tag ||
800-
t1.id() == ID_union_tag || t1.id() == ID_c_enum_tag)
797+
t1.id() == ID_struct_tag || t1.id() == ID_union_tag ||
798+
t1.id() == ID_c_enum_tag)
801799
{
802-
const irep_idt &identifier=t1.get(ID_identifier);
800+
const irep_idt &identifier = to_tag_type(t1).get_identifier();
803801

804802
if(info.o_symbols.insert(identifier).second)
805803
{
@@ -813,10 +811,10 @@ bool linkingt::adjust_object_type_rec(
813811
return false;
814812
}
815813
else if(
816-
t2.id() == ID_symbol_type || t2.id() == ID_struct_tag ||
817-
t2.id() == ID_union_tag || t2.id() == ID_c_enum_tag)
814+
t2.id() == ID_struct_tag || t2.id() == ID_union_tag ||
815+
t2.id() == ID_c_enum_tag)
818816
{
819-
const irep_idt &identifier=t2.get(ID_identifier);
817+
const irep_idt &identifier = to_tag_type(t2).get_identifier();
820818

821819
if(info.n_symbols.insert(identifier).second)
822820
{

src/pointer-analysis/value_set_analysis_fi.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -190,8 +190,6 @@ bool value_set_analysis_fit::check_type(const typet &type)
190190
}
191191
else if(type.id()==ID_array)
192192
return check_type(type.subtype());
193-
else if(type.id() == ID_symbol_type)
194-
return check_type(ns.follow(type));
195193

196194
return false;
197195
}

src/pointer-analysis/value_set_analysis_fivr.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -178,8 +178,6 @@ bool value_set_analysis_fivrt::check_type(const typet &type)
178178
}
179179
else if(type.id()==ID_array)
180180
return check_type(type.subtype());
181-
else if(type.id() == ID_symbol_type)
182-
return check_type(ns.follow(type));
183181

184182
return false;
185183
}

src/pointer-analysis/value_set_analysis_fivrns.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -178,8 +178,6 @@ bool value_set_analysis_fivrnst::check_type(const typet &type)
178178
}
179179
else if(type.id()==ID_array)
180180
return check_type(type.subtype());
181-
else if(type.id() == ID_symbol_type)
182-
return check_type(ns.follow(type));
183181

184182
return false;
185183
}

src/solvers/flattening/boolbv_width.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -180,8 +180,6 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
180180
}
181181
else if(type_id==ID_pointer)
182182
entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
183-
else if(type_id == ID_symbol_type)
184-
entry=get_entry(ns.follow(type));
185183
else if(type_id==ID_struct_tag)
186184
entry=get_entry(ns.follow_tag(to_struct_tag_type(type)));
187185
else if(type_id==ID_union_tag)

src/solvers/flattening/boolbv_with.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -100,8 +100,6 @@ void boolbvt::convert_with(
100100
else if(type.id() == ID_union_tag)
101101
return convert_with(
102102
ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
103-
else if(type.id() == ID_symbol_type)
104-
return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);
105103

106104
error().source_location=type.source_location();
107105
error() << "unexpected with type: " << type.id() << eom;

src/solvers/smt2/smt2_conv.cpp

Lines changed: 0 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -4005,9 +4005,6 @@ void smt2_convt::unflatten(
40054005
const typet &type,
40064006
unsigned nesting)
40074007
{
4008-
if(type.id() == ID_symbol_type)
4009-
return unflatten(where, ns.follow(type));
4010-
40114008
if(type.id()==ID_bool)
40124009
{
40134010
if(where==wheret::BEGIN)
@@ -4533,8 +4530,6 @@ void smt2_convt::convert_type(const typet &type)
45334530
out << "Real";
45344531
else if(type.id()==ID_integer)
45354532
out << "Int";
4536-
else if(type.id() == ID_symbol_type)
4537-
convert_type(ns.follow(type));
45384533
else if(type.id()==ID_complex)
45394534
{
45404535
if(use_datatypes)
@@ -4746,17 +4741,6 @@ void smt2_convt::find_symbols_rec(
47464741
{
47474742
find_symbols_rec(type.subtype(), recstack);
47484743
}
4749-
else if(type.id() == ID_symbol_type)
4750-
{
4751-
const symbol_typet &st=to_symbol_type(type);
4752-
const irep_idt &id=st.get_identifier();
4753-
4754-
if(recstack.find(id)==recstack.end())
4755-
{
4756-
recstack.insert(id);
4757-
find_symbols_rec(ns.follow(type), recstack);
4758-
}
4759-
}
47604744
else if(type.id() == ID_struct_tag)
47614745
{
47624746
const auto &struct_tag = to_struct_tag_type(type);

src/util/base_type.cpp

Lines changed: 9 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -53,20 +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_type)
57-
{
58-
const symbolt *symbol;
59-
60-
if(
61-
!ns.lookup(to_symbol_type(type).get_identifier(), symbol) &&
62-
symbol->is_type && !symbol->type.is_nil())
63-
{
64-
type = symbol->type;
65-
base_type_rec(type, ns, symb); // recursive call
66-
return;
67-
}
68-
}
69-
else if(
56+
if(
7057
type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
7158
type.id() == ID_union_tag)
7259
{
@@ -99,20 +86,7 @@ void base_type_rec(
9986
typet &subtype=to_pointer_type(type).subtype();
10087

10188
// we need to avoid running into an infinite loop
102-
if(subtype.id() == ID_symbol_type)
103-
{
104-
const irep_idt &id = to_symbol_type(subtype).get_identifier();
105-
106-
if(symb.find(id) != symb.end())
107-
return;
108-
109-
symb.insert(id);
110-
111-
base_type_rec(subtype, ns, symb);
112-
113-
symb.erase(id);
114-
}
115-
else if(
89+
if(
11690
subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag ||
11791
subtype.id() == ID_union_tag)
11892
{
@@ -160,8 +134,8 @@ bool base_type_eqt::base_type_eq_rec(
160134

161135
// loop avoidance
162136
if(
163-
(type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
164-
type1.id() == ID_struct_tag || type1.id() == ID_union_tag) &&
137+
(type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
138+
type1.id() == ID_union_tag) &&
165139
type2.id() == type1.id())
166140
{
167141
// already in same set?
@@ -172,8 +146,8 @@ bool base_type_eqt::base_type_eq_rec(
172146
}
173147

174148
if(
175-
type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag ||
176-
type1.id() == ID_struct_tag || type1.id() == ID_union_tag)
149+
type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag ||
150+
type1.id() == ID_union_tag)
177151
{
178152
const symbolt &symbol=
179153
ns.lookup(type1.get(ID_identifier));
@@ -185,8 +159,8 @@ bool base_type_eqt::base_type_eq_rec(
185159
}
186160

187161
if(
188-
type2.id() == ID_symbol_type || type2.id() == ID_c_enum_tag ||
189-
type2.id() == ID_struct_tag || type2.id() == ID_union_tag)
162+
type2.id() == ID_c_enum_tag || type2.id() == ID_struct_tag ||
163+
type2.id() == ID_union_tag)
190164
{
191165
const symbolt &symbol=
192166
ns.lookup(type2.get(ID_identifier));
@@ -309,9 +283,8 @@ bool base_type_eqt::base_type_eq_rec(
309283
/// Check types for equality across all levels of hierarchy. For equality
310284
/// in the top level of the hierarchy only use \ref type_eq.
311285
/// Example:
312-
/// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal,
313286
/// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a")
314-
/// .type}` will also compare equal.
287+
/// .type}` will compare equal.
315288
/// \param type1: The first type to compare.
316289
/// \param type2: The second type to compare.
317290
/// \param ns: The namespace, needed for resolution of symbols.

src/util/endianness_map.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +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_type)
55-
build_big_endian(ns.follow(src));
56-
else if(src.id()==ID_c_enum_tag)
54+
if(src.id() == ID_c_enum_tag)
5755
build_big_endian(ns.follow_tag(to_c_enum_tag_type(src)));
5856
else if(src.id()==ID_unsignedbv ||
5957
src.id()==ID_signedbv ||

src/util/expr_initializer.cpp

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -261,19 +261,6 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
261261
return std::move(value);
262262
}
263263
}
264-
else if(type_id == ID_symbol_type)
265-
{
266-
auto result = expr_initializer_rec(ns.follow(type), source_location);
267-
268-
if(!result.has_value())
269-
return {};
270-
271-
// we might have mangled the type for arrays, so keep that
272-
if(type.id() != ID_array)
273-
result->type() = type;
274-
275-
return *result;
276-
}
277264
else if(type_id==ID_c_enum_tag)
278265
{
279266
auto result = expr_initializer_rec(

src/util/find_symbols.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -156,8 +156,6 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
156156
// dest.insert(identifier);
157157
}
158158
}
159-
else if(src.id() == ID_symbol_type)
160-
dest.insert(to_symbol_type(src).get_identifier());
161159
else if(src.id()==ID_array)
162160
{
163161
// do the size -- the subtype is already done

src/util/format_type.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -79,8 +79,6 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
7979
return os << "struct " << to_struct_tag_type(type).get_identifier();
8080
else if(id == ID_c_enum_tag)
8181
return os << "c_enum " << to_c_enum_tag_type(type).get_identifier();
82-
else if(id == ID_symbol_type)
83-
return os << "symbol_type " << to_symbol_type(type).get_identifier();
8482
else if(id == ID_signedbv)
8583
return os << "signedbv[" << to_signedbv_type(type).get_width() << ']';
8684
else if(id == ID_unsignedbv)

0 commit comments

Comments
 (0)