Skip to content

Commit d902133

Browse files
committed
Move function body generation before goto_check() instrumentation
1 parent 2aed98a commit d902133

File tree

1 file changed

+13
-13
lines changed

1 file changed

+13
-13
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1185,6 +1185,19 @@ void goto_instrument_parse_optionst::instrument_goto_program()
11851185
remove_skip(goto_model);
11861186
}
11871187

1188+
if(cmdline.isset("generate-function-body"))
1189+
{
1190+
auto generate_implementation = generate_function_bodies_factory(
1191+
cmdline.get_value("generate-function-body-options"),
1192+
goto_model.symbol_table,
1193+
*message_handler);
1194+
generate_function_bodies(
1195+
std::regex(cmdline.get_value("generate-function-body")),
1196+
*generate_implementation,
1197+
goto_model,
1198+
*message_handler);
1199+
}
1200+
11881201
// add generic checks, if needed
11891202
goto_check(options, goto_model);
11901203

@@ -1487,19 +1500,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
14871500
throw 0;
14881501
}
14891502

1490-
if(cmdline.isset("generate-function-body"))
1491-
{
1492-
auto generate_implementation = generate_function_bodies_factory(
1493-
cmdline.get_value("generate-function-body-options"),
1494-
goto_model.symbol_table,
1495-
*message_handler);
1496-
generate_function_bodies(
1497-
std::regex(cmdline.get_value("generate-function-body")),
1498-
*generate_implementation,
1499-
goto_model,
1500-
*message_handler);
1501-
}
1502-
15031503
// aggressive slicer
15041504
if(cmdline.isset("aggressive-slice"))
15051505
{

0 commit comments

Comments
 (0)