From 1a79a11372221797bd76de189c73eb63c239872e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Mar 2017 17:24:19 +0000 Subject: [PATCH] stack depth instrumentation: __CPROVER_initialize may be empty Do not attempt to use information from the first instruction in __CPROVER_initialize as there need not be any such instruction. --- src/goto-instrument/stack_depth.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 9784d648f39..581d5c1bb74 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -107,8 +107,8 @@ void stack_depth( goto_programt::targett it=init.insert_before(first); it->make_assignment(); it->code=code_assignt(sym, from_integer(0, sym.type())); - it->source_location=first->source_location; - it->function=first->function; + // no suitable value for source location -- omitted + it->function = INITIALIZE_FUNCTION; // update counters etc. goto_model.goto_functions.update();