Skip to content

Commit 0f2549d

Browse files
Petr BauchPetr Bauch
authored andcommitted
Moved goto_model post-condition to instrumentation (fix regression)
1 parent 15997b4 commit 0f2549d

File tree

2 files changed

+4
-3
lines changed

2 files changed

+4
-3
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -903,6 +903,10 @@ void goto_instrument_parse_optionst::get_goto_program()
903903
throw 0;
904904

905905
config.set(cmdline);
906+
907+
POSTCONDITION(
908+
goto_model.goto_functions.function_map.count(
909+
goto_functionst::entry_point()) != 0);
906910
}
907911

908912
void goto_instrument_parse_optionst::instrument_goto_program()

src/goto-programs/read_bin_goto_object.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -158,9 +158,6 @@ static bool read_bin_goto_object_v4(
158158

159159
functions.compute_location_numbers();
160160

161-
POSTCONDITION(
162-
functions.function_map.count(goto_functionst::entry_point()) != 0);
163-
164161
return false;
165162
}
166163

0 commit comments

Comments
 (0)