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.

Author: tautschnig

src/goto-instrument/stack_depth.cpp

@@ -92,16 +92,17 @@ void stack_depth(
 
   const exprt depth_expr(from_integer(depth, sym.type()));
 
+  const irep_idt init_name=CPROVER_PREFIX "initialize";
+
   Forall_goto_functions(f_it, goto_model.goto_functions)
     if(f_it->second.body_available() &&
-        f_it->first!=CPROVER_PREFIX "initialize" &&
-        f_it->first!=goto_functionst::entry_point())
+       f_it->first!=init_name &&
+       f_it->first!=goto_functionst::entry_point())
       stack_depth(f_it->second.body, sym, depth, depth_expr);
 
   // initialize depth to 0
   goto_functionst::function_mapt::iterator
-    i_it=goto_model.goto_functions.function_map.find(
-      CPROVER_PREFIX "initialize");
+    i_it=goto_model.goto_functions.function_map.find(init_name);
   DATA_INVARIANT(
     i_it!=goto_model.goto_functions.function_map.end(),
     "__CPROVER_initialize must exist");
@@ -111,8 +112,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=init_name;
 
   // update counters etc.
   goto_model.goto_functions.update();