diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 632c741d629..ee8262f3a64 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1185,7 +1185,7 @@ codet java_bytecode_convert_methodt::convert_instructions( { if(cur_pc==it->handler_pc) { - if(catch_type!=typet() || it->catch_type==symbol_typet()) + if(catch_type != typet() || it->catch_type == symbol_typet(irep_idt())) { catch_type=symbol_typet("java::java.lang.Throwable"); break; diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 7d5adcff2d0..317b18f2656 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -105,6 +105,11 @@ class java_bytecode_parse_treet struct exceptiont { public: + exceptiont() + : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt()) + { + } + std::size_t start_pc; std::size_t end_pc; std::size_t handler_pc; diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 655c696f659..4c8e3088730 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1249,7 +1249,8 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( symbol_table_baset &symbol_table, code_blockt &code) { - symbol_typet object_type; + optionalt object_type; + typet value_type; if(type_name==ID_boolean) { @@ -1296,6 +1297,8 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( else UNREACHABLE; + DATA_INVARIANT(object_type.has_value(), "must have symbol for primitive"); + // declare tmp_type_name to hold the value std::string aux_name="tmp_"+id2string(type_name); symbolt symbol=get_fresh_aux_symbol( @@ -1304,7 +1307,9 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( // Check that the type of the object is in the symbol table, // otherwise there is no safe way of finding its value. - if(const auto maybe_symbol=symbol_table.lookup(object_type.get_identifier())) + if( + const auto maybe_symbol = + symbol_table.lookup(object_type->get_identifier())) { struct_typet struct_type=to_struct_type(maybe_symbol->type); // Check that the type has a value field @@ -1321,7 +1326,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( } } - warning() << object_type.get_identifier() + warning() << object_type->get_identifier() << " not available to format function" << eom; code.add(code_declt(value), loc); return value; diff --git a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp index 913658b4e89..3dcadf430b1 100644 --- a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp +++ b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp @@ -17,9 +17,12 @@ SCENARIO("generic_type_index", "[core][java_types]") const auto symbol_type = symbol_typet("java::GenericClass"); const auto generic_symbol_type = java_generic_symbol_typet( symbol_type, "LGenericClass;", "PrefixClassName"); - java_generic_parametert paramX("PrefixClassName::X", symbol_typet()); - java_generic_parametert value("PrefixClassName::value", symbol_typet()); - java_generic_parametert paramZ("PrefixClassName::Z", symbol_typet()); + java_generic_parametert paramX( + "PrefixClassName::X", symbol_typet(irep_idt())); + java_generic_parametert value( + "PrefixClassName::value", symbol_typet(irep_idt())); + java_generic_parametert paramZ( + "PrefixClassName::Z", symbol_typet(irep_idt())); WHEN("Looking for parameter indexes") { @@ -43,9 +46,12 @@ SCENARIO("generic_type_index", "[core][java_types]") const auto symbol_type = symbol_typet("java::java.util.Map"); const auto generic_symbol_type = java_generic_symbol_typet( symbol_type, "Ljava/util/Map;", "java.util.HashMap"); - java_generic_parametert param0("java.util.HashMap::K", symbol_typet()); - java_generic_parametert param1("java.util.HashMap::V", symbol_typet()); - java_generic_parametert param2("java.util.HashMap::T", symbol_typet()); + java_generic_parametert param0( + "java.util.HashMap::K", symbol_typet(irep_idt())); + java_generic_parametert param1( + "java.util.HashMap::V", symbol_typet(irep_idt())); + java_generic_parametert param2( + "java.util.HashMap::T", symbol_typet(irep_idt())); WHEN("Looking for parameter indexes") { diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index aa541a9d6e8..5ece188914f 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -601,10 +601,8 @@ void ansi_c_convert_typet::write(typet &type) if(vector_size.is_not_nil()) { - vector_typet new_type; - new_type.size()=vector_size; + vector_typet new_type(type, vector_size); new_type.add_source_location()=vector_size.source_location(); - new_type.subtype().swap(type); type=new_type; } diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 1aae265fd53..c023ea48041 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -792,9 +792,8 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) } } - symbol_typet symbol_type; + symbol_typet symbol_type(identifier); symbol_type.add_source_location()=type.source_location(); - symbol_type.set_identifier(identifier); c_qualifierst original_qualifiers(type); type.swap(symbol_type); diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index dfaa7902b3f..e4ed361160a 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -5987,9 +5987,7 @@ bool Parser::rNewDeclarator(typet &decl) if(lex.get_token(cb)!=']') return false; - array_typet array_type; - array_type.size().swap(expr); - array_type.subtype().swap(decl); + array_typet array_type(decl, expr); set_location(array_type, ob); decl.swap(array_type); diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index a242577e8cd..8059f7cb558 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -177,7 +177,7 @@ void remove_virtual_functionst::remove_virtual_function( // So long as `this` is already not `void*` typed, the second parameter // is ignored: exprt this_class_identifier = - get_class_identifier_field(this_expr, symbol_typet(), ns); + get_class_identifier_field(this_expr, symbol_typet(irep_idt()), ns); // If instructed, add an ASSUME(FALSE) to handle the case where we don't // match any expected type: diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 09f3f199977..e7ca8c3fb65 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -791,9 +791,7 @@ void string_instrumentationt::do_strerror( new_symbol_size.is_lvalue=true; new_symbol_size.is_static_lifetime=true; - array_typet type; - type.subtype()=char_type(); - type.size()=new_symbol_size.symbol_expr(); + array_typet type(char_type(), new_symbol_size.symbol_expr()); symbolt new_symbol_buf; new_symbol_buf.mode=ID_C; new_symbol_buf.type=type; diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index d52bb8eafa1..d71454d4fd0 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1028,26 +1028,27 @@ typet smt2_parsert::function_signature_definition() return sort(); } - mathematical_function_typet result; + mathematical_function_typet::domaint domain; while(peek()!=CLOSE) { if(next_token()!=OPEN) { error() << "expected '(' at beginning of parameter" << eom; - return result; + return nil_typet(); } if(next_token()!=SYMBOL) { error() << "expected symbol in parameter" << eom; - return result; + return nil_typet(); } - auto &var=result.add_variable(); + mathematical_function_typet::variablet var; std::string id=buffer; var.set_identifier(id); var.type()=sort(); + domain.push_back(var); auto &entry=id_map[id]; entry.type=var.type(); @@ -1056,15 +1057,15 @@ typet smt2_parsert::function_signature_definition() if(next_token()!=CLOSE) { error() << "expected ')' at end of parameter" << eom; - return result; + return nil_typet(); } } next_token(); // eat the ')' - result.codomain()=sort(); + typet codomain = sort(); - return result; + return mathematical_function_typet(domain, codomain); } typet smt2_parsert::function_signature_declaration() @@ -1081,37 +1082,38 @@ typet smt2_parsert::function_signature_declaration() return sort(); } - mathematical_function_typet result; + mathematical_function_typet::domaint domain; while(peek()!=CLOSE) { if(next_token()!=OPEN) { error() << "expected '(' at beginning of parameter" << eom; - return result; + return nil_typet(); } if(next_token()!=SYMBOL) { error() << "expected symbol in parameter" << eom; - return result; + return nil_typet(); } - auto &var=result.add_variable(); + mathematical_function_typet::variablet var; var.type()=sort(); + domain.push_back(var); if(next_token()!=CLOSE) { error() << "expected ')' at end of parameter" << eom; - return result; + return nil_typet(); } } next_token(); // eat the ')' - result.codomain()=sort(); + typet codomain = sort(); - return result; + return mathematical_function_typet(domain, codomain); } void smt2_parsert::command(const std::string &c) diff --git a/src/util/std_types.h b/src/util/std_types.h index a6d1c98c412..ca2c0934685 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -110,10 +110,6 @@ class real_typet:public typet class symbol_typet:public typet { public: - symbol_typet():typet(ID_symbol) - { - } - explicit symbol_typet(const irep_idt &identifier):typet(ID_symbol) { set_identifier(identifier); @@ -492,10 +488,6 @@ inline union_typet &to_union_type(typet &type) class tag_typet:public typet { public: - explicit tag_typet(const irep_idt &_id):typet(_id) - { - } - explicit tag_typet( const irep_idt &_id, const irep_idt &identifier):typet(_id) @@ -980,10 +972,6 @@ inline code_typet &to_code_type(typet &type) class array_typet:public type_with_subtypet { public: - array_typet():type_with_subtypet(ID_array) - { - } - array_typet( const typet &_subtype, const exprt &_size):type_with_subtypet(ID_array, _subtype) @@ -1575,10 +1563,6 @@ inline const string_typet &to_string_type(const typet &type) class range_typet:public typet { public: - range_typet():typet(ID_range) - { - } - range_typet(const mp_integer &_from, const mp_integer &_to) { set_from(_from); @@ -1613,10 +1597,6 @@ inline const range_typet &to_range_type(const typet &type) class vector_typet:public type_with_subtypet { public: - vector_typet():type_with_subtypet(ID_vector) - { - } - vector_typet( const typet &_subtype, const exprt &_size):type_with_subtypet(ID_vector, _subtype) @@ -1706,11 +1686,6 @@ inline complex_typet &to_complex_type(typet &type) class mathematical_function_typet:public typet { public: - mathematical_function_typet():typet(ID_mathematical_function) - { - subtypes().resize(2); - } - // the domain of the function is composed of zero, one, or // many variables class variablet:public irept @@ -1740,6 +1715,14 @@ class mathematical_function_typet:public typet using domaint=std::vector; + mathematical_function_typet(const domaint &_domain, const typet &_codomain) + : typet(ID_mathematical_function) + { + subtypes().resize(2); + domain() = _domain; + codomain() = _codomain; + } + domaint &domain() { return (domaint &)subtypes()[0].subtypes();