diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 74299a6f2de..87aef322acc 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -484,21 +484,19 @@ void java_bytecode_convert_methodt::convert( // be rewritten below in the loop that iterates through the method // parameters; the only field that seem to be useful to write here is the // symbol_expr, others will be rewritten - variables[v.index].push_back(variablet()); - auto &newv=variables[v.index].back(); - newv.symbol_expr=result; - newv.start_pc=v.start_pc; - newv.length=v.length; + variables[v.index].emplace_back(result, v.start_pc, v.length); } // The variables is a expanding_vectort, and the loop above may have expanded // the vector introducing gaps where the entries are empty vectors. We now // make sure that the vector of each LV slot contains exactly one variablet, - // possibly default-initialized + // which we will add below std::size_t param_index=0; for(const auto ¶m : parameters) { - variables[param_index].resize(1); + INVARIANT( + variables[param_index].size() <= 1, + "should have at most one entry per index"); param_index+=java_local_variable_slots(param.type()); } INVARIANT( @@ -522,23 +520,20 @@ void java_bytecode_convert_methodt::convert( base_name = ID_this; identifier=id2string(method_identifier)+"::"+id2string(base_name); } - else + else if(!variables[param_index].empty()) { // if already present in the LVT ... base_name=variables[param_index][0].symbol_expr.get(ID_C_base_name); identifier=variables[param_index][0].symbol_expr.get(ID_identifier); - - // ... then base_name will not be empty - if(base_name.empty()) - { - // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local - // variable slot where the parameter is stored and T is a character - // indicating the type - const typet &type=param.type(); - char suffix=java_char_from_type(type); - base_name="arg"+std::to_string(param_index)+suffix; - identifier=id2string(method_identifier)+"::"+id2string(base_name); - } + } + else + { + // my.package.ClassName.myMethodName:(II)I::argNT, where N is the local + // variable slot where the parameter is stored and T is a character + // indicating the type + char suffix = java_char_from_type(param.type()); + base_name = "arg" + std::to_string(param_index) + suffix; + identifier = id2string(method_identifier) + "::" + id2string(base_name); } param.set_base_name(base_name); param.set_identifier(identifier); @@ -552,10 +547,12 @@ void java_bytecode_convert_methodt::convert( symbol_table.add(parameter_symbol); // Add as a JVM local variable - variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr(); - variables[param_index][0].is_parameter=true; - variables[param_index][0].start_pc=0; - variables[param_index][0].length=std::numeric_limits::max(); + variables[param_index].clear(); + variables[param_index].emplace_back( + parameter_symbol.symbol_expr(), + 0, + std::numeric_limits::max(), + true); param_index+=java_local_variable_slots(param.type()); } @@ -952,17 +949,14 @@ static void gather_symbol_live_ranges( if(e.id()==ID_symbol) { const auto &symexpr=to_symbol_expr(e); - auto findit = result.insert( - {symexpr.get_identifier(), java_bytecode_convert_methodt::variablet()}); - auto &var=findit.first->second; - if(findit.second) - { - var.symbol_expr=symexpr; - var.start_pc=pc; - var.length=1; - } - else + auto findit = result.emplace( + std::piecewise_construct, + std::forward_as_tuple(symexpr.get_identifier()), + std::forward_as_tuple(symexpr, pc, 1)); + if(!findit.second) { + auto &var = findit.first->second; + if(pc holes; - variablet() : symbol_expr(), start_pc(0), length(0), is_parameter(false) + variablet( + const symbol_exprt &_symbol_expr, + std::size_t _start_pc, + std::size_t _length) + : symbol_expr(_symbol_expr), start_pc(_start_pc), length(_length) + { + } + + variablet( + const symbol_exprt &_symbol_expr, + std::size_t _start_pc, + std::size_t _length, + bool _is_parameter) + : symbol_expr(_symbol_expr), + start_pc(_start_pc), + length(_length), + is_parameter(_is_parameter) + { + } + + variablet( + const symbol_exprt &_symbol_expr, + std::size_t _start_pc, + std::size_t _length, + bool _is_parameter, + std::vector &&_holes) + : symbol_expr(_symbol_expr), + start_pc(_start_pc), + length(_length), + is_parameter(_is_parameter), + holes(std::move(_holes)) { } }; diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index 544d3500fa0..406171f13f2 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -773,7 +773,7 @@ void java_bytecode_convert_methodt::setup_local_variables( // to calculate which variable to use, one uses the address of the instruction // that uses the variable, the size of the instruction and the start_pc / // length values in the local variable table - for(const auto &v : vars_with_holes) + for(auto &v : vars_with_holes) { if(v.is_parameter) continue; @@ -807,12 +807,8 @@ void java_bytecode_convert_methodt::setup_local_variables( // Create a new local variable in the variables[] array, the result of // merging multiple local variables with equal name (parameters excluded) // into a single local variable with holes - variables[v.var.index].push_back(variablet()); - auto &newv=variables[v.var.index].back(); - newv.symbol_expr=result; - newv.start_pc=v.var.start_pc; - newv.length=v.var.length; - newv.holes=std::move(v.holes); + variables[v.var.index].emplace_back( + result, v.var.start_pc, v.var.length, false, std::move(v.holes)); // Register the local variable in the symbol table symbolt new_symbol; @@ -862,9 +858,7 @@ java_bytecode_convert_methodt::find_variable_for_slot( // with scope from 0 to SIZE_T_MAX // as it is at the end of the vector, it will only be taken into account // if no other variable is valid - size_t list_length=var_list.size(); - var_list.resize(list_length+1); - var_list[list_length].start_pc=0; - var_list[list_length].length=std::numeric_limits::max(); - return var_list[list_length]; + var_list.emplace_back( + symbol_exprt(irep_idt(), typet()), 0, std::numeric_limits::max()); + return var_list.back(); } diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 715e17787b6..ef720d8e3ce 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1559,14 +1559,14 @@ code_blockt java_string_library_preprocesst::make_object_get_class_code( loc); // > class1 = Class.forName(string1) + java_method_typet fun_type( + {java_method_typet::parametert(string_ptr_type)}, class_type); code_function_callt fun_call( class1, symbol_exprt( - "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;"), + "java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;", + std::move(fun_type)), {string1}); - const java_method_typet fun_type( - {java_method_typet::parametert(string_ptr_type)}, class_type); - fun_call.function().type()=fun_type; code.add(fun_call, loc); // > return class1; diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp index 7ff60da82c7..ee415768f18 100644 --- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp @@ -224,7 +224,7 @@ SCENARIO( simplify(sc.premise, empty_ns); simplify(sc.s0, empty_ns); simplify(sc.s1, empty_ns); - witnesses[sc] = generator.fresh_symbol("w", t.witness_type()); + witnesses.emplace(sc, generator.fresh_symbol("w", t.witness_type())); nc_axioms.push_back(sc); return accu + to_string(sc) + "\n\n"; }); @@ -296,7 +296,7 @@ SCENARIO( // Create witness for axiom string_constraint_generatort generator(empty_ns); std::unordered_map witnesses; - witnesses[vacuous] = generator.fresh_symbol("w", t.witness_type()); + witnesses.emplace(vacuous, generator.fresh_symbol("w", t.witness_type())); INFO("Original axiom:\n"); INFO(to_string(vacuous) + "\n\n"); @@ -346,7 +346,7 @@ SCENARIO( // Create witness for axiom string_constraint_generatort generator(empty_ns); std::unordered_map witnesses; - witnesses[trivial] = generator.fresh_symbol("w", t.witness_type()); + witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type())); INFO("Original axiom:\n"); INFO(to_string(trivial) + "\n\n"); @@ -397,7 +397,7 @@ SCENARIO( // Create witness for axiom string_constraint_generatort generator(empty_ns); std::unordered_map witnesses; - witnesses[trivial] = generator.fresh_symbol("w", t.witness_type()); + witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type())); INFO("Original axiom:\n"); INFO(to_string(trivial) + "\n\n"); @@ -450,7 +450,7 @@ SCENARIO( // Create witness for axiom string_constraint_generatort generator(empty_ns); std::unordered_map witnesses; - witnesses[trivial] = generator.fresh_symbol("w", t.witness_type()); + witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type())); INFO("Original axiom:\n"); INFO(to_string(trivial) + "\n\n"); @@ -501,7 +501,7 @@ SCENARIO( // Create witness for axiom string_constraint_generatort generator(empty_ns); std::unordered_map witnesses; - witnesses[trivial] = generator.fresh_symbol("w", t.witness_type()); + witnesses.emplace(trivial, generator.fresh_symbol("w", t.witness_type())); INFO("Original axiom:\n"); INFO(to_string(trivial) + "\n\n"); diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp index bf31bd8443a..51761280280 100644 --- a/src/analyses/locals.cpp +++ b/src/analyses/locals.cpp @@ -21,12 +21,13 @@ void localst::build(const goto_functiont &goto_function) if(it->is_decl()) { const code_declt &code_decl=to_code_decl(it->code); - locals_map[code_decl.get_identifier()] = code_decl.symbol(); + locals_map.emplace(code_decl.get_identifier(), code_decl.symbol()); } for(const auto ¶m : goto_function.type.parameters()) - locals_map[param.get_identifier()]= - symbol_exprt(param.get_identifier(), param.type()); + locals_map.emplace( + param.get_identifier(), + symbol_exprt(param.get_identifier(), param.type())); } void localst::output(std::ostream &out) const diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 5bf1767e6f5..39e1125fe90 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -635,9 +635,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) symbol_table.add(new_symbol); // produce the code that declares and initializes the symbol - symbol_exprt symbol_expr; - symbol_expr.set_identifier(temp_identifier); - symbol_expr.type() = new_symbol.type; + symbol_exprt symbol_expr(temp_identifier, new_symbol.type); code_declt declaration(symbol_expr); declaration.add_source_location() = size_source_location; diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index cb3a46d607a..bbaad3853ef 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -1451,13 +1451,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name( throw 0; } - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); code_typet t( {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype()); t.make_ellipsis(); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } @@ -1484,14 +1482,12 @@ void cpp_typecheckt::typecheck_expr_cpp_name( throw 0; } - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); const code_typet t( {code_typet::parametert(ptr_arg.type()), code_typet::parametert(signed_int_type())}, ptr_arg.type().subtype()); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } @@ -1518,15 +1514,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name( throw 0; } - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); const code_typet t( {code_typet::parametert(ptr_arg.type()), code_typet::parametert(ptr_arg.type().subtype()), code_typet::parametert(signed_int_type())}, empty_typet()); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } @@ -1553,15 +1547,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name( throw 0; } - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); const code_typet t( {code_typet::parametert(ptr_arg.type()), code_typet::parametert(ptr_arg.type().subtype()), code_typet::parametert(signed_int_type())}, ptr_arg.type().subtype()); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } @@ -1596,15 +1588,13 @@ void cpp_typecheckt::typecheck_expr_cpp_name( const exprt &ptr_arg=fargs.operands.front(); - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); const code_typet t( {code_typet::parametert(ptr_arg.type()), code_typet::parametert(ptr_arg.type()), code_typet::parametert(signed_int_type())}, empty_typet()); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } @@ -1645,16 +1635,14 @@ void cpp_typecheckt::typecheck_expr_cpp_name( const exprt &ptr_arg=fargs.operands.front(); - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); const code_typet t( {code_typet::parametert(ptr_arg.type()), code_typet::parametert(ptr_arg.type()), code_typet::parametert(ptr_arg.type()), code_typet::parametert(signed_int_type())}, empty_typet()); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } @@ -1700,9 +1688,6 @@ void cpp_typecheckt::typecheck_expr_cpp_name( const exprt &ptr_arg=fargs.operands.front(); - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); code_typet::parameterst parameters; parameters.push_back(code_typet::parametert(ptr_arg.type())); parameters.push_back(code_typet::parametert(ptr_arg.type())); @@ -1716,7 +1701,8 @@ void cpp_typecheckt::typecheck_expr_cpp_name( parameters.push_back(code_typet::parametert(signed_int_type())); parameters.push_back(code_typet::parametert(signed_int_type())); code_typet t(std::move(parameters), c_bool_type()); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } @@ -1745,13 +1731,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name( throw 0; } - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); code_typet t( {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype()); t.make_ellipsis(); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } @@ -1780,13 +1764,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name( throw 0; } - symbol_exprt result; - result.add_source_location()=source_location; - result.set_identifier(identifier); code_typet t( {code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype()); t.make_ellipsis(); - result.type()=t; + symbol_exprt result(identifier, t); + result.add_source_location() = source_location; expr.swap(result); return; } diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 4ad0a772465..916e614b888 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -2132,7 +2132,7 @@ bool cpp_typecheck_resolvet::disambiguate_functions( { // it's a constructor const typet &object_type=parameter.type().subtype(); - symbol_exprt object(object_type); + symbol_exprt object(irep_idt(), object_type); object.set(ID_C_lvalue, true); cpp_typecheck_fargst new_fargs(fargs); diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 46f921ff285..5f9b8caccc2 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -440,8 +440,8 @@ int linker_script_merget::ls_data2instructions( // Linker-defined symbol_exprt pointing to start address symbol_exprt start_sym(d["start-symbol"].value, pointer_type(char_type())); - linker_values[d["start-symbol"].value]=std::make_pair(start_sym, - array_start); + linker_values.emplace( + d["start-symbol"].value, std::make_pair(start_sym, array_start)); // Since the value of the pointer will be a random CBMC address, write a // note about the real address in the object file @@ -479,7 +479,8 @@ int linker_script_merget::ls_data2instructions( plus_exprt array_end(array_start, array_size_expr); symbol_exprt end_sym(d["end-symbol"].value, pointer_type(char_type())); - linker_values[d["end-symbol"].value]=std::make_pair(end_sym, array_end); + linker_values.emplace( + d["end-symbol"].value, std::make_pair(end_sym, array_end)); auto entry = std::find_if( to_json_array(data["addresses"]).begin(), @@ -578,7 +579,8 @@ int linker_script_merget::ls_data2instructions( exprt rhs_tc(rhs); rhs_tc.make_typecast(pointer_type(char_type())); - linker_values[irep_idt(d["sym"].value)]=std::make_pair(lhs, rhs_tc); + linker_values.emplace( + irep_idt(d["sym"].value), std::make_pair(lhs, rhs_tc)); code_assignt assign(lhs, rhs_tc); assign.add_source_location()=loc; @@ -641,7 +643,8 @@ int linker_script_merget::ls_data2instructions( exprt rhs_tc(rhs); rhs_tc.make_typecast(pointer_type(char_type())); - linker_values[irep_idt(d["sym"].value)]=std::make_pair(lhs, rhs_tc); + linker_values.emplace( + irep_idt(d["sym"].value), std::make_pair(lhs, rhs_tc)); code_assignt assign(lhs, rhs_tc); assign.add_source_location()=loc; diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index 7f29f3030f1..489d7bfc559 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -96,22 +96,18 @@ void _rw_set_loct::read_write_rec( if(r) { - entryt &entry=r_entries[object]; - entry.object=object; - entry.symbol_expr=symbol_expr; - entry.guard=guard.as_expr(); // should 'OR' + const auto &entry = + r_entries.emplace(object, entryt(symbol_expr, object, guard.as_expr())); - track_deref(entry, true); + track_deref(entry.first->second, true); } if(w) { - entryt &entry=w_entries[object]; - entry.object=object; - entry.symbol_expr=symbol_expr; - entry.guard=guard.as_expr(); // should 'OR' + const auto &entry = + w_entries.emplace(object, entryt(symbol_expr, object, guard.as_expr())); - track_deref(entry, false); + track_deref(entry.first->second, false); } } else if(expr.id()==ID_member) diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h index 2e050f8c5b6..b53478bdd45 100644 --- a/src/goto-instrument/rw_set.h +++ b/src/goto-instrument/rw_set.h @@ -48,7 +48,11 @@ class rw_set_baset irep_idt object; exprt guard; - entryt():guard(true_exprt()) + entryt( + const symbol_exprt &_symbol_expr, + const irep_idt &_object, + const exprt &_guard) + : symbol_expr(_symbol_expr), object(_object), guard(_guard) { } }; diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index 701485949d3..69ad8679d9e 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -121,9 +121,7 @@ void uninitializedt::add_assertions( const irep_idt new_identifier= id2string(identifier)+"#initialized"; - symbol_exprt symbol_expr; - symbol_expr.set_identifier(new_identifier); - symbol_expr.type()=bool_typet(); + symbol_exprt symbol_expr(new_identifier, bool_typet()); i1->type=DECL; i1->source_location=instruction.source_location; i1->code=code_declt(symbol_expr); diff --git a/src/goto-symex/memory_model.cpp b/src/goto-symex/memory_model.cpp index acc0e091f1d..5ad5dd3c13d 100644 --- a/src/goto-symex/memory_model.cpp +++ b/src/goto-symex/memory_model.cpp @@ -84,8 +84,7 @@ void memory_model_baset::read_from(symex_target_equationt &equation) symbol_exprt s=nondet_bool_symbol("rf"); // record the symbol - choice_symbols[ - std::make_pair(r, w)]=s; + choice_symbols.emplace(std::make_pair(r, w), s); // We rely on the fact that there is at least // one write event that has guard 'true'. diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 0d024c5f550..9427185beed 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -408,7 +408,7 @@ void goto_symext::locality( if(c_it != state.level1.current_names.end()) { - frame.old_level1[l0_name]=c_it->second; + frame.old_level1.emplace(l0_name, c_it->second); c_it->second = std::make_pair(ssa, frame_nr); } else diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index e9a145e20f0..cdb7dfc3d1c 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -645,9 +645,9 @@ void symex_target_equationt::convert_io( step.converted_io_args.push_back(arg); else { - symbol_exprt symbol; - symbol.type()=arg.type(); - symbol.set_identifier("symex::io::"+std::to_string(io_count++)); + const irep_idt identifier = + "symex::io::" + std::to_string(io_count++); + symbol_exprt symbol(identifier, arg.type()); equal_exprt eq(arg, symbol); merge_irep(eq); diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index ea3e3e0c3d1..b66b8a1c9aa 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -500,9 +500,8 @@ exprt smt2_parsert::function_application() { const symbol_exprt symbol_expr( smt2_tokenizer.get_buffer(), bool_typet()); - auto &named_term = named_terms[symbol_expr.get_identifier()]; - named_term.term = term; - named_term.name = symbol_expr; + named_terms.emplace( + symbol_expr.get_identifier(), named_termt(term, symbol_expr)); } else throw error("invalid name attribute, expected symbol"); diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 68dba0e384d..2fdcc3751e1 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -47,6 +47,13 @@ class smt2_parsert struct named_termt { + /// Default-constructing a symbol_exprt is deprecated, thus make sure we + /// always construct a named_termt from an initialized \p _name + named_termt(const exprt &_term, const symbol_exprt &_name) + : term(_term), name(_name) + { + } + exprt term; symbol_exprt name; }; diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index f1b158f7d6f..4e680d35568 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -735,8 +735,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() const typet &index_type = rtype.size().type(); return array_typet(index_type, infinity_exprt(index_type)); }(); - not_contain_witnesses[nc_axiom] = - generator.fresh_symbol("not_contains_witness", witness_type); + not_contain_witnesses.emplace( + nc_axiom, generator.fresh_symbol("not_contains_witness", witness_type)); } for(const exprt &lemma : generator.constraints.existential) diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 4a9547cc267..5454f07c5ba 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -16,15 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com class ssa_exprt:public symbol_exprt { public: - ssa_exprt() - { - set(ID_C_SSA_symbol, true); - } - /// Constructor /// \param expr: Expression to be converted to SSA symbol - explicit ssa_exprt(const exprt &expr): - symbol_exprt(expr.type()) + explicit ssa_exprt(const exprt &expr) : symbol_exprt(irep_idt(), expr.type()) { set(ID_C_SSA_symbol, true); add(ID_expression, expr); diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp index 38c451e553e..170233a3a4e 100644 --- a/unit/util/expr_cast/expr_cast.cpp +++ b/unit/util/expr_cast/expr_cast.cpp @@ -19,7 +19,7 @@ Author: Nathan Phillips SCENARIO("expr_dynamic_cast", "[core][utils][expr_cast][expr_dynamic_cast]") { - symbol_exprt symbol_expr; + symbol_exprt symbol_expr("dummy", empty_typet()); GIVEN("A const exprt reference to a symbolt") {