Skip to content

Commit c6f1430

Browse files
author
thk123
committed
Ensure symex and goto-analyzer regenerate functions
1 parent e37d3d5 commit c6f1430

File tree

1 file changed

+16
-0
lines changed

1 file changed

+16
-0
lines changed

src/goto-programs/initialize_goto_model.cpp

+16
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ Author: Daniel Kroening, [email protected]
2121
#include <langapi/mode.h>
2222
#include <langapi/language_ui.h>
2323

24+
#include <goto-programs/rebuild_goto_start_function.h>
25+
2426
#include "goto_convert_functions.h"
2527
#include "read_goto_binary.h"
2628

@@ -131,6 +133,20 @@ bool initialize_goto_model(
131133
return true;
132134
}
133135

136+
if(cmdline.isset("function"))
137+
{
138+
const std::string &function_id=cmdline.get_value("function");
139+
rebuild_goto_start_functiont start_function_rebuilder(
140+
msg.get_message_handler(),
141+
goto_model.symbol_table,
142+
goto_model.goto_functions);
143+
144+
if(start_function_rebuilder(function_id))
145+
{
146+
return 6;
147+
}
148+
}
149+
134150
msg.status() << "Generating GOTO Program" << messaget::eom;
135151

136152
goto_convert(

0 commit comments

Comments
 (0)