From 4da6a43d9049703b046abf8165b69a997b19a6a5 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 17 Feb 2019 10:35:01 +0000 Subject: [PATCH 1/3] Supply function identifier for return from bodyless functions There is no source location for bodyless functions. We have to record it separately. --- src/goto-symex/symex_function_call.cpp | 6 ++++-- src/goto-symex/symex_target.h | 8 ++++++-- src/goto-symex/symex_target_equation.cpp | 2 ++ src/goto-symex/symex_target_equation.h | 7 +++++-- 4 files changed, 17 insertions(+), 6 deletions(-) diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index c576ea72864..a28087c2003 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -286,7 +286,8 @@ void goto_symext::symex_function_call_code( no_body(identifier); // record the return - target.function_return(state.guard.as_expr(), state.source, hidden); + target.function_return( + state.guard.as_expr(), identifier, state.source, hidden); if(call.lhs().is_not_nil()) { @@ -374,7 +375,8 @@ void goto_symext::symex_end_of_function(statet &state) const bool hidden = state.top().hidden_function; // first record the return - target.function_return(state.guard.as_expr(), state.source, hidden); + target.function_return( + state.guard.as_expr(), state.source.function_id, state.source, hidden); // then get rid of the frame pop_frame(state); diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h index ca1cb755e7c..3eddaf1dd8a 100644 --- a/src/goto-symex/symex_target.h +++ b/src/goto-symex/symex_target.h @@ -152,11 +152,15 @@ class symex_targett /// Record return from a function. /// \param guard: Precondition for returning from a function + /// \param function_id: Name of the function from which we return /// \param source: Pointer to location in the input GOTO program of this /// \param hidden: Should this step be recorded as hidden? /// function return - virtual void - function_return(const exprt &guard, const sourcet &source, bool hidden) = 0; + virtual void function_return( + const exprt &guard, + const irep_idt &function_id, + const sourcet &source, + bool hidden) = 0; /// Record a location. /// \param guard: Precondition for reaching this location diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 65afe8c2794..8075528bc09 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -204,6 +204,7 @@ void symex_target_equationt::function_call( void symex_target_equationt::function_return( const exprt &guard, + const irep_idt &function_id, const sourcet &source, const bool hidden) { @@ -211,6 +212,7 @@ void symex_target_equationt::function_return( SSA_stept &SSA_step=SSA_steps.back(); SSA_step.guard = guard; + SSA_step.called_function = function_id; SSA_step.hidden = hidden; merge_ireps(SSA_step); diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index b563e980697..998a87959cd 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/src/goto-symex/symex_target_equation.h @@ -85,8 +85,11 @@ class symex_target_equationt:public symex_targett bool hidden); /// \copydoc symex_targett::function_return() - virtual void - function_return(const exprt &guard, const sourcet &source, bool hidden); + virtual void function_return( + const exprt &guard, + const irep_idt &function_id, + const sourcet &source, + bool hidden); /// \copydoc symex_targett::location() virtual void location( From dc8c7c316800e16ac6beb986a795f410be5b3212 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 17 Feb 2019 10:32:06 +0000 Subject: [PATCH 2/3] Use correct function return identifier of functions without body in trace output --- src/goto-programs/json_goto_trace.cpp | 4 +--- src/goto-programs/xml_goto_trace.cpp | 4 ++-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 46b761530c1..2e27f766b5d 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -263,9 +263,7 @@ 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 irep_idt &function_identifier = - (step.type == goto_trace_stept::typet::FUNCTION_CALL) ? step.called_function - : step.function_id; + const irep_idt &function_identifier = step.called_function; const symbolt &symbol = ns.lookup(function_identifier); json_call_return["function"] = diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 61164356bef..4af88697d0f 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -186,11 +186,11 @@ 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.function_id); + const symbolt &symbol = ns.lookup(step.called_function); 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.function_id)); + xml_function.set_attribute("identifier", id2string(symbol.name)); xml_function.new_element()=xml(symbol.location); if(xml_location.name!="") From b06e63ab7f5446b8bc423b9087265f9ed1ac79fa Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 19 Feb 2019 21:16:52 +0000 Subject: [PATCH 3/3] Add regression test for bodyless function return The function_return output should have the correct identifier. --- regression/cbmc/function-return-no-body1/main.c | 9 +++++++++ regression/cbmc/function-return-no-body1/test.desc | 11 +++++++++++ 2 files changed, 20 insertions(+) create mode 100644 regression/cbmc/function-return-no-body1/main.c create mode 100644 regression/cbmc/function-return-no-body1/test.desc diff --git a/regression/cbmc/function-return-no-body1/main.c b/regression/cbmc/function-return-no-body1/main.c new file mode 100644 index 00000000000..bf0e0685d83 --- /dev/null +++ b/regression/cbmc/function-return-no-body1/main.c @@ -0,0 +1,9 @@ +#include + +void no_body(); + +void main() +{ + no_body(); + assert(0); +} diff --git a/regression/cbmc/function-return-no-body1/test.desc b/regression/cbmc/function-return-no-body1/test.desc new file mode 100644 index 00000000000..fffcd09289b --- /dev/null +++ b/regression/cbmc/function-return-no-body1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--xml-ui +activate-multi-line-match +EXIT=10 +SIGNAL=0 +VERIFICATION FAILED +