Skip to content

Commit a152839

Browse files
author
Daniel Kroening
committed
type symbols now use ID_symbol_type
1 parent d24f773 commit a152839

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

45 files changed

+97
-97
lines changed

‎jbmc/src/java_bytecode/ci_lazy_methods.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -565,7 +565,7 @@ void ci_lazy_methodst::gather_field_types(
565565
{
566566
// If class_type is not a symbol this may be a reference array,
567567
// but we can't tell what type.
568-
if(class_type.id() == ID_symbol)
568+
if(class_type.id() == ID_symbol_type)
569569
{
570570
const typet &element_type =
571571
java_array_element_type(to_symbol_type(class_type));
@@ -581,11 +581,11 @@ void ci_lazy_methodst::gather_field_types(
581581
{
582582
for(const auto &field : underlying_type.components())
583583
{
584-
if(field.type().id() == ID_struct || field.type().id() == ID_symbol)
584+
if(field.type().id() == ID_struct || field.type().id() == ID_symbol_type)
585585
gather_field_types(field.type(), ns, needed_lazy_methods);
586586
else if(field.type().id() == ID_pointer)
587587
{
588-
if(field.type().subtype().id() == ID_symbol)
588+
if(field.type().subtype().id() == ID_symbol_type)
589589
{
590590
initialize_all_instantiated_classes_from_pointer(
591591
to_pointer_type(field.type()), ns, needed_lazy_methods);

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2049,15 +2049,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
20492049

20502050
if(needed_lazy_methods)
20512051
{
2052-
if(arg0.type().id()==ID_symbol)
2052+
if(arg0.type().id()==ID_symbol_type)
20532053
{
20542054
needed_lazy_methods->add_needed_class(
20552055
to_symbol_type(arg0.type()).get_identifier());
20562056
}
20572057
else if(arg0.type().id()==ID_pointer)
20582058
{
20592059
const auto &pointer_type=to_pointer_type(arg0.type());
2060-
if(pointer_type.subtype().id()==ID_symbol)
2060+
if(pointer_type.subtype().id()==ID_symbol_type)
20612061
{
20622062
needed_lazy_methods->add_needed_class(
20632063
to_symbol_type(pointer_type.subtype()).get_identifier());
@@ -2107,7 +2107,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
21072107
symbol_table.has_symbol(symbol_expr.get_identifier()),
21082108
"putstatic symbol should have been created before method conversion");
21092109

2110-
if(needed_lazy_methods && arg0.type().id() == ID_symbol)
2110+
if(needed_lazy_methods && arg0.type().id() == ID_symbol_type)
21112111
{
21122112
needed_lazy_methods->add_needed_class(
21132113
to_symbol_type(arg0.type()).get_identifier());
@@ -2265,7 +2265,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
22652265
const typecast_exprt pointer(op[0], java_array_type(statement[0]));
22662266

22672267
dereference_exprt array(pointer, pointer.type().subtype());
2268-
assert(pointer.type().subtype().id()==ID_symbol);
2268+
assert(pointer.type().subtype().id()==ID_symbol_type);
22692269
array.set(ID_java_member_access, true);
22702270

22712271
const member_exprt length(array, "length", java_int_type());

‎jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ java_bytecode_parse_treet::find_annotation(
117117
if(annotation.type.id() != ID_pointer)
118118
return false;
119119
const typet &type = annotation.type.subtype();
120-
return type.id() == ID_symbol &&
120+
return type.id() == ID_symbol_type &&
121121
to_symbol_type(type).get_identifier() == annotation_type_name;
122122
});
123123
if(annotation_it == annotations.end())

‎jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
1616

1717
void java_bytecode_typecheckt::typecheck_type(typet &type)
1818
{
19-
if(type.id()==ID_symbol)
19+
if(type.id()==ID_symbol_type)
2020
{
2121
irep_idt identifier=to_symbol_type(type).get_identifier();
2222

‎jbmc/src/java_bytecode/java_object_factory.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1216,7 +1216,7 @@ void java_object_factoryt::gen_nondet_init(
12161216
if(is_sub)
12171217
{
12181218
const typet &symbol = override_ ? override_type : expr.type();
1219-
PRECONDITION(symbol.id() == ID_symbol);
1219+
PRECONDITION(symbol.id() == ID_symbol_type);
12201220
generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
12211221
to_symbol_type(symbol), struct_type);
12221222
}
@@ -1321,7 +1321,7 @@ void java_object_factoryt::gen_nondet_array_init(
13211321
update_in_placet update_in_place)
13221322
{
13231323
PRECONDITION(expr.type().id()==ID_pointer);
1324-
PRECONDITION(expr.type().subtype().id()==ID_symbol);
1324+
PRECONDITION(expr.type().subtype().id()==ID_symbol_type);
13251325
PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);
13261326

13271327
const typet &type=ns.follow(expr.type().subtype());

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ Date: April 2017
3636
irep_idt get_tag(const typet &type)
3737
{
3838
/// \todo Use follow instead of assuming tag to symbol relationship.
39-
if(type.id() == ID_symbol)
39+
if(type.id() == ID_symbol_type)
4040
return to_symbol_type(type).get_identifier();
4141
else if(type.id() == ID_struct)
4242
return irep_idt("java::" + id2string(to_struct_type(type).get_tag()));
@@ -393,11 +393,11 @@ java_string_library_preprocesst::process_equals_function_operands(
393393
/// \return type of the "data" component
394394
static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
395395
{
396-
PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
397-
if(type.id()==ID_symbol)
396+
PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol_type);
397+
if(type.id()==ID_symbol_type)
398398
{
399399
symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
400-
CHECK_RETURN(sym.type.id()!=ID_symbol);
400+
CHECK_RETURN(sym.type.id()!=ID_symbol_type);
401401
return get_data_type(sym.type, symbol_table);
402402
}
403403
// else type id is ID_struct
@@ -412,11 +412,11 @@ static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
412412
static typet
413413
get_length_type(const typet &type, const symbol_tablet &symbol_table)
414414
{
415-
PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
416-
if(type.id()==ID_symbol)
415+
PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol_type);
416+
if(type.id()==ID_symbol_type)
417417
{
418418
symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
419-
CHECK_RETURN(sym.type.id()!=ID_symbol);
419+
CHECK_RETURN(sym.type.id()!=ID_symbol_type);
420420
return get_length_type(sym.type, symbol_table);
421421
}
422422
// else type id is ID_struct
@@ -891,7 +891,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
891891
PRECONDITION(implements_java_char_sequence_pointer(rhs.type()));
892892

893893
typet deref_type;
894-
if(rhs.type().subtype().id()==ID_symbol)
894+
if(rhs.type().subtype().id()==ID_symbol_type)
895895
deref_type=symbol_table.lookup_ref(
896896
to_symbol_type(rhs.type().subtype()).get_identifier()).type;
897897
else

‎jbmc/src/java_bytecode/java_types.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -738,7 +738,7 @@ bool equal_java_types(const typet &type1, const typet &type2)
738738
bool arrays_with_same_element_type = true;
739739
if(
740740
type1.id() == ID_pointer && type2.id() == ID_pointer &&
741-
type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol)
741+
type1.subtype().id() == ID_symbol_type && type2.subtype().id() == ID_symbol_type)
742742
{
743743
const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype());
744744
const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype());
@@ -785,7 +785,7 @@ void get_dependencies_from_generic_parameters_rec(
785785
}
786786

787787
// symbol type
788-
else if(t.id() == ID_symbol)
788+
else if(t.id() == ID_symbol_type)
789789
{
790790
const symbol_typet &symbol_type = to_symbol_type(t);
791791
const irep_idt class_name(symbol_type.get_identifier());
@@ -919,7 +919,7 @@ std::string pretty_java_type(const typet &type)
919919
return "byte";
920920
else if(is_reference(type))
921921
{
922-
if(type.subtype().id() == ID_symbol)
922+
if(type.subtype().id() == ID_symbol_type)
923923
{
924924
const auto &symbol_type = to_symbol_type(type.subtype());
925925
const irep_idt &id = symbol_type.get_identifier();

‎jbmc/src/java_bytecode/remove_instanceof.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ std::size_t remove_instanceoft::lower_instanceof(
8080

8181
// Find all types we know about that satisfy the given requirement:
8282
INVARIANT(
83-
target_type.id()==ID_symbol,
83+
target_type.id()==ID_symbol_type,
8484
"instanceof second operand should have a simple type");
8585
const irep_idt &target_name=
8686
to_symbol_type(target_type).get_identifier();

‎jbmc/src/java_bytecode/select_pointer_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ pointer_typet select_pointer_typet::specialize_generics(
8888
generic_parameter_specialization_map)
8989
: type;
9090
}
91-
else if(pointer_type.subtype().id() == ID_symbol)
91+
else if(pointer_type.subtype().id() == ID_symbol_type)
9292
{
9393
// if the pointer is an array, recursively specialize its element type
9494
const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype());

‎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/ansi-c/c_typecast.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -252,15 +252,15 @@ bool check_c_implicit_typecast(
252252

253253
typet c_typecastt::follow_with_qualifiers(const typet &src_type)
254254
{
255-
if(src_type.id()!=ID_symbol)
255+
if(src_type.id()!=ID_symbol_type)
256256
return src_type;
257257

258258
typet result_type=src_type;
259259

260260
// collect qualifiers
261261
c_qualifierst qualifiers(src_type);
262262

263-
while(result_type.id()==ID_symbol)
263+
while(result_type.id()==ID_symbol_type)
264264
{
265265
const symbolt &followed_type_symbol =
266266
ns.lookup(to_symbol_type(result_type));
@@ -345,7 +345,7 @@ c_typecastt::c_typet c_typecastt::get_c_type(
345345
{
346346
return INT;
347347
}
348-
else if(type.id()==ID_symbol)
348+
else if(type.id()==ID_symbol_type)
349349
return get_c_type(ns.follow(type));
350350
else if(type.id()==ID_rational)
351351
return RATIONAL;

‎src/ansi-c/c_typecheck_base.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -404,7 +404,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
404404
final_old.subtype()==final_new.subtype())
405405
{
406406
// we don't do symbol types for arrays anymore
407-
PRECONDITION(old_symbol.type.id()!=ID_symbol);
407+
PRECONDITION(old_symbol.type.id()!=ID_symbol_type);
408408
old_symbol.type=new_symbol.type;
409409
}
410410
else if((final_old.id()==ID_incomplete_c_enum ||

‎src/ansi-c/c_typecheck_code.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -383,7 +383,7 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const
383383
}
384384
else if(type.id()==ID_vector)
385385
return is_complete_type(type.subtype());
386-
else if(type.id()==ID_symbol)
386+
else if(type.id()==ID_symbol_type)
387387
return is_complete_type(follow(type));
388388

389389
return true;

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -88,9 +88,9 @@ bool c_typecheck_baset::gcc_types_compatible_p(
8888
// read
8989
// http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
9090

91-
if(type1.id()==ID_symbol)
91+
if(type1.id()==ID_symbol_type)
9292
return gcc_types_compatible_p(follow(type1), type2);
93-
else if(type2.id()==ID_symbol)
93+
else if(type2.id()==ID_symbol_type)
9494
return gcc_types_compatible_p(type1, follow(type2));
9595

9696
// check qualifiers first
@@ -523,8 +523,8 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr)
523523

524524
forall_operands(m_it, member)
525525
{
526-
if(type.id()==ID_symbol)
527-
type=follow(type);
526+
if(type.id()==ID_symbol_type)
527+
type=follow(to_symbol_type(type));
528528

529529
if(m_it->id()==ID_member)
530530
{
@@ -3032,8 +3032,8 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
30323032

30333033
typet subtype=type.subtype();
30343034

3035-
if(subtype.id()==ID_symbol)
3036-
subtype=follow(subtype);
3035+
if(subtype.id()==ID_symbol_type)
3036+
subtype=follow(to_symbol_type(subtype));
30373037

30383038
if(subtype.id()==ID_incomplete_struct)
30393039
{

‎src/ansi-c/expr2c.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -457,7 +457,7 @@ std::string expr2ct::convert_rec(
457457
return convert_rec(
458458
src.subtype(), qualifiers, declarator+"[]");
459459
}
460-
else if(src.id()==ID_symbol)
460+
else if(src.id()==ID_symbol_type)
461461
{
462462
symbol_typet symbolic_type=to_symbol_type(src);
463463
const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);

‎src/ansi-c/padding.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -82,8 +82,8 @@ mp_integer alignment(const typet &type, const namespacet &ns)
8282
result=alignment(type.subtype(), ns);
8383
else if(type.id()==ID_c_enum_tag)
8484
result=alignment(ns.follow_tag(to_c_enum_tag_type(type)), ns);
85-
else if(type.id()==ID_symbol)
86-
result=alignment(ns.follow(type), ns);
85+
else if(type.id()==ID_symbol_type)
86+
result=alignment(ns.follow(to_symbol_type(type)), ns);
8787
else if(type.id()==ID_c_bit_field)
8888
{
8989
// we align these according to the 'underlying type'

‎src/ansi-c/type2name.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -187,7 +187,7 @@ static std::string type2name(
187187
else
188188
result+="ARR"+integer2string(size);
189189
}
190-
else if(type.id()==ID_symbol ||
190+
else if(type.id()==ID_symbol_type ||
191191
type.id()==ID_c_enum_tag ||
192192
type.id()==ID_struct_tag ||
193193
type.id()==ID_union_tag)

‎src/cpp/cpp_convert_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -574,7 +574,7 @@ void cpp_convert_plain_type(typet &type)
574574
type.id()==ID_bool ||
575575
type.id()==ID_floatbv ||
576576
type.id()==ID_empty ||
577-
type.id()==ID_symbol ||
577+
type.id()==ID_symbol_type ||
578578
type.id()==ID_constructor ||
579579
type.id()==ID_destructor)
580580
{

‎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));

0 commit comments

Comments
 (0)