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

Daniel Kroening · Daniel Kroening · commit 4e89e0112836 · 2018-05-19T13:24:36.000+01:00
diff --git a/src/analyses/ai.cpp b/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);
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
@@ -263,7 +263,7 @@ 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));
+      ns.lookup(to_symbol_type(result_type));
 
     result_type=followed_type_symbol.type;
     qualifiers+=c_qualifierst(followed_type_symbol.type);
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -1663,7 +1663,7 @@ std::string expr2ct::convert_symbol(
   const symbol_exprt &src,
   unsigned &precedence)
 {
-  const irep_idt &id=src.get(ID_identifier);
+  const irep_idt &id=src.get_identifier();
   std::string dest;
 
   if(src.operands().size()==1 &&
diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #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>
 
@@ -25,12 +26,12 @@ static std::string type2name(
   const namespacet &ns,
   symbol_numbert &symbol_number);
 
-static std::string type2name_symbol(
-  const typet &type,
+static std::string type2name_tag(
+  const tag_typet &type,
   const namespacet &ns,
   symbol_numbert &symbol_number)
 {
-  const irep_idt &identifier=type.get(ID_identifier);
+  const irep_idt &identifier=type.get_identifier();
 
   const symbolt *symbol;
 
@@ -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
@@ -192,7 +193,7 @@ static std::string type2name(
           type.id()==ID_union_tag)
   {
     parent_is_sym_check=true;
-    result+=type2name_symbol(type, ns, symbol_number);
+    result+=type2name_tag(to_tag_type(type), ns, symbol_number);
   }
   else if(type.id()==ID_struct ||
           type.id()==ID_union)
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -29,11 +29,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 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)
 {
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
@@ -658,16 +658,17 @@ 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=lookup(identifier);
 
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
@@ -609,38 +609,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(
@@ -655,12 +655,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);
 
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
@@ -376,7 +376,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=lookup(identifier);
 
     std::string new_base_name=id2string(new_symbol.base_name);
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
@@ -838,7 +838,9 @@ void interpretert::execute_function_call()
   else
   {
     list_input_varst::iterator it=
-        function_input_vars.find(function_call.function().get(ID_identifier));
+      function_input_vars.find(
+        to_symbol_expr(function_call.function()).get_identifier());
+
     if(it!=function_input_vars.end())
     {
       mp_vectort value;
@@ -852,6 +854,7 @@ void interpretert::execute_function_call()
       it->second.pop_front();
       return;
     }
+
     if(show)
       error() << "no body for "+id2string(identifier) << eom;
   }
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -1086,7 +1086,7 @@ mp_integer interpretert::evaluate_address(
     const irep_idt &identifier=
       is_ssa_expr(expr) ?
       to_ssa_expr(expr).get_original_name() :
-      expr.get(ID_identifier);
+      to_symbol_expr(expr).get_identifier();
 
     interpretert::memory_mapt::const_iterator m_it1=
       memory_map.find(identifier);
diff --git a/src/goto-programs/json_goto_trace.cpp b/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,
diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
@@ -73,7 +73,7 @@ exprt remove_const_function_pointerst::replace_const_symbols(
     if(is_const_expression(expression))
     {
       const symbolt &symbol=
-        *symbol_table.lookup(expression.get(ID_identifier));
+        *symbol_table.lookup(to_symbol_expr(expression).get_identifier());
       if(symbol.type.id()!=ID_code)
       {
         const exprt &symbol_value=symbol.value;
diff --git a/src/goto-programs/remove_unused_functions.cpp b/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);
         }
       }
     }
diff --git a/src/memory-models/mm2cpp.cpp b/src/memory-models/mm2cpp.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <ostream>
 
 #include <util/std_code.h>
+#include <util/std_expr.h>
 
 class mm2cppt
 {
@@ -53,7 +54,7 @@ void mm2cppt::check_acyclic(const exprt &expr, unsigned indent)
 {
   if(expr.id()==ID_symbol)
   {
-    const irep_idt &identifier=expr.get(ID_identifier);
+    const irep_idt &identifier=to_symbol_expr(expr).get_identifier();
     let_valuest::const_iterator v_it=let_values.find(identifier);
     if(v_it!=let_values.end())
       check_acyclic(v_it->second, indent);
@@ -152,7 +153,7 @@ void mm2cppt::instruction2cpp(const codet &code, unsigned indent)
         assert(it->operands().size()==2);
         if(it->op0().id()==ID_symbol)
         {
-          irep_idt identifier=it->op0().get(ID_identifier);
+          irep_idt identifier=to_symbol_expr(it->op0()).get_identifier();
           let_values[identifier]=it->op1();
         }
         else
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
@@ -351,7 +351,7 @@ void value_set_fivrnst::get_value_set_rec(
   {
     // just keep a reference to the ident in the set
     // (if it exists)
-    irep_idt ident = expr.get_string(ID_identifier)+suffix;
+    irep_idt ident = id2string(to_symbol_expr(expr).get_identifier())+suffix;
 
     if(has_prefix(id2string(ident), alloc_adapter_prefix))
     {
@@ -1012,7 +1012,7 @@ void value_set_fivrnst::assign_rec(
 
   if(lhs.id()==ID_symbol)
   {
-    const irep_idt &identifier=lhs.get(ID_identifier);
+    const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
 
     if(has_prefix(id2string(identifier),
                   "value_set::dynamic_object") ||
diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp
diff --git a/src/util/find_macros.cpp b/src/util/find_macros.cpp
diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp
diff --git a/src/util/rename_symbol.cpp b/src/util/rename_symbol.cpp
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp

Original file line number	Diff line number	Diff line change
`@@ -462,7 +462,7 @@ bool ai_baset::do_function_call_rec(`
`462`	`462`
`463`	`463`	`if(function.id()==ID_symbol)`
`464`	`464`	`{`
`465`		`- const irep_idt &identifier=function.get(ID_identifier);`
	`465`	`+ const irep_idt &identifier=to_symbol_expr(function).get_identifier();`
`466`	`466`
`467`	`467`	`goto_functionst::function_mapt::const_iterator it=`
`468`	`468`	`goto_functions.function_map.find(identifier);`
Original file line number	Diff line number	Diff line change
`@@ -263,7 +263,7 @@ typet c_typecastt::follow_with_qualifiers(const typet &src_type)`
`263`	`263`	`while(result_type.id()==ID_symbol)`
`264`	`264`	`{`
`265`	`265`	`const symbolt &followed_type_symbol=`
`266`		`- ns.lookup(result_type.get(ID_identifier));`
	`266`	`+ ns.lookup(to_symbol_type(result_type));`
`267`	`267`
`268`	`268`	`result_type=followed_type_symbol.type;`
`269`	`269`	`qualifiers+=c_qualifierst(followed_type_symbol.type);`
Original file line number	Diff line number	Diff line change
`@@ -1663,7 +1663,7 @@ std::string expr2ct::convert_symbol(`
`1663`	`1663`	`const symbol_exprt &src,`
`1664`	`1664`	`unsigned &precedence)`
`1665`	`1665`	`{`
`1666`		`- const irep_idt &id=src.get(ID_identifier);`
	`1666`	`+ const irep_idt &id=src.get_identifier();`
`1667`	`1667`	`std::string dest;`
`1668`	`1668`
`1669`	`1669`	`if(src.operands().size()==1 &&`
Original file line number	Diff line number	Diff line change
`@@ -658,16 +658,17 @@ void goto_convertt::convert_decl(`
`658`	`658`	`goto_programt &dest,`
`659`	`659`	`const irep_idt &mode)`
`660`	`660`	`{`
`661`		`- const exprt &op0=code.op0();`
	`661`	`+ const exprt &op=code.symbol();`
`662`	`662`
`663`		`- if(op0.id()!=ID_symbol)`
	`663`	`+ if(op.id()!=ID_symbol)`
`664`	`664`	`{`
`665`		`- error().source_location=op0.find_source_location();`
`666`		`- error() << "decl statement expects symbol as first operand" << eom;`
	`665`	`+ error().source_location=op.find_source_location();`
	`666`	`+ error() << "decl statement expects symbol as operand" << eom;`
`667`	`667`	`throw 0;`
`668`	`668`	`}`
`669`	`669`
`670`		`- const irep_idt &identifier=op0.get(ID_identifier);`
	`670`	`+ const irep_idt &identifier=`
	`671`	`+ to_symbol_expr(op).get_identifier();`
`671`	`672`
`672`	`673`	`const symbolt &symbol=lookup(identifier);`
`673`	`674`
Original file line number	Diff line number	Diff line change
`@@ -376,7 +376,7 @@ void goto_convertt::remove_function_call(`
`376`	`376`
`377`	`377`	`if(expr.op0().id()==ID_symbol)`
`378`	`378`	`{`
`379`		`- const irep_idt &identifier=expr.op0().get(ID_identifier);`
	`379`	`+ const irep_idt &identifier=to_symbol_expr(expr.op0()).get_identifier();`
`380`	`380`	`const symbolt &symbol=lookup(identifier);`
`381`	`381`
`382`	`382`	`std::string new_base_name=id2string(new_symbol.base_name);`
Original file line number	Diff line number	Diff line change
`@@ -838,7 +838,9 @@ void interpretert::execute_function_call()`
`838`	`838`	`else`
`839`	`839`	`{`
`840`	`840`	`list_input_varst::iterator it=`
`841`		`- function_input_vars.find(function_call.function().get(ID_identifier));`
	`841`	`+ function_input_vars.find(`
	`842`	`+ to_symbol_expr(function_call.function()).get_identifier());`
	`843`	`+`
`842`	`844`	`if(it!=function_input_vars.end())`
`843`	`845`	`{`
`844`	`846`	`mp_vectort value;`
`@@ -852,6 +854,7 @@ void interpretert::execute_function_call()`
`852`	`854`	`it->second.pop_front();`
`853`	`855`	`return;`
`854`	`856`	`}`
	`857`	`+`
`855`	`858`	`if(show)`
`856`	`859`	`error() << "no body for "+id2string(identifier) << eom;`
`857`	`860`	`}`