Skip to content

Commit f93deec

Browse files
author
Daniel Kroening
committed
type symbols now use ID_symbol_type
1 parent 22b755a commit f93deec

Some content is hidden

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

60 files changed

+149
-157
lines changed

‎jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ void ci_lazy_methods_neededt::gather_field_types(
112112
{
113113
// If class_type is not a symbol this may be a reference array,
114114
// but we can't tell what type.
115-
if(class_type.id() == ID_symbol)
115+
if(class_type.id() == ID_symbol_type)
116116
{
117117
const typet &element_type =
118118
java_array_element_type(to_symbol_type(class_type));
@@ -127,11 +127,11 @@ void ci_lazy_methods_neededt::gather_field_types(
127127
{
128128
for(const auto &field : underlying_type.components())
129129
{
130-
if(field.type().id() == ID_struct || field.type().id() == ID_symbol)
130+
if(field.type().id() == ID_struct || field.type().id() == ID_symbol_type)
131131
gather_field_types(field.type(), ns);
132132
else if(field.type().id() == ID_pointer)
133133
{
134-
if(field.type().subtype().id() == ID_symbol)
134+
if(field.type().subtype().id() == ID_symbol_type)
135135
{
136136
add_all_needed_classes(to_pointer_type(field.type()));
137137
}

‎jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1633,7 +1633,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
16331633
const typecast_exprt pointer(op[0], java_array_type(statement[0]));
16341634

16351635
dereference_exprt array(pointer, pointer.type().subtype());
1636-
assert(pointer.type().subtype().id()==ID_symbol);
1636+
assert(pointer.type().subtype().id() == ID_symbol_type);
16371637
array.set(ID_java_member_access, true);
16381638

16391639
const member_exprt length(array, "length", java_int_type());
@@ -2562,7 +2562,7 @@ codet java_bytecode_convert_methodt::convert_putstatic(
25622562
const exprt::operandst &op,
25632563
const symbol_exprt &symbol_expr)
25642564
{
2565-
if(needed_lazy_methods && arg0.type().id() == ID_symbol)
2565+
if(needed_lazy_methods && arg0.type().id() == ID_symbol_type)
25662566
{
25672567
needed_lazy_methods->add_needed_class(
25682568
to_symbol_type(arg0.type()).get_identifier());
@@ -2612,15 +2612,15 @@ void java_bytecode_convert_methodt::convert_getstatic(
26122612
{
26132613
if(needed_lazy_methods)
26142614
{
2615-
if(arg0.type().id() == ID_symbol)
2615+
if(arg0.type().id() == ID_symbol_type)
26162616
{
26172617
needed_lazy_methods->add_needed_class(
26182618
to_symbol_type(arg0.type()).get_identifier());
26192619
}
26202620
else if(arg0.type().id() == ID_pointer)
26212621
{
26222622
const auto &pointer_type = to_pointer_type(arg0.type());
2623-
if(pointer_type.subtype().id() == ID_symbol)
2623+
if(pointer_type.subtype().id() == ID_symbol_type)
26242624
{
26252625
needed_lazy_methods->add_needed_class(
26262626
to_symbol_type(pointer_type.subtype()).get_identifier());

‎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_parser.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -616,7 +616,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
616616
for(const auto &p : ct.parameters())
617617
get_class_refs_rec(p.type());
618618
}
619-
else if(src.id()==ID_symbol)
619+
else if(src.id()==ID_symbol_type)
620620
{
621621
irep_idt name=src.get(ID_C_base_name);
622622
if(has_prefix(id2string(name), "array["))

‎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
@@ -1179,7 +1179,7 @@ void java_object_factoryt::gen_nondet_init(
11791179
if(is_sub)
11801180
{
11811181
const typet &symbol = override_ ? override_type : expr.type();
1182-
PRECONDITION(symbol.id() == ID_symbol);
1182+
PRECONDITION(symbol.id() == ID_symbol_type);
11831183
generic_parameter_specialization_map_keys.insert_pairs_for_symbol(
11841184
to_symbol_type(symbol), struct_type);
11851185
}
@@ -1286,7 +1286,7 @@ void java_object_factoryt::gen_nondet_array_init(
12861286
const source_locationt &location)
12871287
{
12881288
PRECONDITION(expr.type().id()==ID_pointer);
1289-
PRECONDITION(expr.type().subtype().id()==ID_symbol);
1289+
PRECONDITION(expr.type().subtype().id() == ID_symbol_type);
12901290
PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);
12911291

12921292
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()));
@@ -394,11 +394,11 @@ java_string_library_preprocesst::process_equals_function_operands(
394394
/// \return type of the "data" component
395395
static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
396396
{
397-
PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
398-
if(type.id()==ID_symbol)
397+
PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type);
398+
if(type.id() == ID_symbol_type)
399399
{
400400
symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
401-
CHECK_RETURN(sym.type.id()!=ID_symbol);
401+
CHECK_RETURN(sym.type.id() != ID_symbol_type);
402402
return get_data_type(sym.type, symbol_table);
403403
}
404404
// else type id is ID_struct
@@ -413,11 +413,11 @@ static typet get_data_type(const typet &type, const symbol_tablet &symbol_table)
413413
static typet
414414
get_length_type(const typet &type, const symbol_tablet &symbol_table)
415415
{
416-
PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol);
417-
if(type.id()==ID_symbol)
416+
PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type);
417+
if(type.id() == ID_symbol_type)
418418
{
419419
symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier());
420-
CHECK_RETURN(sym.type.id()!=ID_symbol);
420+
CHECK_RETURN(sym.type.id() != ID_symbol_type);
421421
return get_length_type(sym.type, symbol_table);
422422
}
423423
// else type id is ID_struct
@@ -892,7 +892,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
892892
PRECONDITION(implements_java_char_sequence_pointer(rhs.type()));
893893

894894
typet deref_type;
895-
if(rhs.type().subtype().id()==ID_symbol)
895+
if(rhs.type().subtype().id() == ID_symbol_type)
896896
deref_type=symbol_table.lookup_ref(
897897
to_symbol_type(rhs.type().subtype()).get_identifier()).type;
898898
else

‎jbmc/src/java_bytecode/java_types.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -777,7 +777,8 @@ bool equal_java_types(const typet &type1, const typet &type2)
777777
bool arrays_with_same_element_type = true;
778778
if(
779779
type1.id() == ID_pointer && type2.id() == ID_pointer &&
780-
type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol)
780+
type1.subtype().id() == ID_symbol_type &&
781+
type2.subtype().id() == ID_symbol_type)
781782
{
782783
const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype());
783784
const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype());
@@ -824,7 +825,7 @@ void get_dependencies_from_generic_parameters_rec(
824825
}
825826

826827
// symbol type
827-
else if(t.id() == ID_symbol)
828+
else if(t.id() == ID_symbol_type)
828829
{
829830
const symbol_typet &symbol_type = to_symbol_type(t);
830831
const irep_idt class_name(symbol_type.get_identifier());
@@ -958,7 +959,7 @@ std::string pretty_java_type(const typet &type)
958959
return "byte";
959960
else if(is_reference(type))
960961
{
961-
if(type.subtype().id() == ID_symbol)
962+
if(type.subtype().id() == ID_symbol_type)
962963
{
963964
const auto &symbol_type = to_symbol_type(type.subtype());
964965
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
@@ -85,7 +85,7 @@ bool remove_instanceoft::lower_instanceof(
8585

8686
// Find all types we know about that satisfy the given requirement:
8787
INVARIANT(
88-
target_type.id()==ID_symbol,
88+
target_type.id() == ID_symbol_type,
8989
"instanceof second operand should have a simple type");
9090
const irep_idt &target_name=
9191
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
@@ -108,7 +108,7 @@ pointer_typet select_pointer_typet::specialize_generics(
108108
visited_nodes.erase(parameter_name);
109109
return returned_type;
110110
}
111-
else if(pointer_type.subtype().id() == ID_symbol)
111+
else if(pointer_type.subtype().id() == ID_symbol_type)
112112
{
113113
// if the pointer is an array, recursively specialize its element type
114114
const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype());

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -427,7 +427,7 @@ require_type::require_complete_java_non_generic_class(const typet &class_type)
427427
const symbol_typet &
428428
require_type::require_symbol(const typet &type, const irep_idt &identifier)
429429
{
430-
REQUIRE(type.id() == ID_symbol);
430+
REQUIRE(type.id() == ID_symbol_type);
431431
const symbol_typet &result = to_symbol_type(type);
432432
if(identifier != "")
433433
{

‎jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ SCENARIO(
6363
next.type(),
6464
{{require_type::type_argument_kindt::Var, "java::KeyValue::K"},
6565
{require_type::type_argument_kindt::Var, "java::KeyValue::V"}});
66-
REQUIRE(next_type.subtype().id() == ID_symbol);
66+
REQUIRE(next_type.subtype().id() == ID_symbol_type);
6767
const symbol_typet &next_symbol = to_symbol_type(next_type.subtype());
6868
REQUIRE(
6969
symbol_table.lookup_ref(next_symbol.get_identifier()).name ==
@@ -75,7 +75,7 @@ SCENARIO(
7575
reverse.type(),
7676
{{require_type::type_argument_kindt::Var, "java::KeyValue::V"},
7777
{require_type::type_argument_kindt::Var, "java::KeyValue::K"}});
78-
REQUIRE(next_type.subtype().id() == ID_symbol);
78+
REQUIRE(next_type.subtype().id() == ID_symbol_type);
7979
const symbol_typet &reverse_symbol = to_symbol_type(reverse_type.subtype());
8080
REQUIRE(
8181
symbol_table.lookup_ref(next_symbol.get_identifier()).name ==

‎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: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -253,7 +253,8 @@ bool check_c_implicit_typecast(
253253
typet c_typecastt::follow_with_qualifiers(const typet &src_type)
254254
{
255255
if(
256-
src_type.id() != ID_symbol && src_type.id() != ID_struct_tag &&
256+
src_type.id() != ID_symbol_type &&
257+
src_type.id() != ID_struct_tag &&
257258
src_type.id() != ID_union_tag)
258259
{
259260
return src_type;
@@ -264,7 +265,8 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
264265
// collect qualifiers
265266
c_qualifierst qualifiers(src_type);
266267

267-
while(result_type.id() == ID_symbol || result_type.id() == ID_struct_tag ||
268+
while(result_type.id() == ID_symbol_type ||
269+
result_type.id() == ID_struct_tag ||
268270
result_type.id() == ID_union_tag)
269271
{
270272
const typet &followed_type = ns.follow(result_type);
@@ -348,7 +350,7 @@ c_typecastt::c_typet c_typecastt::get_c_type(
348350
{
349351
return INT;
350352
}
351-
else if(type.id()==ID_symbol)
353+
else if(type.id() == ID_symbol_type)
352354
return get_c_type(ns.follow(type));
353355
else if(type.id()==ID_rational)
354356
return RATIONAL;

‎src/ansi-c/c_typecheck_base.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -406,7 +406,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
406406
final_old.subtype()==final_new.subtype())
407407
{
408408
// we don't do symbol types for arrays anymore
409-
PRECONDITION(old_symbol.type.id()!=ID_symbol);
409+
PRECONDITION(old_symbol.type.id() != ID_symbol_type);
410410
old_symbol.type=new_symbol.type;
411411
}
412412
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: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -91,9 +91,9 @@ bool c_typecheck_baset::gcc_types_compatible_p(
9191
// read
9292
// http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
9393

94-
if(type1.id()==ID_symbol)
94+
if(type1.id() == ID_symbol_type)
9595
return gcc_types_compatible_p(follow(type1), type2);
96-
else if(type2.id()==ID_symbol)
96+
else if(type2.id() == ID_symbol_type)
9797
return gcc_types_compatible_p(type1, follow(type2));
9898

9999
// check qualifiers first
@@ -3067,8 +3067,8 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr)
30673067

30683068
typet subtype=type.subtype();
30693069

3070-
if(subtype.id()==ID_symbol)
3071-
subtype=follow(subtype);
3070+
if(subtype.id() == ID_symbol_type)
3071+
subtype = follow(to_symbol_type(subtype));
30723072

30733073
if(subtype.id()==ID_incomplete_struct)
30743074
{

‎src/ansi-c/c_typecheck_initializer.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -492,7 +492,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
492492

493493
const typet &type=designator.back().subtype;
494494
const typet &full_type=follow(type);
495-
assert(full_type.id()!=ID_symbol);
495+
assert(full_type.id() != ID_symbol_type);
496496

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

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
8989
typecheck_c_bit_field_type(to_c_bit_field_type(type));
9090
else if(type.id()==ID_typeof)
9191
typecheck_typeof_type(type);
92-
else if(type.id()==ID_symbol)
92+
else if(type.id() == ID_symbol_type)
9393
typecheck_symbol_type(to_symbol_type(type));
9494
else if(type.id() == ID_typedef_type)
9595
typecheck_typedef_type(type);

‎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
@@ -86,8 +86,8 @@ mp_integer alignment(const typet &type, const namespacet &ns)
8686
result = alignment(ns.follow_tag(to_struct_tag_type(type)), ns);
8787
else if(type.id() == ID_union_tag)
8888
result = alignment(ns.follow_tag(to_union_tag_type(type)), ns);
89-
else if(type.id()==ID_symbol)
90-
result=alignment(ns.follow(type), ns);
89+
else if(type.id() == ID_symbol_type)
90+
result = alignment(ns.follow(to_symbol_type(type)), ns);
9191
else if(type.id()==ID_c_bit_field)
9292
{
9393
// we align these according to the 'underlying type'

‎src/ansi-c/type2name.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -187,10 +187,9 @@ static std::string type2name(
187187
else
188188
result+="ARR"+integer2string(size);
189189
}
190-
else if(type.id()==ID_symbol ||
191-
type.id()==ID_c_enum_tag ||
192-
type.id()==ID_struct_tag ||
193-
type.id()==ID_union_tag)
190+
else if(
191+
type.id() == ID_symbol_type || type.id() == ID_c_enum_tag ||
192+
type.id() == ID_struct_tag || type.id() == ID_union_tag)
194193
{
195194
parent_is_sym_check=true;
196195
result+=type2name_symbol(type, ns, symbol_number);

‎src/cpp/cpp_convert_type.cpp

Lines changed: 7 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -588,19 +588,13 @@ void cpp_convert_typet::write(typet &type)
588588

589589
void cpp_convert_plain_type(typet &type)
590590
{
591-
if(type.id()==ID_cpp_name ||
592-
type.id()==ID_struct ||
593-
type.id()==ID_union ||
594-
type.id()==ID_array ||
595-
type.id()==ID_code ||
596-
type.id()==ID_unsignedbv ||
597-
type.id()==ID_signedbv ||
598-
type.id()==ID_bool ||
599-
type.id()==ID_floatbv ||
600-
type.id()==ID_empty ||
601-
type.id()==ID_symbol ||
602-
type.id()==ID_constructor ||
603-
type.id()==ID_destructor)
591+
if(
592+
type.id() == ID_cpp_name || type.id() == ID_struct ||
593+
type.id() == ID_union || type.id() == ID_array || type.id() == ID_code ||
594+
type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
595+
type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty ||
596+
type.id() == ID_symbol_type || type.id() == ID_constructor ||
597+
type.id() == ID_destructor)
604598
{
605599
}
606600
else if(type.id()==ID_c_enum)

0 commit comments

Comments
 (0)