Use get_identifier() instead of get(ID_identifier) on symbols

src/analyses/ai.cpp

@@ -462,7 +462,7 @@ bool ai_baset::do_function_call_rec(
 
   if(function.id()==ID_symbol)
   {
-    const irep_idt &identifier=function.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(function).get_identifier();
 
     goto_functionst::function_mapt::const_iterator it=
       goto_functions.function_map.find(identifier);

src/analyses/flow_insensitive_analysis.cpp

@@ -293,7 +293,7 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
 
   if(function.id()==ID_symbol)
   {
-    const irep_idt &identifier=function.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(function).get_identifier();
 
     if(recursion_set.find(identifier)!=recursion_set.end())
     {

src/analyses/invariant_set.cpp

@@ -143,7 +143,7 @@ std::string inv_object_storet::build_string(const exprt &expr) const
   }
 
   if(expr.id()==ID_symbol)
-    return expr.get_string(ID_identifier);
+    return id2string(to_symbol_expr(expr).get_identifier());
 
   return "";
 }

src/analyses/static_analysis.cpp

@@ -328,7 +328,7 @@ void static_analysis_baset::do_function_call_rec(
 
   if(function.id()==ID_symbol)
   {
-    const irep_idt &identifier=function.get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(function).get_identifier();
 
     if(recursion_set.find(identifier)!=recursion_set.end())
     {

src/ansi-c/c_typecast.cpp

@@ -262,8 +262,8 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)
 
   while(result_type.id()==ID_symbol)
   {
-    const symbolt &followed_type_symbol=
-      ns.lookup(result_type.get(ID_identifier));
+    const symbolt &followed_type_symbol =
+      ns.lookup(to_symbol_type(result_type));
 
     result_type=followed_type_symbol.type;
     qualifiers+=c_qualifierst(followed_type_symbol.type);

src/ansi-c/type2name.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/symbol_table.h>
 
@@ -180,7 +181,7 @@ static std::string type2name(
     const array_typet &t=to_array_type(type);
     mp_integer size;
     if(t.size().id()==ID_symbol)
-      result+="ARR"+id2string(t.size().get(ID_identifier));
+      result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
     else if(to_integer(t.size(), size))
       result+="ARR?";
     else

src/cpp/cpp_is_pod.cpp

@@ -82,8 +82,8 @@ bool cpp_typecheckt::cpp_is_pod(const typet &type) const
   }
   else if(type.id()==ID_symbol)
   {
-    const symbolt &symb=lookup(type.get(ID_identifier));
-    assert(symb.is_type);
+    const symbolt &symb = lookup(to_symbol_type(type));
+    DATA_INVARIANT(symb.is_type, "type symbol is a type");
     return cpp_is_pod(symb.type);
   }
 

src/cpp/cpp_typecheck_resolve.cpp

@@ -170,9 +170,9 @@ void cpp_typecheck_resolvet::remove_duplicates(
     irep_idt id;
 
     if(it->id()==ID_symbol)
-      id=it->get(ID_identifier);
+      id = to_symbol_expr(*it).get_identifier();
     else if(it->id()==ID_type && it->type().id()==ID_symbol)
-      id=it->type().get(ID_identifier);
+      id = to_symbol_type(it->type()).get_identifier();
 
     if(id=="")
     {
@@ -2041,8 +2041,8 @@ void cpp_typecheck_resolvet::apply_template_args(
   if(expr.id()!=ID_symbol)
     return; // templates are always symbols
 
-  const symbolt &template_symbol=
-    cpp_typecheck.lookup(expr.get(ID_identifier));
+  const symbolt &template_symbol =
+    cpp_typecheck.lookup(to_symbol_expr(expr).get_identifier());
 
   if(!template_symbol.type.get_bool(ID_is_template))
     return;
@@ -2239,7 +2239,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
         const typet &type=pcomp.type();
         assert(type.id()!=ID_struct);
         if(type.id()==ID_symbol)
-          identifier=type.get(ID_identifier);
+          identifier = to_symbol_type(type).get_identifier();
         else
           continue;
       }
@@ -2261,7 +2261,7 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
           break;
         }
         else if(symbol.type.id()==ID_symbol)
-          identifier=symbol.type.get(ID_identifier);
+          identifier = to_symbol_type(symbol.type).get_identifier();
         else
           break;
       }

src/cpp/template_map.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 #include <ostream>
 
 #include <util/invariant.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 
 void template_mapt::apply(typet &type) const
 {
@@ -39,8 +41,8 @@ void template_mapt::apply(typet &type) const
   }
   else if(type.id()==ID_symbol)
   {
-    type_mapt::const_iterator m_it=
-      type_map.find(type.get(ID_identifier));
+    type_mapt::const_iterator m_it =
+      type_map.find(to_symbol_type(type).get_identifier());
 
     if(m_it!=type_map.end())
     {
@@ -73,8 +75,8 @@ void template_mapt::apply(exprt &expr) const
 
   if(expr.id()==ID_symbol)
   {
-    expr_mapt::const_iterator m_it=
-      expr_map.find(expr.get(ID_identifier));
+    expr_mapt::const_iterator m_it =
+      expr_map.find(to_symbol_expr(expr).get_identifier());
 
     if(m_it!=expr_map.end())
     {

src/goto-programs/builtin_functions.cpp

@@ -29,11 +29,11 @@ Author: Daniel Kroening, [email protected]
 
 void goto_convertt::do_prob_uniform(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  const irep_idt &identifier=function.get(ID_identifier);
+  const irep_idt &identifier = function.get_identifier();
 
   // make it a side effect if there is an LHS
   if(arguments.size()!=2)
@@ -107,11 +107,11 @@ void goto_convertt::do_prob_uniform(
 
 void goto_convertt::do_prob_coin(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  const irep_idt &identifier=function.get(ID_identifier);
+  const irep_idt &identifier = function.get_identifier();
 
   // make it a side effect if there is an LHS
   if(arguments.size()!=2)
@@ -184,11 +184,11 @@ void goto_convertt::do_prob_coin(
 
 void goto_convertt::do_printf(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  const irep_idt &f_id=function.get(ID_identifier);
+  const irep_idt &f_id = function.get_identifier();
 
   if(f_id==CPROVER_PREFIX "printf" ||
      f_id=="printf")
@@ -219,11 +219,11 @@ void goto_convertt::do_printf(
 
 void goto_convertt::do_scanf(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
-  const irep_idt &f_id=function.get(ID_identifier);
+  const irep_idt &f_id = function.get_identifier();
 
   if(f_id==CPROVER_PREFIX "scanf")
   {
@@ -364,7 +364,7 @@ void goto_convertt::do_output(
 
 void goto_convertt::do_atomic_begin(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
@@ -388,7 +388,7 @@ void goto_convertt::do_atomic_begin(
 
 void goto_convertt::do_atomic_end(
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {
@@ -597,7 +597,7 @@ exprt goto_convertt::get_array_argument(const exprt &src)
 void goto_convertt::do_array_op(
   const irep_idt &id,
   const exprt &lhs,
-  const exprt &function,
+  const symbol_exprt &function,
   const exprt::operandst &arguments,
   goto_programt &dest)
 {

src/goto-programs/goto_convert.cpp

@@ -657,16 +657,16 @@ void goto_convertt::convert_decl(
   goto_programt &dest,
   const irep_idt &mode)
 {
-  const exprt &op0=code.op0();
+  const exprt &op = code.symbol();
 
-  if(op0.id()!=ID_symbol)
+  if(op.id() != ID_symbol)
   {
-    error().source_location=op0.find_source_location();
-    error() << "decl statement expects symbol as first operand" << eom;
+    error().source_location = op.find_source_location();
+    error() << "decl statement expects symbol as operand" << eom;
     throw 0;
   }
 
-  const irep_idt &identifier=op0.get(ID_identifier);
+  const irep_idt &identifier = to_symbol_expr(op).get_identifier();
 
   const symbolt &symbol = ns.lookup(identifier);
 

src/goto-programs/goto_convert_class.h

@@ -606,38 +606,38 @@ class goto_convertt:public messaget
   // some built-in functions
   void do_atomic_begin(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_atomic_end(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_create_thread(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_array_equal(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &rhs,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_array_op(
     const irep_idt &id,
     const exprt &lhs,
-    const exprt &function,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_printf(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_scanf(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_input(
@@ -652,12 +652,12 @@ class goto_convertt:public messaget
     goto_programt &dest);
   void do_prob_coin(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
   void do_prob_uniform(
     const exprt &lhs,
-    const exprt &rhs,
+    const symbol_exprt &function,
     const exprt::operandst &arguments,
     goto_programt &dest);
 

src/goto-programs/goto_convert_side_effect.cpp

@@ -373,7 +373,7 @@ void goto_convertt::remove_function_call(
 
   if(expr.op0().id()==ID_symbol)
   {
-    const irep_idt &identifier=expr.op0().get(ID_identifier);
+    const irep_idt &identifier = to_symbol_expr(expr.op0()).get_identifier();
     const symbolt &symbol = ns.lookup(identifier);
 
     new_base_name+='_';

src/goto-programs/interpreter.cpp

@@ -837,8 +837,9 @@ void interpretert::execute_function_call()
   }
   else
   {
-    list_input_varst::iterator it=
-        function_input_vars.find(function_call.function().get(ID_identifier));
+    list_input_varst::iterator it = function_input_vars.find(
+      to_symbol_expr(function_call.function()).get_identifier());
+
     if(it!=function_input_vars.end())
     {
       mp_vectort value;
@@ -852,6 +853,7 @@ void interpretert::execute_function_call()
       it->second.pop_front();
       return;
     }
+
     if(show)
       error() << "no body for "+id2string(identifier) << eom;
   }

src/goto-programs/interpreter_evaluate.cpp

@@ -1083,10 +1083,9 @@ mp_integer interpretert::evaluate_address(
 {
   if(expr.id()==ID_symbol)
   {
-    const irep_idt &identifier=
-      is_ssa_expr(expr) ?
-      to_ssa_expr(expr).get_original_name() :
-      expr.get(ID_identifier);
+    const irep_idt &identifier = is_ssa_expr(expr)
+                                   ? to_ssa_expr(expr).get_original_name()
+                                   : to_symbol_expr(expr).get_identifier();
 
     interpretert::memory_mapt::const_iterator m_it1=
       memory_map.find(identifier);

src/goto-programs/json_goto_trace.cpp

@@ -107,7 +107,8 @@ void convert_decl(
       {
         if(expr.id() == ID_symbol)
         {
-          const symbolt &symbol = ns.lookup(expr.get(ID_identifier));
+          const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
+
           if(expr.find(ID_C_base_name).is_not_nil())
             INVARIANT(
               expr.find(ID_C_base_name).id() == symbol.base_name,

src/goto-programs/remove_const_function_pointers.cpp

@@ -72,8 +72,8 @@ exprt remove_const_function_pointerst::replace_const_symbols(
   {
     if(is_const_expression(expression))
     {
-      const symbolt &symbol=
-        *symbol_table.lookup(expression.get(ID_identifier));
+      const symbolt &symbol =
+        *symbol_table.lookup(to_symbol_expr(expression).get_identifier());
       if(symbol.type.id()!=ID_code)
       {
         const exprt &symbol_value=symbol.value;

src/goto-programs/remove_unused_functions.cpp

@@ -81,9 +81,10 @@ void find_used_functions(
           // check that this is actually a simple call
           assert(call.function().id()==ID_symbol);
 
-          find_used_functions(call.function().get(ID_identifier),
-                              functions,
-                              seen);
+          const irep_idt &identifier =
+            to_symbol_expr(call.function()).get_identifier();
+
+          find_used_functions(identifier, functions, seen);
         }
       }
     }