From f93deec812fc52c5dc3e7d4fc77f39a35e76e671 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 18 May 2018 16:08:39 +0100 Subject: [PATCH 1/3] type symbols now use ID_symbol_type --- .../java_bytecode/ci_lazy_methods_needed.cpp | 6 ++--- .../java_bytecode_convert_method.cpp | 8 +++--- .../java_bytecode_parse_tree.cpp | 2 +- .../java_bytecode/java_bytecode_parser.cpp | 2 +- .../java_bytecode_typecheck_type.cpp | 2 +- .../src/java_bytecode/java_object_factory.cpp | 4 +-- .../java_string_library_preprocess.cpp | 16 +++++------ jbmc/src/java_bytecode/java_types.cpp | 7 ++--- jbmc/src/java_bytecode/remove_instanceof.cpp | 2 +- .../src/java_bytecode/select_pointer_type.cpp | 2 +- jbmc/unit/java-testing-utils/require_type.cpp | 2 +- .../mutually_recursive_generics.cpp | 4 +-- src/analyses/invariant_propagation.cpp | 2 +- src/analyses/uncaught_exceptions_analysis.cpp | 7 +++-- src/ansi-c/c_typecast.cpp | 8 +++--- src/ansi-c/c_typecheck_base.cpp | 2 +- src/ansi-c/c_typecheck_code.cpp | 2 +- src/ansi-c/c_typecheck_expr.cpp | 8 +++--- src/ansi-c/c_typecheck_initializer.cpp | 2 +- src/ansi-c/c_typecheck_type.cpp | 2 +- src/ansi-c/expr2c.cpp | 2 +- src/ansi-c/padding.cpp | 4 +-- src/ansi-c/type2name.cpp | 7 +++-- src/cpp/cpp_convert_type.cpp | 20 +++++--------- src/cpp/cpp_declarator_converter.cpp | 5 ++-- src/cpp/cpp_exception_id.cpp | 2 +- src/cpp/cpp_instantiate_template.cpp | 6 ++--- src/cpp/cpp_is_pod.cpp | 2 +- src/cpp/cpp_typecheck_bases.cpp | 2 +- src/cpp/cpp_typecheck_compound_type.cpp | 6 ++--- src/cpp/cpp_typecheck_constructor.cpp | 18 ++++++------- src/cpp/cpp_typecheck_destructor.cpp | 2 +- src/cpp/cpp_typecheck_expr.cpp | 5 ++-- src/cpp/cpp_typecheck_resolve.cpp | 13 ++++----- src/cpp/cpp_typecheck_template.cpp | 6 ++--- src/cpp/cpp_typecheck_type.cpp | 2 +- src/cpp/expr2cpp.cpp | 2 +- src/cpp/template_map.cpp | 2 +- src/goto-instrument/dump_c.cpp | 9 +++---- src/goto-instrument/goto_program2code.cpp | 6 ++--- src/goto-programs/destructor.cpp | 2 +- src/goto-programs/interpreter.cpp | 3 ++- src/goto-programs/string_abstraction.h | 2 +- src/goto-symex/goto_symex_state.cpp | 4 +-- src/linking/linking.cpp | 16 +++++------ .../refinement/string_refinement_util.cpp | 2 +- src/util/base_type.cpp | 27 +++++++++---------- src/util/endianness_map.cpp | 2 +- src/util/expr_initializer.cpp | 2 +- src/util/find_symbols.cpp | 2 +- src/util/format_type.cpp | 2 +- src/util/irep_ids.def | 1 + src/util/json_expr.cpp | 2 +- src/util/namespace.cpp | 4 +-- src/util/pointer_offset_size.cpp | 4 +-- src/util/replace_symbol.cpp | 4 +-- src/util/std_types.h | 8 +++--- src/util/type.cpp | 2 +- src/util/type_eq.cpp | 4 +-- src/util/xml_expr.cpp | 2 +- 60 files changed, 149 insertions(+), 157 deletions(-) diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index b1467c205c0..c3972be4c2f 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -112,7 +112,7 @@ void ci_lazy_methods_neededt::gather_field_types( { // If class_type is not a symbol this may be a reference array, // but we can't tell what type. - if(class_type.id() == ID_symbol) + if(class_type.id() == ID_symbol_type) { const typet &element_type = java_array_element_type(to_symbol_type(class_type)); @@ -127,11 +127,11 @@ void ci_lazy_methods_neededt::gather_field_types( { for(const auto &field : underlying_type.components()) { - if(field.type().id() == ID_struct || field.type().id() == ID_symbol) + if(field.type().id() == ID_struct || field.type().id() == ID_symbol_type) gather_field_types(field.type(), ns); else if(field.type().id() == ID_pointer) { - if(field.type().subtype().id() == ID_symbol) + if(field.type().subtype().id() == ID_symbol_type) { add_all_needed_classes(to_pointer_type(field.type())); } diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 21cac212cd4..db7d8e4536d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1633,7 +1633,7 @@ codet java_bytecode_convert_methodt::convert_instructions( const typecast_exprt pointer(op[0], java_array_type(statement[0])); dereference_exprt array(pointer, pointer.type().subtype()); - assert(pointer.type().subtype().id()==ID_symbol); + assert(pointer.type().subtype().id() == ID_symbol_type); array.set(ID_java_member_access, true); const member_exprt length(array, "length", java_int_type()); @@ -2562,7 +2562,7 @@ codet java_bytecode_convert_methodt::convert_putstatic( const exprt::operandst &op, const symbol_exprt &symbol_expr) { - if(needed_lazy_methods && arg0.type().id() == ID_symbol) + if(needed_lazy_methods && arg0.type().id() == ID_symbol_type) { needed_lazy_methods->add_needed_class( to_symbol_type(arg0.type()).get_identifier()); @@ -2612,7 +2612,7 @@ void java_bytecode_convert_methodt::convert_getstatic( { if(needed_lazy_methods) { - if(arg0.type().id() == ID_symbol) + if(arg0.type().id() == ID_symbol_type) { needed_lazy_methods->add_needed_class( to_symbol_type(arg0.type()).get_identifier()); @@ -2620,7 +2620,7 @@ void java_bytecode_convert_methodt::convert_getstatic( else if(arg0.type().id() == ID_pointer) { const auto &pointer_type = to_pointer_type(arg0.type()); - if(pointer_type.subtype().id() == ID_symbol) + if(pointer_type.subtype().id() == ID_symbol_type) { needed_lazy_methods->add_needed_class( to_symbol_type(pointer_type.subtype()).get_identifier()); diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp index 75698dc0d31..903024e91ae 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -117,7 +117,7 @@ java_bytecode_parse_treet::find_annotation( if(annotation.type.id() != ID_pointer) return false; const typet &type = annotation.type.subtype(); - return type.id() == ID_symbol && + return type.id() == ID_symbol_type && to_symbol_type(type).get_identifier() == annotation_type_name; }); if(annotation_it == annotations.end()) diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index ef41a7366f4..40b46bcd346 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -616,7 +616,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src) for(const auto &p : ct.parameters()) get_class_refs_rec(p.type()); } - else if(src.id()==ID_symbol) + else if(src.id()==ID_symbol_type) { irep_idt name=src.get(ID_C_base_name); if(has_prefix(id2string(name), "array[")) diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp index 2f26feb59bc..ecfb83a47ca 100644 --- a/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com void java_bytecode_typecheckt::typecheck_type(typet &type) { - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) { irep_idt identifier=to_symbol_type(type).get_identifier(); diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index d9461898a10..7007def5165 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -1179,7 +1179,7 @@ void java_object_factoryt::gen_nondet_init( if(is_sub) { const typet &symbol = override_ ? override_type : expr.type(); - PRECONDITION(symbol.id() == ID_symbol); + PRECONDITION(symbol.id() == ID_symbol_type); generic_parameter_specialization_map_keys.insert_pairs_for_symbol( to_symbol_type(symbol), struct_type); } @@ -1286,7 +1286,7 @@ void java_object_factoryt::gen_nondet_array_init( const source_locationt &location) { PRECONDITION(expr.type().id()==ID_pointer); - PRECONDITION(expr.type().subtype().id()==ID_symbol); + PRECONDITION(expr.type().subtype().id() == ID_symbol_type); PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE); const typet &type=ns.follow(expr.type().subtype()); diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index e7c8c8058c7..d6fa7bfdaca 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -36,7 +36,7 @@ Date: April 2017 irep_idt get_tag(const typet &type) { /// \todo Use follow instead of assuming tag to symbol relationship. - if(type.id() == ID_symbol) + if(type.id() == ID_symbol_type) return to_symbol_type(type).get_identifier(); else if(type.id() == ID_struct) return irep_idt("java::" + id2string(to_struct_type(type).get_tag())); @@ -394,11 +394,11 @@ java_string_library_preprocesst::process_equals_function_operands( /// \return type of the "data" component static typet get_data_type(const typet &type, const symbol_tablet &symbol_table) { - PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol); - if(type.id()==ID_symbol) + PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type); + if(type.id() == ID_symbol_type) { symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier()); - CHECK_RETURN(sym.type.id()!=ID_symbol); + CHECK_RETURN(sym.type.id() != ID_symbol_type); return get_data_type(sym.type, symbol_table); } // else type id is ID_struct @@ -413,11 +413,11 @@ static typet get_data_type(const typet &type, const symbol_tablet &symbol_table) static typet get_length_type(const typet &type, const symbol_tablet &symbol_table) { - PRECONDITION(type.id()==ID_struct || type.id()==ID_symbol); - if(type.id()==ID_symbol) + PRECONDITION(type.id() == ID_struct || type.id() == ID_symbol_type); + if(type.id() == ID_symbol_type) { symbolt sym=*symbol_table.lookup(to_symbol_type(type).get_identifier()); - CHECK_RETURN(sym.type.id()!=ID_symbol); + CHECK_RETURN(sym.type.id() != ID_symbol_type); return get_length_type(sym.type, symbol_table); } // else type id is ID_struct @@ -892,7 +892,7 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr( PRECONDITION(implements_java_char_sequence_pointer(rhs.type())); typet deref_type; - if(rhs.type().subtype().id()==ID_symbol) + if(rhs.type().subtype().id() == ID_symbol_type) deref_type=symbol_table.lookup_ref( to_symbol_type(rhs.type().subtype()).get_identifier()).type; else diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index 67e3a27e971..2d775c05293 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -777,7 +777,8 @@ bool equal_java_types(const typet &type1, const typet &type2) bool arrays_with_same_element_type = true; if( type1.id() == ID_pointer && type2.id() == ID_pointer && - type1.subtype().id() == ID_symbol && type2.subtype().id() == ID_symbol) + type1.subtype().id() == ID_symbol_type && + type2.subtype().id() == ID_symbol_type) { const symbol_typet &subtype_symbol1 = to_symbol_type(type1.subtype()); const symbol_typet &subtype_symbol2 = to_symbol_type(type2.subtype()); @@ -824,7 +825,7 @@ void get_dependencies_from_generic_parameters_rec( } // symbol type - else if(t.id() == ID_symbol) + else if(t.id() == ID_symbol_type) { const symbol_typet &symbol_type = to_symbol_type(t); const irep_idt class_name(symbol_type.get_identifier()); @@ -958,7 +959,7 @@ std::string pretty_java_type(const typet &type) return "byte"; else if(is_reference(type)) { - if(type.subtype().id() == ID_symbol) + if(type.subtype().id() == ID_symbol_type) { const auto &symbol_type = to_symbol_type(type.subtype()); const irep_idt &id = symbol_type.get_identifier(); diff --git a/jbmc/src/java_bytecode/remove_instanceof.cpp b/jbmc/src/java_bytecode/remove_instanceof.cpp index d980983bf41..dbacbac4a04 100644 --- a/jbmc/src/java_bytecode/remove_instanceof.cpp +++ b/jbmc/src/java_bytecode/remove_instanceof.cpp @@ -85,7 +85,7 @@ bool remove_instanceoft::lower_instanceof( // Find all types we know about that satisfy the given requirement: INVARIANT( - target_type.id()==ID_symbol, + target_type.id() == ID_symbol_type, "instanceof second operand should have a simple type"); const irep_idt &target_name= to_symbol_type(target_type).get_identifier(); diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index 6059b1e5084..e9b69ba002a 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -108,7 +108,7 @@ pointer_typet select_pointer_typet::specialize_generics( visited_nodes.erase(parameter_name); return returned_type; } - else if(pointer_type.subtype().id() == ID_symbol) + else if(pointer_type.subtype().id() == ID_symbol_type) { // if the pointer is an array, recursively specialize its element type const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype()); diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 77d09d02bc8..a3079048a33 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -427,7 +427,7 @@ require_type::require_complete_java_non_generic_class(const typet &class_type) const symbol_typet & require_type::require_symbol(const typet &type, const irep_idt &identifier) { - REQUIRE(type.id() == ID_symbol); + REQUIRE(type.id() == ID_symbol_type); const symbol_typet &result = to_symbol_type(type); if(identifier != "") { diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp index 98dc10b63ed..296e2ffaf11 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp @@ -63,7 +63,7 @@ SCENARIO( next.type(), {{require_type::type_argument_kindt::Var, "java::KeyValue::K"}, {require_type::type_argument_kindt::Var, "java::KeyValue::V"}}); - REQUIRE(next_type.subtype().id() == ID_symbol); + REQUIRE(next_type.subtype().id() == ID_symbol_type); const symbol_typet &next_symbol = to_symbol_type(next_type.subtype()); REQUIRE( symbol_table.lookup_ref(next_symbol.get_identifier()).name == @@ -75,7 +75,7 @@ SCENARIO( reverse.type(), {{require_type::type_argument_kindt::Var, "java::KeyValue::V"}, {require_type::type_argument_kindt::Var, "java::KeyValue::K"}}); - REQUIRE(next_type.subtype().id() == ID_symbol); + REQUIRE(next_type.subtype().id() == ID_symbol_type); const symbol_typet &reverse_symbol = to_symbol_type(reverse_type.subtype()); REQUIRE( symbol_table.lookup_ref(next_symbol.get_identifier()).name == diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index e89a21529e7..8bcd917a6bf 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -189,7 +189,7 @@ bool invariant_propagationt::check_type(const typet &type) const return false; else if(type.id()==ID_array) return false; - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) return check_type(ns.follow(type)); else if(type.id()==ID_unsignedbv || type.id()==ID_signedbv) diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp index 21e4c47ec67..e41f93dae4e 100644 --- a/src/analyses/uncaught_exceptions_analysis.cpp +++ b/src/analyses/uncaught_exceptions_analysis.cpp @@ -19,11 +19,10 @@ irep_idt uncaught_exceptions_domaint::get_exception_type(const typet &type) { PRECONDITION(type.id()==ID_pointer); - if(type.subtype().id()==ID_symbol) - { + if(type.subtype().id() == ID_symbol_type) return to_symbol_type(type.subtype()).get_identifier(); - } - return ID_empty; + else + return ID_empty; } /// Returns the symbol corresponding to an exception diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index b0f3aeda819..746a01cb834 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -253,7 +253,8 @@ bool check_c_implicit_typecast( typet c_typecastt::follow_with_qualifiers(const typet &src_type) { if( - src_type.id() != ID_symbol && src_type.id() != ID_struct_tag && + src_type.id() != ID_symbol_type && + src_type.id() != ID_struct_tag && src_type.id() != ID_union_tag) { return src_type; @@ -264,7 +265,8 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type) // collect qualifiers c_qualifierst qualifiers(src_type); - while(result_type.id() == ID_symbol || result_type.id() == ID_struct_tag || + while(result_type.id() == ID_symbol_type || + result_type.id() == ID_struct_tag || result_type.id() == ID_union_tag) { const typet &followed_type = ns.follow(result_type); @@ -348,7 +350,7 @@ c_typecastt::c_typet c_typecastt::get_c_type( { return INT; } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) return get_c_type(ns.follow(type)); else if(type.id()==ID_rational) return RATIONAL; diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index ee120fe00fd..8b158712237 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -406,7 +406,7 @@ void c_typecheck_baset::typecheck_redefinition_non_type( final_old.subtype()==final_new.subtype()) { // we don't do symbol types for arrays anymore - PRECONDITION(old_symbol.type.id()!=ID_symbol); + PRECONDITION(old_symbol.type.id() != ID_symbol_type); old_symbol.type=new_symbol.type; } else if((final_old.id()==ID_incomplete_c_enum || diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index be2d711416d..0ce2899c793 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -383,7 +383,7 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const } else if(type.id()==ID_vector) return is_complete_type(type.subtype()); - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) return is_complete_type(follow(type)); return true; diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b8b0e7fe595..d30aa74e270 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -91,9 +91,9 @@ bool c_typecheck_baset::gcc_types_compatible_p( // read // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html - if(type1.id()==ID_symbol) + if(type1.id() == ID_symbol_type) return gcc_types_compatible_p(follow(type1), type2); - else if(type2.id()==ID_symbol) + else if(type2.id() == ID_symbol_type) return gcc_types_compatible_p(type1, follow(type2)); // check qualifiers first @@ -3067,8 +3067,8 @@ void c_typecheck_baset::typecheck_arithmetic_pointer(const exprt &expr) typet subtype=type.subtype(); - if(subtype.id()==ID_symbol) - subtype=follow(subtype); + if(subtype.id() == ID_symbol_type) + subtype = follow(to_symbol_type(subtype)); if(subtype.id()==ID_incomplete_struct) { diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 977ad82f43f..2444b6201b1 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -492,7 +492,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( const typet &type=designator.back().subtype; const typet &full_type=follow(type); - assert(full_type.id()!=ID_symbol); + assert(full_type.id() != ID_symbol_type); // do we initialize a scalar? if(full_type.id()!=ID_struct && diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index c6767fb40e1..ad092c42e42 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -89,7 +89,7 @@ void c_typecheck_baset::typecheck_type(typet &type) typecheck_c_bit_field_type(to_c_bit_field_type(type)); else if(type.id()==ID_typeof) typecheck_typeof_type(type); - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) typecheck_symbol_type(to_symbol_type(type)); else if(type.id() == ID_typedef_type) typecheck_typedef_type(type); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 80b5515dd0f..c1327cdd807 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -457,7 +457,7 @@ std::string expr2ct::convert_rec( return convert_rec( src.subtype(), qualifiers, declarator+"[]"); } - else if(src.id()==ID_symbol) + else if(src.id() == ID_symbol_type) { symbol_typet symbolic_type=to_symbol_type(src); const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef); diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index 78489fde8ab..ba4771f97ba 100644 --- a/src/ansi-c/padding.cpp +++ b/src/ansi-c/padding.cpp @@ -86,8 +86,8 @@ mp_integer alignment(const typet &type, const namespacet &ns) result = alignment(ns.follow_tag(to_struct_tag_type(type)), ns); else if(type.id() == ID_union_tag) result = alignment(ns.follow_tag(to_union_tag_type(type)), ns); - else if(type.id()==ID_symbol) - result=alignment(ns.follow(type), ns); + else if(type.id() == ID_symbol_type) + result = alignment(ns.follow(to_symbol_type(type)), ns); else if(type.id()==ID_c_bit_field) { // we align these according to the 'underlying type' diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index b17d92752fe..87789b6c457 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -187,10 +187,9 @@ static std::string type2name( else result+="ARR"+integer2string(size); } - else if(type.id()==ID_symbol || - type.id()==ID_c_enum_tag || - type.id()==ID_struct_tag || - type.id()==ID_union_tag) + else if( + type.id() == ID_symbol_type || type.id() == ID_c_enum_tag || + type.id() == ID_struct_tag || type.id() == ID_union_tag) { parent_is_sym_check=true; result+=type2name_symbol(type, ns, symbol_number); diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp index e3dcadddea7..3f0b445fc59 100644 --- a/src/cpp/cpp_convert_type.cpp +++ b/src/cpp/cpp_convert_type.cpp @@ -588,19 +588,13 @@ void cpp_convert_typet::write(typet &type) void cpp_convert_plain_type(typet &type) { - if(type.id()==ID_cpp_name || - type.id()==ID_struct || - type.id()==ID_union || - type.id()==ID_array || - type.id()==ID_code || - type.id()==ID_unsignedbv || - type.id()==ID_signedbv || - type.id()==ID_bool || - type.id()==ID_floatbv || - type.id()==ID_empty || - type.id()==ID_symbol || - type.id()==ID_constructor || - type.id()==ID_destructor) + if( + type.id() == ID_cpp_name || type.id() == ID_struct || + type.id() == ID_union || type.id() == ID_array || type.id() == ID_code || + type.id() == ID_unsignedbv || type.id() == ID_signedbv || + type.id() == ID_bool || type.id() == ID_floatbv || type.id() == ID_empty || + type.id() == ID_symbol_type || type.id() == ID_constructor || + type.id() == ID_destructor) { } else if(type.id()==ID_c_enum) diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index 880d05fe2ef..800faa07aa6 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -141,8 +141,9 @@ symbolt &cpp_declarator_convertert::convert( cpp_typecheck_resolvet::wantt::TYPE, cpp_typecheck_fargst()); - if(symbol_expr.id()!=ID_type || - symbol_expr.type().id()!=ID_symbol) + if( + symbol_expr.id() != ID_type || + symbol_expr.type().id() != ID_symbol_type) { cpp_typecheck.error().source_location=name.source_location(); cpp_typecheck.error() << "error: expected type" diff --git a/src/cpp/cpp_exception_id.cpp b/src/cpp/cpp_exception_id.cpp index aef6606a4bd..f06f221f3c5 100644 --- a/src/cpp/cpp_exception_id.cpp +++ b/src/cpp/cpp_exception_id.cpp @@ -20,7 +20,7 @@ void cpp_exception_list_rec( const std::string &suffix, std::vector &dest) { - if(src.id()==ID_symbol) + if(src.id() == ID_symbol_type) { cpp_exception_list_rec(ns.follow(src), ns, suffix, dest); } diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index b47a864814e..93c6ee2e602 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -50,8 +50,8 @@ std::string cpp_typecheckt::template_suffix( if(expr.id()==ID_type) { const typet &type=expr.type(); - if(type.id()==ID_symbol) - result+=type.get_string(ID_identifier); + if(type.id() == ID_symbol_type) + result += id2string(to_symbol_type(type).get_identifier()); else result+=cpp_type2name(type); } @@ -190,7 +190,7 @@ const symbolt &cpp_typecheckt::class_template_symbol( void cpp_typecheckt::elaborate_class_template( const typet &type) { - if(type.id()!=ID_symbol) + if(type.id() != ID_symbol_type) return; const symbolt &symbol = lookup(to_symbol_type(type)); diff --git a/src/cpp/cpp_is_pod.cpp b/src/cpp/cpp_is_pod.cpp index 5ea145f505f..1f4ceee38a8 100644 --- a/src/cpp/cpp_is_pod.cpp +++ b/src/cpp/cpp_is_pod.cpp @@ -80,7 +80,7 @@ bool cpp_typecheckt::cpp_is_pod(const typet &type) const // but pointers are PODs! return true; } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) { const symbolt &symb = lookup(to_symbol_type(type)); DATA_INVARIANT(symb.is_type, "type symbol is a type"); diff --git a/src/cpp/cpp_typecheck_bases.cpp b/src/cpp/cpp_typecheck_bases.cpp index a9cabf3c112..6870a5cf3b1 100644 --- a/src/cpp/cpp_typecheck_bases.cpp +++ b/src/cpp/cpp_typecheck_bases.cpp @@ -44,7 +44,7 @@ void cpp_typecheckt::typecheck_compound_bases(struct_typet &type) // elaborate any class template instances given as bases elaborate_class_template(base_symbol_expr.type()); - if(base_symbol_expr.type().id()!=ID_symbol) + if(base_symbol_expr.type().id() != ID_symbol_type) { error().source_location=name.source_location(); error() << "expected type symbol as struct/class base" << eom; diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index f89ca87cc55..0422bcfffab 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -889,7 +889,7 @@ void cpp_typecheckt::typecheck_friend_declaration( // TODO // typecheck_type(ftype); - // assert(ftype.id()==ID_symbol); + // assert(ftype.id()==ID_symbol_type); // symbol.type.add("ID_C_friends").move_to_sub(ftype); return; @@ -1631,7 +1631,7 @@ void cpp_typecheckt::get_bases( forall_irep(it, bases) { assert(it->id()==ID_base); - assert(it->get(ID_type)==ID_symbol); + assert(it->get(ID_type) == ID_symbol_type); const struct_typet &base= to_struct_type(lookup(it->find(ID_type).get(ID_identifier)).type); @@ -1653,7 +1653,7 @@ void cpp_typecheckt::get_virtual_bases( forall_irep(it, bases) { assert(it->id()==ID_base); - assert(it->get(ID_type)==ID_symbol); + assert(it->get(ID_type) == ID_symbol_type); const struct_typet &base= to_struct_type(lookup(it->find(ID_type).get(ID_identifier)).type); diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp index b89b7460a39..d9d9ec2e3e3 100644 --- a/src/cpp/cpp_typecheck_constructor.cpp +++ b/src/cpp/cpp_typecheck_constructor.cpp @@ -252,7 +252,7 @@ void cpp_typecheckt::default_cpctor( forall_irep(parent_it, bases.get_sub()) { assert(parent_it->id()==ID_base); - assert(parent_it->get(ID_type)==ID_symbol); + assert(parent_it->get(ID_type) == ID_symbol_type); const symbolt &parsymb= lookup(parent_it->find(ID_type).get(ID_identifier)); @@ -367,7 +367,7 @@ void cpp_typecheckt::default_assignop( std::string arg_name("ref"); cpctor.add(ID_storage_spec).id(ID_cpp_storage_spec); - cpctor.type().id(ID_symbol); + cpctor.type().id(ID_symbol_type); cpctor.type().add(ID_identifier).id(symbol.name); cpctor.operands().push_back(exprt(ID_cpp_declarator)); cpctor.add_source_location()=source_location; @@ -447,7 +447,7 @@ void cpp_typecheckt::default_assignop_value( forall_irep(parent_it, bases.get_sub()) { assert(parent_it->id()==ID_base); - assert(parent_it->get(ID_type)==ID_symbol); + assert(parent_it->get(ID_type) == ID_symbol_type); const symbolt &symb= lookup(parent_it->find(ID_type).get(ID_identifier)); @@ -540,7 +540,7 @@ void cpp_typecheckt::check_member_initializers( bool ok=false; forall_irep(parent_it, bases.get_sub()) { - assert(parent_it->get(ID_type)==ID_symbol); + assert(parent_it->get(ID_type) == ID_symbol_type); if(member_type.get(ID_identifier) ==parent_it->find(ID_type).get(ID_identifier)) @@ -584,7 +584,7 @@ void cpp_typecheckt::check_member_initializers( if(c_it->get_bool("is_type")) { typet type=static_cast(c_it->find(ID_type)); - if(type.id()!=ID_symbol) + if(type.id() != ID_symbol_type) continue; const symbolt &symb=lookup(type.get(ID_identifier)); @@ -594,7 +594,7 @@ void cpp_typecheckt::check_member_initializers( // check for a direct parent forall_irep(parent_it, bases.get_sub()) { - assert(parent_it->get(ID_type)==ID_symbol); + assert(parent_it->get(ID_type) == ID_symbol_type); if(symb.name==parent_it->find(ID_type).get(ID_identifier)) { ok=true; @@ -617,7 +617,7 @@ void cpp_typecheckt::check_member_initializers( // check for a direct parent forall_irep(parent_it, bases.get_sub()) { - assert(parent_it->get(ID_type)==ID_symbol); + assert(parent_it->get(ID_type) == ID_symbol_type); if(member_type.get(ID_identifier)== parent_it->find(ID_type).get(ID_identifier)) @@ -711,7 +711,7 @@ void cpp_typecheckt::full_member_initialization( forall_irep(parent_it, bases.get_sub()) { assert(parent_it->id()==ID_base); - assert(parent_it->get(ID_type)==ID_symbol); + assert(parent_it->get(ID_type) == ID_symbol_type); const symbolt &ctorsymb= lookup(parent_it->find(ID_type).get(ID_identifier)); @@ -764,7 +764,7 @@ void cpp_typecheckt::full_member_initialization( typecheck_type(member_type); - if(member_type.id()!=ID_symbol) + if(member_type.id() != ID_symbol_type) break; if(parent_it->find(ID_type).get(ID_identifier)== diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index 193dede0a8f..8f66277be04 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -160,7 +160,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol) bit++) { assert(bit->id()==ID_base); - assert(bit->find(ID_type).id()==ID_symbol); + assert(bit->find(ID_type).id() == ID_symbol_type); const symbolt &psymb = lookup(bit->find(ID_type).get(ID_identifier)); symbol_exprt this_ptr(ID_this, pointer_type(symbol.type)); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 2ffd3524407..9cb17f46b33 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -605,8 +605,9 @@ bool cpp_typecheckt::operator_is_overloaded(exprt &expr) // TODO: need to resolve an incomplete struct (template) here // go into scope of first operand - if(expr.op0().type().id()==ID_symbol && - follow(expr.op0().type()).id()==ID_struct) + if( + expr.op0().type().id() == ID_symbol_type && + follow(expr.op0().type()).id() == ID_struct) { const irep_idt &struct_identifier= expr.op0().type().get(ID_identifier); diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 484fc458712..42c0ac58ed4 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -174,7 +174,7 @@ void cpp_typecheck_resolvet::remove_duplicates( if(it->id()==ID_symbol) id = to_symbol_expr(*it).get_identifier(); - else if(it->id()==ID_type && it->type().id()==ID_symbol) + else if(it->id() == ID_type && it->type().id() == ID_symbol_type) id = to_symbol_type(it->type()).get_identifier(); if(id=="") @@ -362,7 +362,7 @@ exprt cpp_typecheck_resolvet::convert_identifier( typet followed_type=symbol.type; bool constant=followed_type.get_bool(ID_C_constant); - while(followed_type.id()==ID_symbol) + while(followed_type.id() == ID_symbol_type) { followed_type = cpp_typecheck.follow(to_symbol_type(followed_type)); @@ -2285,7 +2285,8 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( assert(pcomp.get_bool(ID_is_type)); const typet &type=pcomp.type(); assert(type.id()!=ID_struct); - if(type.id()==ID_symbol) + + if(type.id() == ID_symbol_type) identifier = to_symbol_type(type).get_identifier(); else continue; @@ -2307,7 +2308,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( new_set.insert(&class_id); break; } - else if(symbol.type.id()==ID_symbol) + else if(symbol.type.id() == ID_symbol_type) identifier = to_symbol_type(symbol.type).get_identifier(); else break; @@ -2350,7 +2351,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( if(e.id()!=ID_type) continue; // expressions are definitively not a scope - if(e.type().id()==ID_symbol) + if(e.type().id() == ID_symbol_type) { symbol_typet type=to_symbol_type(e.type()); @@ -2361,7 +2362,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes( const symbolt &symbol=cpp_typecheck.lookup(identifier); assert(symbol.is_type); - if(symbol.type.id()==ID_symbol) + if(symbol.type.id() == ID_symbol_type) type=to_symbol_type(symbol.type); else if(symbol.type.id()==ID_struct || symbol.type.id()==ID_incomplete_struct || diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index 052be288891..0281e0fea24 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -786,8 +786,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( // is it a type or not? if(declaration.get_bool(ID_is_type)) { - parameter=exprt(ID_type, typet(ID_symbol)); - parameter.type().set(ID_identifier, identifier); + parameter = exprt(ID_type, symbol_typet(identifier)); parameter.type().add_source_location()=declaration.find_source_location(); } else @@ -822,8 +821,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( if(cpp_declarator_converter.is_typedef) { - parameter=exprt(ID_type, typet(ID_symbol)); - parameter.type().set(ID_identifier, symbol.name); + parameter = exprt(ID_type, symbol_typet(symbol.name)); parameter.type().add_source_location()=declaration.find_location(); } else diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp index cb8dfe198ba..8bab226bde4 100644 --- a/src/cpp/cpp_typecheck_type.cpp +++ b/src/cpp/cpp_typecheck_type.cpp @@ -186,7 +186,7 @@ void cpp_typecheckt::typecheck_type(typet &type) type.id()==ID_empty) { } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) { } else if(type.id()==ID_constructor || diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 7d483bd1b05..24db086866a 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -187,7 +187,7 @@ std::string expr2cppt::convert_rec( else return expr2ct::convert_rec(src, qualifiers, declarator); } - else if(src.id()==ID_symbol) + else if(src.id() == ID_symbol_type) { const irep_idt &identifier= to_symbol_type(src).get_identifier(); diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp index 02d901e391f..28bbb632834 100644 --- a/src/cpp/template_map.cpp +++ b/src/cpp/template_map.cpp @@ -39,7 +39,7 @@ void template_mapt::apply(typet &type) const apply(subtype); } } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) { type_mapt::const_iterator m_it = type_map.find(to_symbol_type(type).get_identifier()); diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 2715f303063..baecc693418 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -61,8 +61,7 @@ void dump_ct::operator()(std::ostream &os) { typet &type=it2->type(); - if(type.id()==ID_symbol && - type.get_bool(ID_C_transparent_union)) + if(type.id() == ID_symbol_type && type.get_bool(ID_C_transparent_union)) { symbolt new_type_sym= ns.lookup(to_symbol_type(type).get_identifier()); @@ -314,7 +313,7 @@ void dump_ct::convert_compound( bool recursive, std::ostream &os) { - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) { const symbolt &symbol= ns.lookup(to_symbol_type(type).get_identifier()); @@ -382,7 +381,7 @@ void dump_ct::convert_compound( UNREACHABLE; /* assert(parent_it->id() == ID_base); - assert(parent_it->get(ID_type) == ID_symbol); + assert(parent_it->get(ID_type) == ID_symbol_type); const irep_idt &base_id= parent_it->find(ID_type).get(ID_identifier); @@ -669,7 +668,7 @@ void dump_ct::collect_typedefs_rec( { collect_typedefs_rec(type.subtype(), early, local_deps); } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) { const symbolt &symbol= ns.lookup(to_symbol_type(type).get_identifier()); diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 5f8a4b00c74..2a5f7304264 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1422,7 +1422,7 @@ goto_programt::const_targett goto_program2codet::convert_catch( void goto_program2codet::add_local_types(const typet &type) { - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) { const typet &full_type=ns.follow(type); @@ -1655,7 +1655,7 @@ void goto_program2codet::remove_const(typet &type) if(type.get_bool(ID_C_constant)) type.remove(ID_C_constant); - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) { const irep_idt &identifier=to_symbol_type(type).get_identifier(); if(!const_removed.insert(identifier).second) @@ -1861,7 +1861,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) if(no_typecast) return; - assert(expr.type().id()==ID_symbol); + assert(expr.type().id() == ID_symbol_type); const typet &t=expr.type(); diff --git a/src/goto-programs/destructor.cpp b/src/goto-programs/destructor.cpp index cc6b14c0d2b..db13c0ea3a5 100644 --- a/src/goto-programs/destructor.cpp +++ b/src/goto-programs/destructor.cpp @@ -19,7 +19,7 @@ code_function_callt get_destructor( const namespacet &ns, const typet &type) { - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) { return get_destructor(ns, ns.follow(type)); } diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 4ec0c2ac729..7136eec4509 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -1043,10 +1043,11 @@ mp_integer interpretert::get_size(const typet &type) } return subtype_size; } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) { return get_size(ns.follow(type)); } + return 1; } diff --git a/src/goto-programs/string_abstraction.h b/src/goto-programs/string_abstraction.h index c79ec5154fe..da78ecd3779 100644 --- a/src/goto-programs/string_abstraction.h +++ b/src/goto-programs/string_abstraction.h @@ -52,7 +52,7 @@ class string_abstractiont:public messaget bool is_char_type(const typet &type) const { - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) return is_char_type(ns.follow(type)); if(type.id()!=ID_signedbv && diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index e306a86d13d..1cc7de3e427 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -760,7 +760,7 @@ void goto_symex_statet::rename_address( // type might not have been renamed in case of nesting of // structs and pointers/arrays - if(member_expr.struct_op().type().id()!=ID_symbol) + if(member_expr.struct_op().type().id() != ID_symbol_type) { const struct_union_typet &su_type= to_struct_union_type(member_expr.struct_op().type()); @@ -843,7 +843,7 @@ void goto_symex_statet::rename( { rename(type.subtype(), irep_idt(), ns, level); } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) { const symbolt &symbol= ns.lookup(to_symbol_type(type).get_identifier()); diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 4e480e7570f..f39b1a9666e 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -44,7 +44,7 @@ static const typet &follow_tags_symbols( const namespacet &ns, const typet &type) { - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) return ns.follow(type); else if(type.id()==ID_c_enum_tag) return ns.follow_tag(to_c_enum_tag_type(type)); @@ -790,10 +790,9 @@ bool linkingt::adjust_object_type_rec( if(base_type_eq(t1, t2, ns)) return false; - if(t1.id()==ID_symbol || - t1.id()==ID_struct_tag || - t1.id()==ID_union_tag || - t1.id()==ID_c_enum_tag) + if( + t1.id() == ID_symbol_type || t1.id() == ID_struct_tag || + t1.id() == ID_union_tag || t1.id() == ID_c_enum_tag) { const irep_idt &identifier=t1.get(ID_identifier); @@ -808,10 +807,9 @@ bool linkingt::adjust_object_type_rec( return false; } - else if(t2.id()==ID_symbol || - t2.id()==ID_struct_tag || - t2.id()==ID_union_tag || - t2.id()==ID_c_enum_tag) + else if( + t2.id() == ID_symbol_type || t2.id() == ID_struct_tag || + t2.id() == ID_union_tag || t2.id() == ID_c_enum_tag) { const irep_idt &identifier=t2.get(ID_identifier); diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index 85ac59305f5..30ae4748ab9 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -36,7 +36,7 @@ bool is_char_type(const typet &type) bool is_char_array_type(const typet &type, const namespacet &ns) { - if(type.id() == ID_symbol) + if(type.id() == ID_symbol_type) return is_char_array_type(ns.follow(type), ns); return type.id() == ID_array && is_char_type(type.subtype()); } diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp index f999c4beef7..e26a4225cf1 100644 --- a/src/util/base_type.cpp +++ b/src/util/base_type.cpp @@ -53,7 +53,7 @@ class base_type_eqt void base_type_rec( typet &type, const namespacet &ns, std::set &symb) { - if(type.id() == ID_symbol) + if(type.id() == ID_symbol_type) { const symbolt *symbol; @@ -99,7 +99,7 @@ void base_type_rec( typet &subtype=to_pointer_type(type).subtype(); // we need to avoid running into an infinite loop - if(subtype.id() == ID_symbol) + if(subtype.id() == ID_symbol_type) { const irep_idt &id = to_symbol_type(subtype).get_identifier(); @@ -159,11 +159,10 @@ bool base_type_eqt::base_type_eq_rec( #endif // loop avoidance - if((type1.id()==ID_symbol || - type1.id()==ID_c_enum_tag || - type1.id()==ID_struct_tag || - type1.id()==ID_union_tag) && - type2.id()==type1.id()) + if( + (type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag || + type1.id() == ID_struct_tag || type1.id() == ID_union_tag) && + type2.id() == type1.id()) { // already in same set? if(identifiers.make_union( @@ -172,10 +171,9 @@ bool base_type_eqt::base_type_eq_rec( return true; } - if(type1.id()==ID_symbol || - type1.id()==ID_c_enum_tag || - type1.id()==ID_struct_tag || - type1.id()==ID_union_tag) + if( + type1.id() == ID_symbol_type || type1.id() == ID_c_enum_tag || + type1.id() == ID_struct_tag || type1.id() == ID_union_tag) { const symbolt &symbol= ns.lookup(type1.get(ID_identifier)); @@ -186,10 +184,9 @@ bool base_type_eqt::base_type_eq_rec( return base_type_eq_rec(symbol.type, type2); } - if(type2.id()==ID_symbol || - type2.id()==ID_c_enum_tag || - type2.id()==ID_struct_tag || - type2.id()==ID_union_tag) + if( + type2.id() == ID_symbol_type || type2.id() == ID_c_enum_tag || + type2.id() == ID_struct_tag || type2.id() == ID_union_tag) { const symbolt &symbol= ns.lookup(type2.get(ID_identifier)); diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp index 677f7b6b81e..bd0e54b8a6d 100644 --- a/src/util/endianness_map.cpp +++ b/src/util/endianness_map.cpp @@ -51,7 +51,7 @@ void endianness_mapt::build_little_endian(const typet &src) void endianness_mapt::build_big_endian(const typet &src) { - if(src.id()==ID_symbol) + if(src.id() == ID_symbol_type) build_big_endian(ns.follow(src)); else if(src.id()==ID_c_enum_tag) build_big_endian(ns.follow_tag(to_c_enum_tag_type(src))); diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 3d8ec337e32..16640b3382b 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -280,7 +280,7 @@ exprt expr_initializert::expr_initializer_rec( return value; } - else if(type_id==ID_symbol) + else if(type_id == ID_symbol_type) { exprt result = expr_initializer_rec(ns.follow(type), source_location); // we might have mangled the type for arrays, so keep that diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp index 2c6a596ba42..e379120960f 100644 --- a/src/util/find_symbols.cpp +++ b/src/util/find_symbols.cpp @@ -165,7 +165,7 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest) // dest.insert(identifier); } } - else if(src.id()==ID_symbol) + else if(src.id() == ID_symbol_type) dest.insert(to_symbol_type(src).get_identifier()); else if(src.id()==ID_array) { diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp index 8d54599598d..1e4bed98ead 100644 --- a/src/util/format_type.cpp +++ b/src/util/format_type.cpp @@ -51,7 +51,7 @@ std::ostream &format_rec(std::ostream &os, const typet &type) } else if(id == ID_struct) return format_rec(os, to_struct_type(type)); - else if(id == ID_symbol) + else if(id == ID_symbol_type) return os << "symbol_type " << to_symbol_type(type).get_identifier(); else return os << id; diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index d0066054482..95438d3fefd 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -58,6 +58,7 @@ IREP_ID_ONE(bitxnor) IREP_ID_ONE(notequal) IREP_ID_ONE(if) IREP_ID_ONE(symbol) +IREP_ID_ONE(symbol_type) IREP_ID_ONE(next_symbol) IREP_ID_ONE(nondet_symbol) IREP_ID_ONE(predicate_symbol) diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index 0e9147fe775..5c30ca16d9d 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -117,7 +117,7 @@ json_objectt json( const namespacet &ns, const irep_idt &mode) { - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) return json(ns.follow(type), ns, mode); json_objectt result; diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp index 04a6f260db8..76f0a8dbc40 100644 --- a/src/util/namespace.cpp +++ b/src/util/namespace.cpp @@ -60,7 +60,7 @@ const typet &namespace_baset::follow(const typet &src) const if(src.id() == ID_struct_tag) return follow_tag(to_struct_tag_type(src)); - if(src.id()!=ID_symbol) + if(src.id() != ID_symbol_type) return src; const symbolt *symbol = &lookup(to_symbol_type(src)); @@ -70,7 +70,7 @@ const typet &namespace_baset::follow(const typet &src) const { DATA_INVARIANT(symbol->is_type, "symbol type points to type"); - if(symbol->type.id() == ID_symbol) + if(symbol->type.id() == ID_symbol_type) symbol = &lookup(to_symbol_type(symbol->type)); else return symbol->type; diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 872e69a65fc..0035ba29fe7 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -234,7 +234,7 @@ mp_integer pointer_offset_bits( return to_bitvector_type(type).get_width(); } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) { return pointer_offset_bits(ns.follow(type), ns); } @@ -510,7 +510,7 @@ exprt size_of_expr( bytes++; return from_integer(bytes, size_type()); } - else if(type.id()==ID_symbol) + else if(type.id() == ID_symbol_type) { return size_of_expr(ns.follow(type), ns); } diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index e568758661f..91acab8de72 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -185,7 +185,7 @@ bool replace_symbolt::replace(typet &dest) const if(!replace(*it)) result=false; } - else if(dest.id()==ID_symbol) + else if(dest.id() == ID_symbol_type) { type_mapt::const_iterator it = type_map.find(to_symbol_type(dest).get_identifier()); @@ -250,7 +250,7 @@ bool replace_symbolt::have_to_replace(const typet &dest) const if(have_to_replace(*it)) return true; } - else if(dest.id()==ID_symbol) + else if(dest.id() == ID_symbol_type) { const irep_idt &identifier = to_symbol_type(dest).get_identifier(); return type_map.find(identifier) != type_map.end(); diff --git a/src/util/std_types.h b/src/util/std_types.h index 00f9566926b..39cb1b49b94 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -110,7 +110,7 @@ class real_typet:public typet class symbol_typet:public typet { public: - explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol) + explicit symbol_typet(const irep_idt &identifier) : typet(ID_symbol_type) { set_identifier(identifier); } @@ -138,7 +138,7 @@ class symbol_typet:public typet */ inline const symbol_typet &to_symbol_type(const typet &type) { - PRECONDITION(type.id()==ID_symbol); + PRECONDITION(type.id() == ID_symbol_type); return static_cast(type); } @@ -147,14 +147,14 @@ inline const symbol_typet &to_symbol_type(const typet &type) */ inline symbol_typet &to_symbol_type(typet &type) { - PRECONDITION(type.id()==ID_symbol); + PRECONDITION(type.id() == ID_symbol_type); return static_cast(type); } template <> inline bool can_cast_type(const typet &type) { - return type.id() == ID_symbol; + return type.id() == ID_symbol_type; } /*! \brief Base type of C structs and unions, and C++ classes diff --git a/src/util/type.cpp b/src/util/type.cpp index a83e5576717..2a235c2d652 100644 --- a/src/util/type.cpp +++ b/src/util/type.cpp @@ -87,7 +87,7 @@ bool is_constant_or_has_constant_components( // we have to use the namespace to resolve to its definition: // struct t { const int a; }; // struct t t1; - if(type.id() == ID_symbol) + if(type.id() == ID_symbol_type) { const auto &resolved_type = ns.follow(type); return has_constant_components(resolved_type); diff --git a/src/util/type_eq.cpp b/src/util/type_eq.cpp index 5fc587f58e3..5a4e4585d94 100644 --- a/src/util/type_eq.cpp +++ b/src/util/type_eq.cpp @@ -20,7 +20,7 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns) if(type1==type2) return true; - if(type1.id()==ID_symbol) + if(type1.id() == ID_symbol_type) { const symbolt &symbol = ns.lookup(to_symbol_type(type1)); if(!symbol.is_type) @@ -29,7 +29,7 @@ bool type_eq(const typet &type1, const typet &type2, const namespacet &ns) return type_eq(symbol.type, type2, ns); } - if(type2.id()==ID_symbol) + if(type2.id() == ID_symbol_type) { const symbolt &symbol = ns.lookup(to_symbol_type(type2)); if(!symbol.is_type) diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp index 319a463b914..56176a88e57 100644 --- a/src/util/xml_expr.cpp +++ b/src/util/xml_expr.cpp @@ -51,7 +51,7 @@ xmlt xml( const typet &type, const namespacet &ns) { - if(type.id()==ID_symbol) + if(type.id() == ID_symbol_type) return xml(ns.follow(type), ns); xmlt result; From 617890831c393a4f4999808f0295efb68cd9483b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 30 Jul 2018 08:57:40 +0100 Subject: [PATCH 2/3] bump goto binary version --- .../ansi-c/arch_flags_mcpu_bad/object.intel | Bin 4454 -> 4335 bytes .../ansi-c/arch_flags_mcpu_good/object.arm | Bin 4183 -> 4062 bytes .../ansi-c/arch_flags_mthumb_good/object.arm | Bin 4185 -> 4120 bytes regression/goto-diff/syntactic-diff1/a.gb | Bin 5839 -> 5738 bytes regression/goto-diff/syntactic-diff1/b.gb | Bin 5936 -> 5830 bytes src/goto-programs/read_bin_goto_object.cpp | 9 +++++---- src/goto-programs/write_goto_binary.cpp | 13 ++++++------- src/goto-programs/write_goto_binary.h | 2 +- 8 files changed, 12 insertions(+), 12 deletions(-) diff --git a/regression/ansi-c/arch_flags_mcpu_bad/object.intel b/regression/ansi-c/arch_flags_mcpu_bad/object.intel index 11593f7dcf173d5b37e0ea5e851e403068c6528c..0ddb17184a5f40df69373225165716361ffdeb00 100644 GIT binary patch literal 4335 zcmbtY{dW{s8NPQH%FY%Ci;5UjViViiHcd7uDYZ!3jPy$!8b+`m+F>$tH<@O4W|^5K z34SyQX_5s(2w&PlzhY}^{Z+(M>(L&6^#}h2{Y^dtp#&PRK6mbHcD6kme<0_;Ih&b% zp67ku_rC9Y^U~uTk1c5=b*5`EqF$sP3yPkj2LlC0=rZ5#c9_+*i>N1PpKS#_BrzYtbNxn8gBbnBMwF*9(z0h0PS z)!gIeS#z)FG6&C^3!dBUHJe>|v#Hw-nmyL-G2aJ#v*Gx5li6%|W{;lD8Qs2~Hw#6* z%djAaNUx_&H(vlfKHf5x?lL@5ie!+n^mJ0e|D-;hEw~7hc|^N)87x^oCap&>|4uZR zuHy#=;$I49zA%z7dw>A>C#ZZm)qX#Zcm)Fd;(w$KT}3+=*iI9dVh0GN=&>e0@Sxw{ z$Rob(H7NsFgq$K|!}E**qOA%g zay>+~e0w(|UsYl+ujY?sJpS6jasqQM{Ef2MvCGI68L9hJYPp%8Oor#1s2yuArTW*m z>ya1AhqNIl7?u+4>x!COt#*9lmGsR}@$Yh~#Cp<0E9n4N2FPr?+m|zGlQ$&NvX&c?KsI>}lcXM^sM_(Z_ZK%H!$}qScAi~zWy3Kk(;nqc`3r66 zGJHlFN2Cl_cKduSC3%)dLF;aTd4^-@VX{i;c?g^5!oDq}+_7hIDPjDIe5a6d*C8o` z!VAj?QX0vfS8LJt@p9Dz-S+h&&Iv#B@Z~D#uX6hD2>QD}T7(`pMD+Iv`g;#Z88nIt z{XJLyAHC=>rSugLU*W_}g806VYZ41uk%DGH+_GQdHCG{SzFdnqtar;TcIB8}Ccg~w z%bYwT$Xowjle{Hj=lO3F7ny z+ng%539%Y1N5lN#M56ply*&Lab%xqb)^_Y*06lrNB5#3&r>~^M5NzU8(6Vek|HbHQ z533VWw~)?+W9JCjvNxtpv`J{$3oUyk(z?~uv?bhXWZC-B3=KK9aSnCm_LrpxqT~Z` z8|mCO8iNXYJZ4zF&iXNfdAAz{padE*Rw<0)y{RDWc5M22NzLEHUO%mC49wj*k5eseGPv?wCuJ(sLYyw~t0Q0k20I;F}yZ5tTMY0QEJ_jpK#=!Dns1>+L zz)b?KFRR@eR;b)Bf*p86%9N)M+5G|4epavj{5X!-FHEdf)-QpMo$aNeo7>qk;bw&W zaFEWXu#UfZK z@liS*L-yPvss<}~o?pgF>1kk1qsG^cM_8!DQY3PWR!~ZGxRyP<+WA_yn|Uq}hhfw( zjMDbfb&eabokb%@w0#w+`y;7$RnWDG@?*4cO_A}+etI}2JE|zKIIIs#HNSk6(uX1b zFpM}rc^gWgtxVF%O6L=|jDvKIHdTgKA zI$Vrj;i#`hsK@CarMB{t$#1+TC@)()?tGP=iXrmRXJd-u@>NQo0^li$)V~&4B5oR! z_|oeU?uf|he5@~*Z){kL#30p++&kP3(4FT~DB(9E1F==S$#GD^QLpD)|C{u5Oixwu z#uu&A&~}>FEx-CE-=cNebOiewI=<);#}XWF7jJX!Wt@9;w&fG+jCbh{@wW$VB(TQPZ`0-PaSfW<@jLn_8hE&l;^$NRtRSS5zd+xk h;xnb>eLyFFPwR*}NNo!{i=DM`Q-4Q5Nq7@E`X5G!zlZ<; literal 4454 zcmbtYZFCe@8NPS7X|j{h)r4vZ)M1G%I%*k7Z;`HShq3c;T=k$?SxY0KAR+1?h zGpRbdX^;RRa&1b_FcSP{Xk8+&XPhS8Xi_yz=il2=d|#K*4My&mky_jEuisbnnAQ&6 zNGqCdv7}>KeWct)wz) z+E%j3TwY128o@`t63nTVnq>~NY;q?7*8r&u7e?0s(L6Oeu)4Mc-3t5-j##PssI+k+tozw+NoypjNCQ2tYwK$1mAHjVYvK( z{-`jR`wJIz2kzx9)?_;t>=agiaIdt+HMxSsenT4*s?A94Yf=O#Bs?4~=`Tl6lHIDM z2$l2E;ppYyaFn#vh4QexaT~R!peB(2yGiB8#cvw_B(;mKs36zNgl5$YdQ9QJfz<1edR-zdRi6-2 zS55m%b%hG4_Y0}DB}4C@@KdRo`9y|!5+@*W0umoc=S)av7KwjyeJuQ-VEw7TNbO#k z?F&l0NtTmOgWLmh*Jl=}ylwMl6x@S1%N4OKT3yL7bq5sPgrb{VQIk-#deUD}i;%<% zrCBIyIVeTYiX~mmQ+~R7+}bYXZVJMtAgn4P0^bu0w+hgjd@B4M-6$&)kxAGk(-l zdN0$Ilxbl&n<|H$0qq&?NL0YCiiIB$u>pJ%FN zseL5A$%Tc@T|`c~P51?fc!ED&j;EVPic`MGjfd;{;v3Q1O}iz(kGNwRK=R*1I5YFT zyyUkC&mI=_^Db@7h?7Gi@h3Sax$8?8|G%*AV1)Wj__H+~-{ks6w#@k@#k7&#IpkoD zXE!dg`_%ECeqc$-l3^g!diy^HD0pA>wB8!?rIpL=uD<-L#W0q=Y#WUgrgq+~ss3QDbv2a2_ zCts8n&7Z`OA9BJpGhUYs0dNR_S~|`!`cuM^^dF^mZ}fVjzZ)?%jDC{3R%TJ*5Hl0o zv8kYDuEC*e+#y|1d@2^+E-3C8ks@f}lHJ=+`f+52rmKd5h6dtEa6HLHX9OZ%n{%n0iKnP+c44* zM&{p>+R+k1vS;K@gtWMk&ebv_HNNzCHeQ8|SGkQn9=~3}udsn|YP|z~)XF!R0Zr?2aM1_P3$EWjT!S;XNS4FP!9MbQe@$t-$>}+UQJQ!Aw7=$Zu)l`1 z?5^MyMaTruqio{!#uGdH+1-z)qa^{|%*!NM0S71v%m=4Vb}+wp2)3`>fQJN#;a{C+wnMZ5v` zF6G0&FtEw1^pu|(zT~4zPC>*ei1-mm@0L@q(f`om4ghMCxPI_0{5&i_&n^FP!E!Y9!2;`_(4$go5zbwy4$?DzT=~wZAfLOK zWdipMIG+LM`zjl5h32ETLYITLLgbZq0*7ci{!@xRI$R*#Pp?SrUU7PzG{E^BqP&+5 z(}gk#XePc}tAhUm_%DF}5qL95c^kxVzz@;E(t1@~CsM;O&h=}g5PFpUPHHPoZTN-f zl_T_0SuioHq306fT#`uZvay0s=&tbs%mf{;?kK{zK8@3f>QZl6Xe*81n6vzHJ|CT^ z#&TXwIwxs8ZtBZ$_dN=vzXn()qvvehCK9+zaqwySR^f8HI*ID469a-AqrZ(N&1??$ zcHEw)=-Frj8`FIBEKENe#r1clKysEI^{wl|MZ>*R9p}N&WGCnWiC1!|*N)Rkzl^(s z_kZpklVC83v{Ozfc#_t~PZg;AjK1wlh4&WdAaE>vTIl9lSETYr(*19WIY=xcB?sT2 z^+eu)OT5F}-Qo;Qi2v~@K%9-9rZsQ!(7WZXx9G2_W8t=r&-?g<3Hdn<5dIE*lZr=_ dl3ySl0G9VqUBkYjr*vGK=BWE#2=7rs{tI8e{D}Yn diff --git a/regression/ansi-c/arch_flags_mcpu_good/object.arm b/regression/ansi-c/arch_flags_mcpu_good/object.arm index 9ac75ab47a9beb812f67ffc2eeb7632fa668a285..d417b14bad43db553dfc0ccc5d627cbd03752a82 100644 GIT binary patch literal 4062 zcmai%{dW}A8OQJ4O=L#tsHwCzlu8@5X>CY0ya-jJ%@kkhKpEd!rNivZ-DJY<%sMkm z0>vT`BL+f@7;PIYHNW(n{#;6r+S7XaYk%m!V0eFRAP9J1kNw`cv%9l+Hr;c`NtoHs z_j$X|^W2?J^giBnFKM+rn-T3I^;uZ*T_fC9WP~mVoIaP?*{wu7NCzD|>?f(urRCj( zsGp_VEb&%)e@eV&IBrM?(f*V!n!Z_JA@c*$g#Y+=iskc8F>nIX{AntKcT}Y<@JhbL zjJ#)=q2sya7NXsmbMlNV_(B%XmRb02OWtuAY1Te&8ua`vj@xJ0j?b*n^S2S{iqzTf z6>={#t(I3PLLYzLa$U}vJ}Jj`kn8evTE$PY^wwO_gO|)F`fXAP$Xa+7zA3MUV>78X z%X5R!L@b&SrLXNyS^a>)m4h^;Dhk}Z{WJODY{|)oj@!WvazZ#%@>xd^`tTy?;eOw7 zNY1RmFCRBagxvWNHEo;wVt6^Cw=8vBn+*~D>r+&G$Eb>G=_q%1S*Gus+lanMg789a z3DNAp+0Mu})WpkF>)mSRON@N;bGd82PbSmF1EuxeJtrY2r6Hb0Mg4@fV}Q$pI^JtNQTAm0_5Tfl5j;PUEj{>w~0_L z;i1%8zVm^cLF7fC?)ix7OPA{3ouXR$F0J=_mnG9L^yj#(OJFOvG1etZE;rKS;!wN{ z#mi7^TM+5ZqazOEk{AUf3A@w z%(WfUb&+@2GY5O-xII4*7X0wf^IMSNVOEs~gato(PtL5WSDoqAG-de` z1iJfeIkP;8&Rl4Oj>z@g3*cVh+~tD1;?sE|hHyoNsVXal_Nx7I2CXhCEaa@6tUTXH zyW*DUk!ATjgwJ!~2V-GXSuLPz-jXY)I%2Lq(})?M737&wL7oBf3`hRBihM{Q7uGC% z=yW4m+_$Q@)4-kPxQ7Mqk$*J~jfhNCOg%#K(KqBoHMf(VQ;l@<9$I$v1AViqehTWR zxcXy4{U@I^R!35}0lbuZg}VBsv@)5O-V=?~qnfBh@B~CpaM7Q}qN=i103R<)b@jXU zcq3re^YT?Mjstj{1D~j-bg`{wND;v1pG>9jsbd%L!YifpApb?Ur2T3_{`Bp zP>jmzu{{djQO^6B;N7Pxn&7SfQ0_)pYt^G&Z3NVwTeps%+3n2ta9*#1c@@kJe72;} z6@NaFsvPHPveDuslzc@1@}cHfh>0NW(H&y{U;84I#f;>3Si1rDW!bZdA#e z1-Y}91wNrRsmf-u`9OkPF!NZIcn(}Pi1Em0ds#jJjRUaOtRx~kUQ2{n$E?M=T~))1 z$Nk9tMeeTaLR#7+>~KP^=oA@tic%Dl!%#U4l|D<~q}lzm)Nyl;>xA1dzp1J?0{Up= z0#2zz22!pAkDZYOQG_Ni*bvqop1KiGM|kSC2=ns)n6C#!J&5;!0@N_|U#WL}wvF%!XkfQRrDw^2cTFnG z*QDw6HHqx|XX+J8_bWSAFjfnHW$m-WSu7)nQ%Pv8sl=&721=s|)5X|DWJY1+s7$)s zwu;C+qAG*J>-L)0gJ%<8t@GOUO4-EVI1AcYxI83W7HbULK=yboJQX2tB)qL`hX|ZV zvr*!uRF-eR=Nl5~+Md&Y-NOn+6o9Ji5SUl@$r&s>!aiuk>+TNn8~CtY>)rVu%9{w9 z!j7?o;Wj_XUUmQrFa*Y6>KHGH*QoG(g{thL!u2>sd=BrTGYLeU@5x-xfHni#FwN<& z(;ijX%~5bUj$+M9Ja~gE4r6)UNp{n{2|O(1C(jf`yBEy8V2*(KCTH%6nX7L091q^& z%#nz>hmI$h@nNp|Jr3$PsP4dMjO&hY6JPyKyo^oY8xuTId*eu0PgXWpJ1Ct=tD+KM~syPP^1Q{SV1m6um4k6%9D zr@T$z@xUZKk|6Sq<)GE$22_@h0C)r!I?6A4>EF^;{dcj;zo$3m>qC4Oi5B}QuD?KQ zY1Zz}m0T;j!ycr#B-Y}jr9X)5eV+=mw8wBS3|Ta3{y;a2t2Q?ltn2a=U3iGwuu1Fv zBmElh==3ygCE9D$u`#@yoP&GmL4lI-CgSivX3U$m literal 4183 zcmaJ^YjhN68UDUq(y)`ntt75(sF*gkYBkMnvgKkCDVwy`;!qi>t(Q(`cfZ|Cvpch$ znI#EUTWYNpsn}vK&_WTCmKOD=5Uzo62^5Y8V}A8m5D}4c{OJXMP@iwU-Pwtp$({oz zm&x-y@AF>g>HC-67rvdeX3Q)j@<-HSPT4Y4XQ;#oUCN3jXNaVt?Y3FAGE6O)8O_m6 zgM?v-Fs**w$g5f1 zVj0J@hDhDNBb|L_k#+WK7GuTEteNS|q>GtOi{&k5+d%5n3|sHWbZS?u6iVPnqqEvG!nekkLzzC!;_8NJ)A>+$7ry-11cf_1D%H#pCEBJNSvE+N8+TCK zvA8cDpd9`<(=1CHBFdZyAS7Tn5;CenmUnu^}aqm-L(TPr22A-qr9)0)jl`%9AR%dLBZ zgrrTgpo-F%jO~S-y!kTU0pyPTL8Nw{X*oQ>9`k-M z@8`^)6U?6HL4pq-pE5J zmzGpC37W9neD@Kl8=dIVfILa+ljFY5cls=*Wo?xWqK2~oA4l7dOC&y@H(66Ex}-|)O&DFBsg5wXHC-T9DM zIT{35FtNz|gJ~3?qa5^`9_T6oT4^(mw`z9~o*!yApmqc5;a1!!Em-{DBJw{%tWeNP zwr-OKr0fwuKl=O1TE8m;YnufP`S!V3#w?a_vEXcYQ^5s~i=?gy9SNp)Lk_Pl~yM8iD|iifgTQ0>z3&MZOX$?eHg0e*RQL{{TcnMl&ns;OV{hF zti(%Db&0E5Ur~j6e6gbH=kzrxQH5}``yw3=Qss_alw|dIKzha@Y8;|AP%(-|XZ?b1 zt5s#S)zH~5(YgFC$!NAil$R??P-Pn{!8FyDt{mP#$wqqA7m>jR9aUUHs?Lv~qX_CK zg6jGuU0|3Fd$Oz*i1JDe_tgsSYxHkY(tjblS6o*riU(e$mwg;Xkxc|>umPOv{7q&u zb{RyMxqGkIus2oQ+e|k}iD}rI=&>O8s_T8afyZFrG1tI1=v?K^8poE3{;l+o)a}h7 zJ~LcQK&Swyx0`&TvW?G@}DbW@{yHTb=Mi<0ehb7QT=OL~dn zEwAkM&gRCc@a9Gmr+gEIhiR)aQo((j{$a*b3qdKEH5)a5nZ1ZQR9~yX2l<)8o{!@V1E0NBBeu`3()Z&(K{| h{D@NWTiPmz-=*?es%J3>^qh|O<(&d6g6Ak9{{y2Sze4~3 diff --git a/regression/ansi-c/arch_flags_mthumb_good/object.arm b/regression/ansi-c/arch_flags_mthumb_good/object.arm index 86bbebb12405c587251c3ad7911f441edc17138e..d0104c3b6059702ba2db08248a06360b62e47905 100644 GIT binary patch literal 4120 zcmaKv>vP=H8OG09nPj!4!nn{-#|4AAl!CF>A;Bpm1&eS=6NN@i+Tc<}E1k7PcBPG0 z8{26M&Ju!iag1}JlmIDi8D{uQnhu3&nSSku{tN9)bH6xu6Wr40=xBGf>8y9gp0TC< zJ@4(j?|WW-w(psydr7w7Ic~swqSIu_Ejj}(vol+W_AVWA>|l^2-jI6z`7GWdtJyMw+%KtU=Q!gn#X(E6GJYc&v03y^?P+Bj;IW;CL>Xhv&Cu zog5?c|1Cd}DLJ{oaXU@l8gv3?1tp(#76adL2a3z_W=qa-8A-k;r=hR?xoODrH{qFK zJ3e0a{1GBwO?C}>dDgYb_n3=kT?OA8@Vl%`-s&81f-av8_^eojc9#j)I;}1)W@K~b zK+(ttgQa}N81OtBhLhB%)U<8>y5VJs{*89Wwb?MyZ$3nYQAX8&O$xpKre*rRIYM+L z3AYo7M-$QPqO+BeTh!Rg&GX|?y$SE#x;G*IWgzrCYJFSGT#1pEFXisJKIt^#&R_r5 z#pH1B5@X4uJkImf&uB+Z5G11CrfO2N)_41BbF-ksQIdk6Z)bIdXO570GqPc*FRWd& ze#KfNo|*6uQcj7Sk{NkQQt_K~FPP82iTaSZW8@B@{+*BKR!?(vRcS>*%-32Lz9pxZ zgh`f(`Z?{$m_D<3ec#_2Ya_b+!?o`h+7IlJdF|9(zkj-scFyC6%qwMb%n&W0 zoSKICG#CF~B(5qC3UFHu`QZ6R$Qx+qK|9ZB-xsupzG&=9xA29#@~}|s+$k@Od-CwP zMzTe;gqRcOAbXC>J`%~QN|!(;YEE>WZA6RuWHlydfji4_-2#{XYz{9_2~k3Ngyf>H zlZ)eC^qgv>8`eT45vL$}iiAGmhIC7U3wbthMoG_v+cOs?P*7{+V~L$RDX0+k~?&_59%6wx{n==BHW zblu@ucO?d?3$&TTLX&49@Ctxe0Q{+?uhi_HO;g9sI<6CpAfnBxvO!q+;_GsyK+$tH zkp6`0AdVY$#3V$(iv}CU;=+q!2hcmXtv?sGKBOuy30r^hWwNd&UOFD*)R~I?raHrp zgLfP}Lqu5FC~T8NzAn)YUgb8+5_2Y5o7a2*8rUarJl2r@jWfw|Y9=`)%_Pa5za}!4 zZdLXad%Tvf%Hn3TX&S~ME3`U8ErcLT`m?)YMvJKnr+2}~T{7ueFd&>B{L5SoFzn;J zjXNSR&(~_tIUU2-#iTgs`53~n)^Zx6rxBT#MP$U<0dF@6tCxn<*;r62ix?;(+eV3( zXgM{D(99;0vs|^l^1?Lt1Gxvovu0p^wvmC_x>c+A@z~0Ik27K2EUfdgdSN-s7f@TO zvRRn+fZ)O6a7*U@_o3`*eZ_xJ&cUv;c|0a$^Pb~nUdFZy^f=JtKnGc!hCNUz32V0; zmeZAEMTS15`f$5GatOKHYGJFhe<{5C)mL*R2jeN+wXjNH0_Th@l zOtbcpR4{!r&u}X$k~bjv_XNx3oI=ql5(!}$<5ujX|CPlu{D_5GX%T0W?4pw?%gYyV z%fYo`jE<%w+%w=d?~S+^kQ0$jZjC!Zr(#?mP1)wRuRM=fIW+~y z6voVgHzNo--ehE4)TKVBZDf)ji$Us)iy!J^pdEur`;h1TJkJLrd)D8WXFNE_759aC zK0pt~@X>W3$IMNz@F186!F-FhBEi4m)VCw*Z|NW9MU`!sAl>g!UhR0?|291uBl79s zV1(dCS56%T@Tg4MDNm?$h_>qQM!vsCx23{`yTLECzVIIKKG)w#d9B=$ExA^BDL#x6 ziM1L{`dw)7J5<=EJ&8Maz`_ys0o^DHm0JtgXzG1>^AtB?rPlX*`X?IrxJ2UfH9ofx m($8O@Q&jv-Dft7?(uWkcu2JgPn2Ju;!Oj1$K*@L$f%qTAa*zW6 literal 4185 zcmaJ^YjhN68UDUq(y)`ntt75(sF*gkYBkMnvgKkCDVwy`;!qi>t(Q(`cfQ?Bvpch$ zoh1oYTWYNpsn}vK&_WTCmKOD=5Uzo62^5Y8V}A8m5D}4c{OJXMP@iwU-Pwtp$({oz zm&x-y@AF>g>HC-67rvdeW-Of%`6FsGr)-<5GgM@RE@g$HGelC+_L5b$Gfd4}8O<>) zlY|J7=VXmMBjNu<7N^Tb-sv#R4o%k${`=Ar{JuGFn2gMNPwMK%cOTRZSa!c*=2YFV zS;n#KAyW76NN1l_V4eM%%~+vRw=$iXbRpAevz*OJB_MTbX36NtbZT~{PtE4FTuCiB zedR)0%~_UC@R2_Z7d2ZeFo)SCasz?f5UCHDMxMxFH;x-fXqTj_sfSjsc(`|^YM9Wd z<&8CrOvXfDWS2A*PT_yjHal0e3=>#HiA2gE&zVe5uO{*^9WZpKk4PVe7J_75xIKeF z9nEw|!=FM4{AhGmdqz0d_;M)Ir`cTHFl{;?>h8jqADf`?hsUK_S)xSS3{z)=M7ePX zEjc!K#sieYA7`3vYePht69I$->_#GIOI&nwukX2**?xshcy1!@lXCMqS=MMEO+uIr1|FG#YBdAf{_NpLHf!z>kz6%u3NWDiADJ9 z59;bj>J)9y3(^Ln%esYz6gZ!O} zO@&XzNPOOG{s+iP1Gj*DT9CGFX_|>N;gY7JxAG|E=G)dv$!ZAi)AqDhVx;{g$@S&d zy+K0KmX%jUX-vlULe5?;=QBdU?b~M(!1)n%Dtdz4<4WSs&(J}h;CuUa0wEGnrcou`BNtP&D@8YHJdl3+?#9rqe2+3su9Ftfao zhfpppsb~^3VY&J4BT_dy(WL=-lGG>1eVy<0*-X<*DjP%%>i{1|+mA~mKA$&PQ!2VZ zz%&S*YeVgPe&{Sq7G90i>X3J#iq=A?JNI{U;x!1m+T3G z#EjNecgjr0_5g1W$6G4!?mas50Ex%>5R5JpoT+V60&}uPy6j{SDKm9LGffOeq~s)6 zPjc2CFN$7)c;72hVpvM>y#H0`#jJ8fTgdaU_I?@_-=z+EyvC zz#qy36G6lUR={FYts=8E({pkH^b?%^K|y~@D!N=ifBg+9akn3O`SBp=tTD)RHEY>e zgO=vNs^fq?&S7N%+m?#15U>wDFHJ*Tu`dYKHL5zj_5pAo2mFTT{Yn9-T#JY$j_J;a z#LCeiz`TV;<{wO>03GF^-}FFN3D8QLalBQ#gYf)Ny8*QuP!G4_Qfa~B{}z$|5n}ng zQ7joH(twmb0_aD7Us>ySWngWypdsHr7t2_MB5oF(4Ue3SrLmtUV`l+*Hb&aMBPM{@ zAB#x+cY%X}5_juY5#yB9Hv0i>4so}G-1V3v$vmdyK}7w2OlPIZIitwtW~V~2u* zE#V6Ab@U;KJA`;2&neo{R5UF#W&SKBt3!@2Jom;RI#?fVj^r1q_srd4|GK#){7&(|gU02Cj9Vk4(K0mc17asHf? z^rpY3xBzkkib?a4Eds9(MC@sD%b$KpuSFJNaQn?|jQBv11 z+d}kbpz#beKFJijdR&#>tj+Q2<(74>VV_~SltmP)|0s1=%|WG=Nqu?BCtS2X@TZ`8 zN+Mk?141*peNZ3_?P!=^MR40_aJZqiR&1+`L5S`t@LPN`Hry~39&R8D*W{G%!^@`x z#t;53CB5GEy!;`k)^IPMx^kT)HP5tu;9Y^PE8NScJujc3!pybwTqrT^^mvAz2(lBW zbIvRiPBSDsq2D|0*S`6YkRW zx+*L25>#E{s@7Ljp&nnXsQNj5O-fWD-0Z$c$AeV4V;3b^Jsyyraflj+s0~z%qS0Bu zpxbIyS#33R_Dggwze_S&$sx+i6(y*$jg?@UYD-rRZ=hr&J?e|dWP^?>E+N(6N6=9O zbreB${gN&)Er&f>*78JorH1=z1@|@jH!11Aklib;D;329uhPptj)KT00yNnGPIdk! zGa0)KqRZU9*K63DD(-Ejo20}v>`nAokbBkjKHb1$Fz}db;2U(V@@9==OGW=ydPwT_ z<`AD5u031mm`}RjnK1|+lgPriyp${=+kpM68us=I_71wK(Y+e{-oHi3cDlK-*5XB@ z$ncg|c6(=Y<5YNaBZ*VKiNeFQRT-(^zD@ry=xg&#&om>ezT&#OEV?qJ;d0hTLc9 jE-HRRDfumJmBa5+c`Y?`3<4u-;C*?gz>45GO342JQ3=2s diff --git a/regression/goto-diff/syntactic-diff1/a.gb b/regression/goto-diff/syntactic-diff1/a.gb index 2bf7c7b9947e2094186bd3379fdcd4736a43fa45..0cfbfe7718c51972aa74d035f38a68997b2ecb2b 100644 GIT binary patch literal 5738 zcmbtYX_yq%6@71NfUa_;(TPL?iJ4?#)I^+VP(V~9Q-VuOX(*9s3`I><^-M{3S6kf; zGe#rJK(mNABE$r6856e{O`cHk)Z{`5f2IcQ8I*9y6LT^$n@XGV)znht=F(BbFI% zCeIj?YBFw$v0BEolag-AVT0x>=Ghi58&Yn@VS~HnL<_ElCkq)X?|K~D~Czk_K zbGw)KM%ivM*_`Xj!*$*+Qj@^-3!4v$L2aL+v1~L3uAW zhP0i~&(o%x2{gsn0);LD+fLZdS2|(20Csgl5E!n$S<_^BnOxpP0P0_^0UP2|!{TcB zt|kSsVp{8LGgWZd(0ApQWB&*w-jwqSzU3Gx&oYBhod}sHy)9qRR&Y~!H#5rgtqwPj zP!)VM`YIWfn?UhzB)eBPbO!F73J|z_GV2zT>M~njn!fL2rizSvNtyN z91=a8G-?eWx>rt|7b;*Qp5vx%(>57ilIbHG-Hh#YGX2AAxKM3GLiG{L^nJ67>8A#a zM8q^Z=icP7kE)u~NOw=c-H+W-%Dj|^oDu1#wSN3R$BXT8B2VcF;jK-3VrkRza)DFo z3%n^MHm{!PpCBDt>uIZ%V`ClvDKSZ>;?F0O`l;j?W5W**v`NrXR1RZn4r6OhPwFQJ zk%*rmB7WvNIf2ay_MCm{Ij(=YQ9o-9*Q8MvpzX7T=H^5HZ+Pf5Av`U+W1Zv28e-GW zKzt}Jp)c%=g9G_MSqCo;!i$6OqAmehKpXw&v1KJ%uq$eOjBxdw)pBBN=ql2CFdMUf zAilJdMjbJ{tmB&*+X&LAsO$&*exg5D&<|DPV+HiMyX3^VQRuPz27)$IsE=s}r@pA{ z1K>Ua94`RRTX1ZDkQwC91VMWKopJ()r*vEgvk7|#BAr7=&dAeQEo4OH1^r&o?IO~Bg(uk=`0xv%c2_)%Jonlf!9 zbxF(2<(YnspgvEHPbYV@hG7+IP14!)#S!|9)0sE&9lm4QhHJxv#b8`ayZD82Vq7ac zsIS0WyCDKm zG}9iEvZimQ9W>A!n?Z?kJu}uQmY2?AG_o1HzAvJI_RvL9L8B`wecsGgH*4EG z4>Of!x9vhX#}-?H?DEo9T1>JQMUX@+a)#51>3{;V2xyDog-u()kxI^r$`**unH;IN zmxJCR2;8US(N*V2lWf+pKEjlBvksbfAt-|D!LpvhenS~(mI!<54mm-SRXC3fX0!H0 zK&pZt)VJ#Dwg z38tv51j$N}%uecapuAInsz)pDWL?0X4dtwJc?8s^jP}}Yz=Q{|;V6r74CW_b6P;5gbjh6D>2%3+hW78{7nyO1t=>jS|cG<_KSvdMYdBKyL=~X2@TGK;J=u?g_OIK045Na3`r-5d^x2FN@$K zW9b~2qU~P6Cou{c6afe5%?hayC!mmHie(XfpI)!w3VDAp?-ilIZU;Uo36mGoH` zLfukHA8LN<_`Ha$Xycm)QS&H$?kT5_8o!rN@Je$cd_9>Op>BAhiz8keSKg{Sv`E0JR68 z_TfOS(51#72?dK}V8$c7pBI&W-YfNU)>s?7?hksDkI=ux$K|@xZD_dkVltPzHYR*G z>Ea#uF^;!>HI9!3(zp2trcFZ4%R9jvz~g+f?O15i^thkP@h8Y7Q)~SWe}?CMyz}Gt zK7KUr&8q>Rk?3ef@CcfpgsOjeP}s~jbP>A$4i#f{d})Hv0X zvO-++$#+NXUxWRx$UY78*EuE!KEahs8h0VkS8L$uX5O{a^eI9*j)E=b<;kqw^+zmM6^=zFZ+0 zF!D+>#Xlu%3(!_X{lCju{1(UPjHeQ1Zg}eG8>93#$TyT6+{p3qPmR}x`|~(5sFrmr zwK%&aqfJ=9xw5`|xYYQT@Q|q5@FAiAb}L(WfvO8WL5Ya&!bUAHK>=ZWjM}&3WM?)R+3c({vnG+) z^?`ua`atBZR$E)EqPE&%>!ZGv2IUb*K(ZiEk*a7!5!?FccjvJ)slSy!+~1F|vvbaO zzH{z5=bn3WXH7dZTus!BuB9#2AR?Wjwq~pj!bhu2J!>RXDWxZ5OViUNM2IjvsijmB zeuz7*DXXQdv08eptSB0LZ=QkoBT`ygC4+8{)W`6&y`)Vy=4$C?Nzn{7Vd+K(DOtnS zTxhC>S!2mr%S^PSYZ_H^uBB&crnZ?=jb?t@9DZE0X4M#Kv!R+Mplh0SOCPIf$z+Y$ zk+$T7r6ue~7$N+ka8&~4EjeuwZb!)eEgB+`>4jf~u+@=KL8$R^Ih9pOX`Tuf&YlhB z(9(z`@#mg@&PCJDms;f%oR##ZOTm@&$7QlK(jDgUmy9n{#cxdEqk|EGurT7NTO)Oo zZ3j!3eGcIoOomJs!ev5ZDH*&t0IH}qs%)tWAQuC0G2n)lnp$&ORhlj*!acN2Q>+#e z-5IK@g+FTtRV5^w@X@P6j+lhi0o!4rw3Z@5csRa~0Fz_hj?3c`EbPZV#?|5f@?!Pi)mUcP58)pykcq|@o2a6j@+evr$-8ebrcvbu++$wk6s< zI-a>zzGR?ViXW*ZaBB(NI-x9^4mx(?uF%AKxD@@CV}L_SAYxz8D(0V}Cds!S=KKXP zwJTH!jv@q=cZNJDWFRugjld`e=sU|I^@x=Xw>&`0T|x!~KbM2na?q+OY0~u+At#-h z)-Cn2tehg^cj4Ahq4DGox$#H%F#e+*v)@}0sb_Jvy;w)9nq*TY)h}`}M2(2wcOkJt zRZL~{$}cn1Oew9lNwQ(c9bmW;3|E5Tm{O!cl%*1UKboB4AdP(^egtkvc0M`|SRqS#l8BQkwX~wP z6LIq0)S)H?$~2yE0wXrqb`XntA}IE1o`#T|&VD@+zn*c2R~UiZ5E_5*=8@v{)!~fA zSo1)enDPMEK53%lYItNF@sf>uwIPLSVXA4Z2sc-}S@v7KB$b`K`7Xu55 zb=Zq_*o$>&EDI#d^woZ$xHWR7ldKc%H0=%4mltUiQ&LN7R)>^jD*f?Zt~=bzAq~%R z5^u(ivZ9fSId9l{&ve%NSg#(c$;?f~eDD@Za++O#d=tFc1aD?BZ`h(%lCwv$wvdob zi-@xwCMWaJIgUHR$6Otj$G0VfXOTIF1Ma2Oc1yBa3{_Snjdk0@aO*I0>l_E{+-FOR zy2W0=HRjfNj$7w%=3=J?4W75Vm~*XaEA}=?&!~o+RwTFm?1qQC;h~7S;iDHgs26VI zYP}vyE_#WIKdcmgbT<{kKTe1Zg7On5yMFrC*UPS$-I0*VKYNgCl@q$j{JH>%%o5m5 zIjV*WtBKfVw2_ksSHpF7dJcw6zLV4=f@S&`KK@hlFhjm6@CF{zL>8xe<%EbM6qPv7_zVYhSE4tvJ2dD&X7;03dp*<8#f z+Y$@G-wdOhnNh+y8+nE0J9F@E9utA!~vzVg7ySjm!W6V3OkUsvfAj6_n>+8M39`TT&#=v=xUeT9dsQR^H#>r z^VM`mF^+9^_4`%010;8Vwp_ptzU zb}ndeihDF6mpI?-!hNu0%-z02_qcX{L!ajc)a^aAx0qQIK?=mY7bbg|JHK^d$MVs8 zUD)5zEnEx(vA>r0(mlm+RfJzor!fx0kv%}&!%%Z}wpOQ6neW~9YGg?N)w4Sv` z#`UG$;q|59{;-esh|B$tbORR~uxmU*cNXKG)Y?@=O6rD`OzAS4Mt6euP8OCw`N4kF zg?@~_&eaYW10SXPi$SwPzJ!=up&G2O?Fa6DhWlq1_b>GIqGOgj=GuGfTG#mF^kt46 z5&V^2OScy@Znx_HE8Xp2upJBr*=O^TztRfvZ*;QR(b|OLDLaqmGzDiaEvexy<_U@u zIv>SBKl~)EAi^|kO_pk($)2KTDQW^ITK2k&ju`qh^QcN_{5yStS_ZB-@c9CtC?U_l z$g}<$J;!{(?qCV!$N7FR6T-CT=_NpfL>GOI9`!W!AYK5(i*&M0@CoSK!Y|PoxZA)E zTF{948l4P*de4-Sm(i=4TJAW2zv6Oe_c)Y6k`m&lTA<$#S?8)w`v;ZHxmpIU<+;uh z51i2J0{i!jnT^w7p+a2G_#Q9hUZuF0AmT`e^lNmcj4P#PT#T?=k33gCq<}*$T5 zF_#kYQr}Jsq+0^gyCD4rlb$8yc2gXch|+|p?6q_AxXL7c>f`#794I zYvOUr<`cUzq5BC96xF{yKDRR1PiTORUpejoJLo?!)G7X#nYsbdIY^24DQ%LC<}B+V zI1f53KckX&XDB6bQ_14fiHW%LXrJ@vfcnDad{t-xt}4Wm9sr~0osGJpXWE+ zOalPdget^qLpbZs4^@iSh1h8~E;K$5N>jbFC=56V3qsqep0zSr4B-W=K|YyGlbzXQ%1rS7iqdOYkS$I4$rmIc-WNj+%~T%-kORxwmG>b&u;VVY!*mO zZEntOw46kuDchaSnShV`A7jw9kVvLXiA|X@n-!E+wm_N9`Xm+Kv(x3Vao4h$_73;# zT;59y%ao~hDwFGGYP2Ei=DoOWB;B~_OFjn14besqUnox|Q%3mWBl!1WDPwwO%FaPC zi!$xC8atVEGFd0fM!r%*I@IVfY}6Vh?xr&Ej>Xt9y-GppRr;h}h1IiT)wr9^=1llf zlY9p=t>q>&nYY>K`AT!upI9^fA^78jw&UN6OdxG14DgicqyvTOOT3}g%pwfzxOoaa z@Lkdcm)xp!!6EbDj=EupH&@@PX((wKiHO&*kEogiIb+_HtLhLBV5k~B5kkhkEuY(( zcak|L-DrC8b|;6p<~_SHoAVIM>{RF)J??&aJf*}7wGjq^L)nQ(WW!J|pLN+)(`Oms zZH9K`rI#8`)|hR3E;JvJ`=lc>YyM~=<0AcRkLf3o_~8&wl0P=TCf-iDMHzhZ-pIr= zNmxAz(?)-Mog6zmpk<$Uo|~3MiDbA5rZ?0(Y0K_n`X^U&A=N1PLX$ofH$BhnX8I|D z3`9(`vd(OqoeCFyn!Y_5^rtN=o{gl7tQH4EYx&IkALhTo-5aAoLwL()_e4@=+|Bw% zsW0+|q{x(!Oh27;Xf2Ja2FaPhS&C1INje38&q(N}kYS9~AFdW3XelU%5tYM;N>f5V z$@fIGS$I6QR*unup+K|o&vSi3y?*9uu1ROb0c}kbnkOClf89gp4DOk{JJL0Iq9KCb z4F8Z{0$W(~!D=>8!oiAzu;L)Bs5=|7fHvjP!DYpo{o{9zF!kKK<=Di)R6nQB* zWv5W-3^!wYX4*3RG%6_jLBF5qKPTwNsL`nc`nzSZP{Cmw3CjUk)vapPmA6F`n{mvOY|2A`suF> zLJwaC^fLtg%sb>5`c9dC#_kWJ7Y(bR>;~~}5Hm?yr-=G~Dr47+-%#-wdwfXUg+kOt z?^G2fBnh8fEJR&$yBtHRl|@~=tC}eP{9A6mHEA0~VY?t~7ld6p7LDig2=2qu2sTPu ztCVY>fllC2S0$OOP77S8MlTZzF27AKRxm%wF56K}Ko-?D#JvODJ181o5RkK8t!g;h zN+}w;puM73o)orQ-&T#*x4T&UN|tW}`!=v&8P~6h6mvw38N*RFzqq8P_@z-S-`1CQ zaVMQ{(hfQ@N}C$J8d|>mZbY<~M(Qt?qZ>g7Sae^0FPp)d-_8j{17s%;uPWy`Vl{ zjhbW*Mv5}ECSA+SLWn+Xcjb&+yJwr0;aISs0LB7Ev9**Kabdy8GE96!2%^FQ^rKQp zHUMe^pe#y8d#V~u2t94j$PR1p$61HUxy9;vy8Mpvw3!o}VF6Bs#)Y7s`MLSK8)7_F2 zGlJm8r{(b#=R%W`EVDkulyNdPI(pu(jO)R&p4{k_fU?4kxn**Url`_nlHC&msc@!W z^eRi<9^mc)Za$&k1dnzKapws%3@H9kLf?0RH?OsHzrks~L5g&)4ABJrA!(Z(aLG!5 zt^}wv`>eE^vv16sNv40bBz%q_QOlC`uLTcrY#cQ@hs{|L1~-$KYN=MI?M}>EG}aW9 z6(CswlA9CyEl}RW1?nY7OUHw`9Pl?oJnP|0LckVfsoQ!3<~;x|0pJpH@vXER-Eb7UkJ^^(Xi+y zmZFPMLFofXpUfuLEe}BMZw~QQsHd_~a`a{}Z-)Gp zaP-~e=v9ICp+`F!5AGp#D}6_=;)_H0$VSR@QKsKa}B1J!)XPO!Cnf27>tY1lK+;8EJHW72)WuAFb$ z@(_8DD8X#F9CXV;x6Y@dn;KnqQcU_r03aIJp%78=_JU&}ny8Vd`dLs8Mf#*e5p=El z`8d6=oFWedP`$jIBh--|;B!N|!rf>tRL!Lv`DQ6c)aZi*gY)|kKN6`JS|8+FLO2!9 z^-F1SO4=1{7`D(|o3hmmY1n*av$@JjIJk*JJ532ooI2+#QqtzYipA(#CSJAOnvP(6D1k5N3Z<(|+M zRF{5vRd~x!u;r(;#leoBar8^3&n|P!!TLENhM!~kFK9U$K@WcoeE{nhhZxW(`sGDo zhF@aK>$C-TX{yet-mSb#SdRKWv zC)Rg{6#fp&e^1M=#qvLJOqNVH%F9hGH$%(+h~{f5(o06!rWQbq71{5A8sS>X#n~@AwyXyh%IS!SNQy z=*aYc^EbIa*Z41X{u3OqxA}8CVJ7h=3<-?6RB9Lh6*Hs*&>bQ58%hbhkz>BaQ;Bjm zIGgnTQrZOa%|!#ZaJ*PlqqRYNp5*jUfi@5>$jEHm(GshQJd(bPm@K$uBWL<7dFj(0x?dAD3G<1i~TyI(PHAOrAO<)ndY`Ez3Dva>M(4Ewn&v$P@nst;VM;k7Qp3|%u)wSNvML+-ioln%^7kYB=SU$jw3YVf%gS^@i__3_cLOS=Yqtv3w2>US_ z90x+@y%Djx25%aAtVJ`h&2qXrHf!kU5mx^gpZA5vc`1+E8F8ieE|Zlcwot2zoiPyE ziPY|lu$l>~6yZE8ZJzbF`eH3eKIbrza}dkV?-fGM-euofL+D?;&B*BllfGT4rQ&KE zlP29q7Ax7)L?*{9O{50P#p;rJCdSR=MWIF`|Mm=sGv#h)+j?q3Y`oy@|0mVaQyU8L z)`li_;lo1P_;IpTvlFAQQB~6FYXXxl;zY#8iw}P}Utq#r`5W-}JF3*c*u*_W^MG6; z1$&T!JxIZK%RF^5b%nb@?7eY`Rh#FVRoUm+SB}!yLdHIW_MSb!g;FtT9 zET7-sB!tfMRY!TlAe=V)-6h5Cc7Laozk*$>x{ z^rK4Y$M=!w|4B@05aU0!Qvb7ezFg`7JlJmPuYJUUPQc;pT({^iO&ErC2KJ07Z#uDXmB2Up=>$^gj(lOVmcH3 zbJ@HDo}Om3=&BNzH9q?tKpQ(Cu<_xm$pX4G8oY)q*4NSt!k~t64Q(mL+w4_GG^{P) zz6IQ`qY8{t*V81%syfNXI_urXr;H(4$K--R4*!JbyF9vV9+hsh?4sUc4D8cFLAPG` z?uGB+ozzKP_0}ABCS%jBcc!~XhAg0%G)9cyK%b*!Vec*EKB3}`^obBI^fmMQ(F^I| z5h`Y7wGA@^m+~N_JjkC2zjQ;m$qr$p8^TSrwO9!8bgn6>79!Y+2)6PFM&Ha~Fm;X; zN8Li07EQE|_ylQ=!gJvL!^j+j^btnk@U6E0+vv@rUDtjjnOkj;ECV4TQIG!i#MNsLCa_pm)%gz_>x1Ug1Uv!py6~m^%ny+ zaWR)V!!}6w1G^vCbMK~;qyBMyD zyeX*^##Jb=8>qWE>hIj>AGA?_Pp=E1LEZd8$`?a*(l%J&JmB+ye~7GsZgt62_As=5 z#Pzn)*7{NEE}bw)8`1v|v6Zy0)NMW)Eu&(Z&Y2_Ky3!v1x>8p2nAxo!Cp=7_u)+R7 z{X(r%ar~@zs`*>h6O{L)jt__$P5|b?DUY<}1y=c_i8dT-PKyRtaXf5fYnotHtEig> zBHh&E?gd@6n_V+(WIHEV8Ia#Js5A`j87ChHWIEe zm~^tE6~7wE3l$!THo>}wTbGF)n+f+nOd94|4~6wmkM$N<_j2noVn-k0=*^_Du5}Hp zYdqFlVZDu8GqK}M!c`TM0(j-KJmIo|NjrG%PREfk8pLgdop1g= zFP!aJxf3hj;wxLkj$MSQl}Sn0dIqd#c&vBBdJngrD|Y-HJr~w@(k^by7pm=Dl?GOqy4%Yp;;_W77zp@fpe-5E-i z4>ed~zj5Nlw|QZqm&_+lxgJDYv+9l4sJ;F8eU<-HFgRof_)o&P5e@R;#1!#)c)*AK zk(&wI*je^3toV0fMPVOBgP+;^;dbIvjkztc_A~PAsLvfjw{Y0c$iv3nHTD2m@&z1q zlJp<$>oMqakeGCsz`8ldTMdqk7R{@DvUA@k$8ZnI73w6+q@8rEOZysMg>11lU@2sik) eQ95U2a+re)SS2o*g+9BF-015B6He75#eV_ZKjiiR diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index b3f868e50ff..0543c0d2ad9 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -20,10 +20,10 @@ Date: June 2006 #include "goto_functions.h" -/// read goto binary format v3 +/// read goto binary format v4 /// \par parameters: input stream, symbol_table, functions /// \return true on error, false otherwise -static bool read_bin_goto_object_v3( +static bool read_bin_goto_object_v4( std::istream &in, symbol_tablet &symbol_table, goto_functionst &functions, @@ -221,13 +221,14 @@ bool read_bin_goto_object( { case 1: case 2: + case 3: message.error() << "The input was compiled with an old version of " "goto-cc; please recompile" << messaget::eom; return true; - case 3: - return read_bin_goto_object_v3( + case 4: + return read_bin_goto_object_v4( in, symbol_table, functions, irepconverter); break; diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp index a6d0f144cb2..3ab58528319 100644 --- a/src/goto-programs/write_goto_binary.cpp +++ b/src/goto-programs/write_goto_binary.cpp @@ -19,8 +19,8 @@ Author: CM Wintersteiger #include -/// Writes a goto program to disc, using goto binary format ver 2 -bool write_goto_binary_v3( +/// Writes a goto program to disc, using goto binary format ver 4 +bool write_goto_binary_v4( std::ostream &out, const symbol_tablet &symbol_table, const goto_functionst &goto_functions, @@ -151,13 +151,12 @@ bool write_goto_binary( switch(version) { case 1: - throw "version 1 no longer supported"; - case 2: - throw "version 2 no longer supported"; - case 3: - return write_goto_binary_v3( + throw "version no longer supported"; + + case 4: + return write_goto_binary_v4( out, symbol_table, goto_functions, irepconverter); default: diff --git a/src/goto-programs/write_goto_binary.h b/src/goto-programs/write_goto_binary.h index d9cf23d6def..c700f41cc04 100644 --- a/src/goto-programs/write_goto_binary.h +++ b/src/goto-programs/write_goto_binary.h @@ -12,7 +12,7 @@ Author: CM Wintersteiger #ifndef CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H #define CPROVER_GOTO_PROGRAMS_WRITE_GOTO_BINARY_H -#define GOTO_BINARY_VERSION 3 +#define GOTO_BINARY_VERSION 4 #include #include From 355fbd2920e5e22cdff23a31491916e8a09c1476 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 30 Jul 2018 09:00:20 +0100 Subject: [PATCH 3/3] avoid assert() --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 2 +- src/ansi-c/c_typecheck_initializer.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index db7d8e4536d..1b223a80b14 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1633,7 +1633,7 @@ codet java_bytecode_convert_methodt::convert_instructions( const typecast_exprt pointer(op[0], java_array_type(statement[0])); dereference_exprt array(pointer, pointer.type().subtype()); - assert(pointer.type().subtype().id() == ID_symbol_type); + PRECONDITION(pointer.type().subtype().id() == ID_symbol_type); array.set(ID_java_member_access, true); const member_exprt length(array, "length", java_int_type()); diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 2444b6201b1..ad1be10fe07 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -492,7 +492,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( const typet &type=designator.back().subtype; const typet &full_type=follow(type); - assert(full_type.id() != ID_symbol_type); + CHECK_RETURN(full_type.id() != ID_symbol_type); // do we initialize a scalar? if(full_type.id()!=ID_struct && diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 2a5f7304264..a634b081a19 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1861,7 +1861,8 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) if(no_typecast) return; - assert(expr.type().id() == ID_symbol_type); + DATA_INVARIANT(expr.type().id() == ID_symbol_type, + "type of union/struct expressions"); const typet &t=expr.type();