Merge pull request #2818 from diffblue/trace-with-arguments

rename 'identifier' to 'function_identifier'

Author: Daniel Kroening

src/goto-programs/goto_trace.cpp

@@ -66,7 +66,7 @@ void goto_trace_stept::output(
   if(is_assert() || is_assume() || is_goto())
     out << " (" << cond_value << ")";
   else if(is_function_call() || is_function_return())
-    out << ' ' << identifier;
+    out << ' ' << function_identifier;
 
   if(hidden)
     out << " hidden";
@@ -444,14 +444,14 @@ void show_goto_trace(
     case goto_trace_stept::typet::FUNCTION_CALL:
       function_depth++;
       if(options.show_function_calls)
-        out << "\n#### Function call: " << step.identifier << " (depth "
-            << function_depth << ") ####\n";
+        out << "\n#### Function call: " << step.function_identifier
+            << " (depth " << function_depth << ") ####\n";
       break;
     case goto_trace_stept::typet::FUNCTION_RETURN:
       function_depth--;
       if(options.show_function_calls)
-        out << "\n#### Function return: " << step.identifier << " (depth "
-            << function_depth << ") ####\n";
+        out << "\n#### Function return: " << step.function_identifier
+            << " (depth " << function_depth << ") ####\n";
       break;
     case goto_trace_stept::typet::SPAWN:
     case goto_trace_stept::typet::MEMORY_BARRIER:

src/goto-programs/goto_trace.h

@@ -120,7 +120,7 @@ class goto_trace_stept
   bool formatted;
 
   // for function call/return
-  irep_idt identifier;
+  irep_idt function_identifier;
 
   /*! \brief outputs the trace step in ASCII to a given stream
   */

src/goto-programs/interpreter.cpp

@@ -771,8 +771,8 @@ void interpretert::execute_function_call()
 #if 0
   const memory_cellt &cell=memory[address];
 #endif
-  const irep_idt &identifier=address_to_identifier(address);
-  trace_step.identifier=identifier;
+  const irep_idt &identifier = address_to_identifier(address);
+  trace_step.function_identifier = identifier;
 
   const goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(identifier);

src/goto-programs/json_goto_trace.cpp

@@ -274,10 +274,10 @@ void convert_return(
   json_call_return["internal"] = jsont::json_boolean(step.internal);
   json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
 
-  const symbolt &symbol = ns.lookup(step.identifier);
+  const symbolt &symbol = ns.lookup(step.function_identifier);
   json_objectt &json_function = json_call_return["function"].make_object();
   json_function["displayName"] = json_stringt(symbol.display_name());
-  json_function["identifier"] = json_stringt(step.identifier);
+  json_function["identifier"] = json_stringt(step.function_identifier);
   json_function["sourceLocation"] = json(symbol.location);
 
   if(!location.is_null())

src/goto-programs/xml_goto_trace.cpp

@@ -190,11 +190,12 @@ void convert(
         xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
         xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
 
-        const symbolt &symbol=ns.lookup(step.identifier);
+        const symbolt &symbol = ns.lookup(step.function_identifier);
         xmlt &xml_function=xml_call_return.new_element("function");
         xml_function.set_attribute(
           "display_name", id2string(symbol.display_name()));
-        xml_function.set_attribute("identifier", id2string(step.identifier));
+        xml_function.set_attribute(
+          "identifier", id2string(step.function_identifier));
         xml_function.new_element()=xml(symbol.location);
 
         if(xml_location.name!="")

src/goto-symex/build_goto_trace.cpp

@@ -309,7 +309,7 @@ void build_goto_trace(
       goto_trace_step.format_string = SSA_step.format_string;
       goto_trace_step.io_id = SSA_step.io_id;
       goto_trace_step.formatted = SSA_step.formatted;
-      goto_trace_step.identifier = SSA_step.identifier;
+      goto_trace_step.function_identifier = SSA_step.function_identifier;
 
       // update internal field for specific variables in the counterexample
       update_internal_field(SSA_step, goto_trace_step, ns);

src/goto-symex/symex_target.h

@@ -104,13 +104,13 @@ class symex_targett
   // record a function call
   virtual void function_call(
     const exprt &guard,
-    const irep_idt &identifier,
+    const irep_idt &function_identifier,
     const sourcet &source)=0;
 
   // record return from a function
   virtual void function_return(
     const exprt &guard,
-    const irep_idt &identifier,
+    const irep_idt &function_identifier,
     const sourcet &source)=0;
 
   // just record a location

src/goto-symex/symex_target_equation.cpp

@@ -209,33 +209,33 @@ void symex_target_equationt::location(
 /// just record a location
 void symex_target_equationt::function_call(
   const exprt &guard,
-  const irep_idt &identifier,
+  const irep_idt &function_identifier,
   const sourcet &source)
 {
   SSA_steps.push_back(SSA_stept());
   SSA_stept &SSA_step=SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.type=goto_trace_stept::typet::FUNCTION_CALL;
-  SSA_step.source=source;
-  SSA_step.identifier=identifier;
+  SSA_step.guard = guard;
+  SSA_step.type = goto_trace_stept::typet::FUNCTION_CALL;
+  SSA_step.source = source;
+  SSA_step.function_identifier = function_identifier;
 
   merge_ireps(SSA_step);
 }
 
 /// just record a location
 void symex_target_equationt::function_return(
   const exprt &guard,
-  const irep_idt &identifier,
+  const irep_idt &function_identifier,
   const sourcet &source)
 {
   SSA_steps.push_back(SSA_stept());
   SSA_stept &SSA_step=SSA_steps.back();
 
-  SSA_step.guard=guard;
-  SSA_step.type=goto_trace_stept::typet::FUNCTION_RETURN;
-  SSA_step.source=source;
-  SSA_step.identifier=identifier;
+  SSA_step.guard = guard;
+  SSA_step.type = goto_trace_stept::typet::FUNCTION_RETURN;
+  SSA_step.source = source;
+  SSA_step.function_identifier = function_identifier;
 
   merge_ireps(SSA_step);
 }

src/goto-symex/symex_target_equation.h

@@ -74,13 +74,13 @@ class symex_target_equationt:public symex_targett
   // record a function call
   virtual void function_call(
     const exprt &guard,
-    const irep_idt &identifier,
+    const irep_idt &function_identifier,
     const sourcet &source);
 
   // record return from a function
   virtual void function_return(
     const exprt &guard,
-    const irep_idt &identifier,
+    const irep_idt &function_identifier,
     const sourcet &source);
 
   // just record a location
@@ -230,7 +230,7 @@ class symex_target_equationt:public symex_targett
     std::list<exprt> converted_io_args;
 
     // for function call/return
-    irep_idt identifier;
+    irep_idt function_identifier;
 
     // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
     unsigned atomic_section_id=0;