Type the operand of code_declt

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 =

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())

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 &param : goto_function.type.parameters())

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));

src/cpp/cpp_util.cpp

@@ -11,12 +11,12 @@
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
-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;
 }

src/cpp/cpp_util.h

@@ -13,7 +13,7 @@
 #include <util/expr.h>
 #include <util/symbol.h>
 
-exprt cpp_symbol_expr(const symbolt &symbol);
+symbol_exprt cpp_symbol_expr(const symbolt &symbol);
 
 inline void already_typechecked(irept &irep)
 {

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())
     {

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<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::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<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::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<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
+      it != distinguishers.end();
       ++it)
   {
     path_val[*it]=program.eval(*it).is_true();

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<exprt> distinguishers;
+  std::list<symbol_exprt> distinguishers;
   expr_sett modified;
   goto_programt fixed;
   std::list<distinguish_valuest> accelerated_paths;

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';

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())
     {

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;

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);
 

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)

src/util/std_code.cpp

@@ -13,11 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #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();

src/util/std_code.h

@@ -12,9 +12,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <list>
 
-#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<symbol_exprt &>(op0());
   }
 
-  exprt &symbol()
+  const symbol_exprt &symbol() const
   {
-    return op0();
+    return static_cast<const symbol_exprt &>(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<code_declt>(const exprt &base)