code_declt is now typed

Author: Daniel Kroening

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -668,7 +668,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(
@@ -700,7 +700,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(
@@ -732,7 +732,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(
@@ -775,7 +775,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 =
@@ -1217,7 +1217,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.
@@ -1325,8 +1325,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

@@ -91,7 +91,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/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/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.insert(std::pair<irep_idt, code_declt>(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/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);
+    copy_to_operands(symbol);
   }
 
-  explicit code_declt(const exprt &symbol):codet(ID_decl)
+  symbol_exprt &symbol()
   {
-    copy_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)