Skip to content

Commit 417e0cc

Browse files
Merge pull request #4225 from peterschrammel/function-return-without-body
Use correct function ID for return from function without body
2 parents 88c9629 + b06e63a commit 417e0cc

File tree

8 files changed

+40
-11
lines changed

8 files changed

+40
-11
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include <assert.h>
2+
3+
void no_body();
4+
5+
void main()
6+
{
7+
no_body();
8+
assert(0);
9+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--xml-ui
4+
activate-multi-line-match
5+
EXIT=10
6+
SIGNAL=0
7+
VERIFICATION FAILED
8+
<function_call hidden="false" step_nr="18" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
9+
<function_return hidden="false" step_nr="19" thread="0">\n\s*<function display_name="no_body" identifier="no_body">
10+
--
11+
^warning: ignoring

src/goto-programs/json_goto_trace.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -263,9 +263,7 @@ void convert_return(
263263
json_call_return["internal"] = jsont::json_boolean(step.internal);
264264
json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
265265

266-
const irep_idt &function_identifier =
267-
(step.type == goto_trace_stept::typet::FUNCTION_CALL) ? step.called_function
268-
: step.function_id;
266+
const irep_idt &function_identifier = step.called_function;
269267

270268
const symbolt &symbol = ns.lookup(function_identifier);
271269
json_call_return["function"] =

src/goto-programs/xml_goto_trace.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -186,11 +186,11 @@ void convert(
186186
xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
187187
xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
188188

189-
const symbolt &symbol = ns.lookup(step.function_id);
189+
const symbolt &symbol = ns.lookup(step.called_function);
190190
xmlt &xml_function=xml_call_return.new_element("function");
191191
xml_function.set_attribute(
192192
"display_name", id2string(symbol.display_name()));
193-
xml_function.set_attribute("identifier", id2string(step.function_id));
193+
xml_function.set_attribute("identifier", id2string(symbol.name));
194194
xml_function.new_element()=xml(symbol.location);
195195

196196
if(xml_location.name!="")

src/goto-symex/symex_function_call.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -286,7 +286,8 @@ void goto_symext::symex_function_call_code(
286286
no_body(identifier);
287287

288288
// record the return
289-
target.function_return(state.guard.as_expr(), state.source, hidden);
289+
target.function_return(
290+
state.guard.as_expr(), identifier, state.source, hidden);
290291

291292
if(call.lhs().is_not_nil())
292293
{
@@ -374,7 +375,8 @@ void goto_symext::symex_end_of_function(statet &state)
374375
const bool hidden = state.top().hidden_function;
375376

376377
// first record the return
377-
target.function_return(state.guard.as_expr(), state.source, hidden);
378+
target.function_return(
379+
state.guard.as_expr(), state.source.function_id, state.source, hidden);
378380

379381
// then get rid of the frame
380382
pop_frame(state);

src/goto-symex/symex_target.h

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -152,11 +152,15 @@ class symex_targett
152152

153153
/// Record return from a function.
154154
/// \param guard: Precondition for returning from a function
155+
/// \param function_id: Name of the function from which we return
155156
/// \param source: Pointer to location in the input GOTO program of this
156157
/// \param hidden: Should this step be recorded as hidden?
157158
/// function return
158-
virtual void
159-
function_return(const exprt &guard, const sourcet &source, bool hidden) = 0;
159+
virtual void function_return(
160+
const exprt &guard,
161+
const irep_idt &function_id,
162+
const sourcet &source,
163+
bool hidden) = 0;
160164

161165
/// Record a location.
162166
/// \param guard: Precondition for reaching this location

src/goto-symex/symex_target_equation.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,13 +204,15 @@ void symex_target_equationt::function_call(
204204

205205
void symex_target_equationt::function_return(
206206
const exprt &guard,
207+
const irep_idt &function_id,
207208
const sourcet &source,
208209
const bool hidden)
209210
{
210211
SSA_steps.emplace_back(source, goto_trace_stept::typet::FUNCTION_RETURN);
211212
SSA_stept &SSA_step=SSA_steps.back();
212213

213214
SSA_step.guard = guard;
215+
SSA_step.called_function = function_id;
214216
SSA_step.hidden = hidden;
215217

216218
merge_ireps(SSA_step);

src/goto-symex/symex_target_equation.h

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,8 +85,11 @@ class symex_target_equationt:public symex_targett
8585
bool hidden);
8686

8787
/// \copydoc symex_targett::function_return()
88-
virtual void
89-
function_return(const exprt &guard, const sourcet &source, bool hidden);
88+
virtual void function_return(
89+
const exprt &guard,
90+
const irep_idt &function_id,
91+
const sourcet &source,
92+
bool hidden);
9093

9194
/// \copydoc symex_targett::location()
9295
virtual void location(

0 commit comments

Comments
 (0)