Skip to content

rename 'identifier' to 'function_identifier' #2818

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Aug 22, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions src/goto-programs/goto_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/goto_trace.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
*/
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/interpreter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/json_goto_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand Down
5 changes: 3 additions & 2 deletions src/goto-programs/xml_goto_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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!="")
Expand Down
2 changes: 1 addition & 1 deletion src/goto-symex/build_goto_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
4 changes: 2 additions & 2 deletions src/goto-symex/symex_target.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
20 changes: 10 additions & 10 deletions src/goto-symex/symex_target_equation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down
6 changes: 3 additions & 3 deletions src/goto-symex/symex_target_equation.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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;
Expand Down