diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index aa22e28d1de..8886a13641c 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -683,7 +683,7 @@ void add_pointer_to_array_association( loc, ID_java, symbol_table); - exprt return_expr = return_sym.symbol_expr(); + auto return_expr = return_sym.symbol_expr(); code.add(code_declt(return_expr), loc); code.add( code_assign_function_application( @@ -715,7 +715,7 @@ void add_array_to_length_association( loc, ID_java, symbol_table); - const exprt return_expr = return_sym.symbol_expr(); + const auto return_expr = return_sym.symbol_expr(); code.add(code_declt(return_expr), loc); code.add( code_assign_function_application( @@ -747,7 +747,7 @@ void add_character_set_constraint( PRECONDITION(pointer.type().id() == ID_pointer); symbolt &return_sym = get_fresh_aux_symbol( java_int_type(), "cnstr_added", "cnstr_added", loc, ID_java, symbol_table); - const exprt return_expr = return_sym.symbol_expr(); + const auto return_expr = return_sym.symbol_expr(); code.add(code_declt(return_expr), loc); const constant_exprt char_set_expr(char_set, string_typet()); code.add( @@ -790,7 +790,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function( loc, ID_java, symbol_table); - const exprt return_code = return_code_sym.symbol_expr(); + const auto return_code = return_code_sym.symbol_expr(); code.add(code_declt(return_code), loc); const refined_string_exprt string_expr = @@ -1232,7 +1232,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( std::string aux_name="tmp_"+id2string(type_name); symbolt symbol=get_fresh_aux_symbol( value_type, aux_name, aux_name, loc, ID_java, symbol_table); - exprt value=symbol.symbol_expr(); + auto value = symbol.symbol_expr(); // Check that the type of the object is in the symbol table, // otherwise there is no safe way of finding its value. @@ -1340,8 +1340,9 @@ exprt java_string_library_preprocesst::make_argument_for_format( std::string tmp_name="tmp_"+id2string(name); symbolt field_symbol = get_fresh_aux_symbol( type, id2string(function_id), tmp_name, loc, ID_java, symbol_table); - field_expr=field_symbol.symbol_expr(); - code.add(code_declt(field_expr), loc); + auto field_symbol_expr = field_symbol.symbol_expr(); + field_expr = field_symbol_expr; + code.add(code_declt(field_symbol_expr), loc); } else field_expr = diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 0779eeda196..e912f1469e6 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -93,7 +93,7 @@ void constant_propagator_domaint::transform( if(from->is_decl()) { const code_declt &code_decl=to_code_decl(from->code); - const symbol_exprt &symbol=to_symbol_expr(code_decl.symbol()); + const symbol_exprt &symbol = code_decl.symbol(); values.set_to_top(symbol); } else if(from->is_assign()) diff --git a/src/analyses/locals.cpp b/src/analyses/locals.cpp index 8d146f9713f..bf31bd8443a 100644 --- a/src/analyses/locals.cpp +++ b/src/analyses/locals.cpp @@ -21,8 +21,7 @@ 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()]= - to_symbol_expr(code_decl.symbol()); + locals_map[code_decl.get_identifier()] = code_decl.symbol(); } for(const auto ¶m : goto_function.type.parameters()) diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index cfbe24fe27d..6cbc5396ddb 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -100,7 +100,7 @@ void cpp_typecheckt::typecheck_try_catch(codet &code) to_code_decl(to_code(code.op0().op0())); // get the type - const typet &type=code_decl.op0().type(); + const typet &type = code_decl.symbol().type(); // annotate exception ID op.set(ID_exception_id, cpp_exception_id(type, *this)); diff --git a/src/cpp/cpp_util.cpp b/src/cpp/cpp_util.cpp index 6992e4b1fe6..8bf3f2ef3c5 100644 --- a/src/cpp/cpp_util.cpp +++ b/src/cpp/cpp_util.cpp @@ -11,12 +11,12 @@ #include #include -exprt cpp_symbol_expr(const symbolt &symbol) +symbol_exprt cpp_symbol_expr(const symbolt &symbol) { symbol_exprt tmp(symbol.name, symbol.type); if(symbol.is_lvalue) tmp.set(ID_C_lvalue, true); - return std::move(tmp); + return tmp; } diff --git a/src/cpp/cpp_util.h b/src/cpp/cpp_util.h index 87a667b3a6a..ec07ac4169d 100644 --- a/src/cpp/cpp_util.h +++ b/src/cpp/cpp_util.h @@ -13,7 +13,7 @@ #include #include -exprt cpp_symbol_expr(const symbolt &symbol); +symbol_exprt cpp_symbol_expr(const symbolt &symbol); inline void already_typechecked(irept &irep) { diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp index 1e916a5250a..c2ac6a75026 100644 --- a/src/goto-diff/change_impact.cpp +++ b/src/goto-diff/change_impact.cpp @@ -80,8 +80,8 @@ void full_slicert::operator()( jumps.push_back(e_it->second); else if(e_it->first->is_decl()) { - const exprt &s=to_code_decl(e_it->first->code).symbol(); - decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second); + const auto &s=to_code_decl(e_it->first->code).symbol(); + decl_dead[s.get_identifier()].push(e_it->second); } else if(e_it->first->is_dead()) { diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 3d5927264b1..b94b616ea31 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -546,8 +546,8 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial( // Start building the program. Begin by decl'ing each of the // master distinguishers. - for(std::list::iterator it=distinguishers.begin(); - it!=distinguishers.end(); + for(std::list::iterator it = distinguishers.begin(); + it != distinguishers.end(); ++it) { program.add_instruction(DECL)->code=code_declt(*it); @@ -888,8 +888,8 @@ void disjunctive_polynomial_accelerationt::build_fixed() // Create shadow distinguisher variables. These guys identify the path that // is taken through the fixed-path body. - for(std::list::iterator it=distinguishers.begin(); - it!=distinguishers.end(); + for(std::list::iterator it = distinguishers.begin(); + it != distinguishers.end(); ++it) { exprt &distinguisher=*it; @@ -1006,8 +1006,8 @@ void disjunctive_polynomial_accelerationt::record_path( { distinguish_valuest path_val; - for(std::list::iterator it=distinguishers.begin(); - it!=distinguishers.end(); + for(std::list::iterator it = distinguishers.begin(); + it != distinguishers.end(); ++it) { path_val[*it]=program.eval(*it).is_true(); diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h index 33c23ad7bd6..9fef71f077b 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h @@ -98,7 +98,7 @@ class disjunctive_polynomial_accelerationt acceleration_utilst utils; exprt loop_counter; distinguish_mapt distinguishing_points; - std::list distinguishers; + std::list distinguishers; expr_sett modified; goto_programt fixed; std::list accelerated_paths; diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 6113ec6133c..5e8b3d56d96 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -894,7 +894,9 @@ void dump_ct::convert_global_variable( } if(!func.empty() && !symbol.is_extern) - local_static_decls[symbol.name]=d; + { + local_static_decls.emplace(symbol.name, d); + } else if(!symbol.value.is_nil()) { os << "// " << symbol.name << '\n'; diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 07d3864473a..1947de6a9b5 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -310,8 +310,8 @@ void full_slicert::operator()( jumps.push_back(e_it->second); else if(e_it->first->is_decl()) { - const exprt &s=to_code_decl(e_it->first->code).symbol(); - decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second); + const auto &s = to_code_decl(e_it->first->code).symbol(); + decl_dead[s.get_identifier()].push(e_it->second); } else if(e_it->first->is_dead()) { diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index f4989e7d99d..e286897c0bc 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -458,7 +458,7 @@ goto_programt::const_targett goto_program2codet::convert_decl( codet &dest) { code_declt d=to_code_decl(target->code); - symbol_exprt &symbol=to_symbol_expr(d.symbol()); + symbol_exprt &symbol = d.symbol(); goto_programt::const_targett next=target; ++next; diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 18eed256dda..4e2d9536eb5 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -607,7 +607,7 @@ void goto_convertt::convert_decl( goto_programt &dest, const irep_idt &mode) { - const irep_idt &identifier = to_symbol_expr(code.symbol()).get_identifier(); + const irep_idt &identifier = code.get_identifier(); const symbolt &symbol = ns.lookup(identifier); diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp index 3942382be1a..70c2d21ee5b 100644 --- a/src/goto-symex/symex_decl.cpp +++ b/src/goto-symex/symex_decl.cpp @@ -29,7 +29,7 @@ void goto_symext::symex_decl(statet &state) // we handle the decl with only one operand PRECONDITION(code.operands().size() == 1); - symex_decl(state, to_symbol_expr(to_code_decl(code).symbol())); + symex_decl(state, to_code_decl(code).symbol()); } void goto_symext::symex_decl(statet &state, const symbol_exprt &expr) diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp index 50b8e2d1f4a..41f82c4f32c 100644 --- a/src/util/std_code.cpp +++ b/src/util/std_code.cpp @@ -13,11 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_expr.h" -const irep_idt &code_declt::get_identifier() const -{ - return to_symbol_expr(symbol()).get_identifier(); -} - const irep_idt &code_deadt::get_identifier() const { return to_symbol_expr(symbol()).get_identifier(); diff --git a/src/util/std_code.h b/src/util/std_code.h index 6e17b9566a9..8c37f5bb7f9 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "expr.h" #include "expr_cast.h" #include "invariant.h" +#include "std_expr.h" /// Data structure for representing an arbitrary statement in a program. Every /// specific type of statement (e.g. block of statements, assignment, @@ -276,28 +276,25 @@ inline code_assignt &to_code_assign(codet &code) class code_declt:public codet { public: - DEPRECATED("use code_declt(symbol) instead") - code_declt():codet(ID_decl) + explicit code_declt(const symbol_exprt &symbol) : codet(ID_decl) { - operands().resize(1); + add_to_operands(symbol); } - explicit code_declt(const exprt &symbol):codet(ID_decl) + symbol_exprt &symbol() { - add_to_operands(symbol); + return static_cast(op0()); } - exprt &symbol() + const symbol_exprt &symbol() const { - return op0(); + return static_cast(op0()); } - const exprt &symbol() const + const irep_idt &get_identifier() const { - return op0(); + return symbol().get_identifier(); } - - const irep_idt &get_identifier() const; }; template<> inline bool can_cast_expr(const exprt &base)