Skip to content

Commit 1a79a11

Browse files
committed
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.
1 parent a7690ba commit 1a79a11

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/goto-instrument/stack_depth.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -107,8 +107,8 @@ void stack_depth(
107107
goto_programt::targett it=init.insert_before(first);
108108
it->make_assignment();
109109
it->code=code_assignt(sym, from_integer(0, sym.type()));
110-
it->source_location=first->source_location;
111-
it->function=first->function;
110+
// no suitable value for source location -- omitted
111+
it->function = INITIALIZE_FUNCTION;
112112

113113
// update counters etc.
114114
goto_model.goto_functions.update();

0 commit comments

Comments
 (0)