Skip to content

Commit 5fca235

Browse files
Remove obsolete rebuild_goto_start_function class
Removes the need for templates and dependency on lazy_goto_modelt.
1 parent b215331 commit 5fca235

File tree

4 files changed

+40
-89
lines changed

4 files changed

+40
-89
lines changed

src/goto-programs/initialize_goto_model.cpp

Lines changed: 17 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,9 @@ Author: Daniel Kroening, kroening@kroening.com
2020
#include <util/options.h>
2121
#include <util/unicode.h>
2222

23-
#include <langapi/mode.h>
2423
#include <langapi/language.h>
24+
#include <langapi/language_file.h>
25+
#include <langapi/mode.h>
2526

2627
#include <goto-programs/rebuild_goto_start_function.h>
2728
#include <util/exception_utils.h>
@@ -151,11 +152,21 @@ goto_modelt initialize_goto_model(
151152

152153
if(binaries_provided_start && options.is_set("function"))
153154
{
154-
// Rebuild the entry-point, using the language annotation of the
155-
// existing __CPROVER_start function:
156-
rebuild_goto_start_functiont rebuild_existing_start(
157-
options, goto_model, msg.get_message_handler());
158-
entry_point_generation_failed=rebuild_existing_start();
155+
// Get the language annotation of the existing __CPROVER_start function.
156+
std::unique_ptr<languaget> language = get_entry_point_language(
157+
goto_model.symbol_table, options, message_handler);
158+
159+
// To create a new entry point we must first remove the old one
160+
remove_existing_entry_point(goto_model.symbol_table);
161+
162+
// Create the new entry-point
163+
entry_point_generation_failed =
164+
language->generate_support_functions(goto_model.symbol_table);
165+
166+
// Remove the function from the goto functions so it is copied back in
167+
// from the symbol table during goto_convert
168+
if(!entry_point_generation_failed)
169+
goto_model.unload(goto_functionst::entry_point());
159170
}
160171
else if(!binaries_provided_start)
161172
{

src/goto-programs/lazy_goto_model.cpp

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -201,11 +201,21 @@ void lazy_goto_modelt::initialize(
201201

202202
if(binaries_provided_start && options.is_set("function"))
203203
{
204-
// Rebuild the entry-point, using the language annotation of the
205-
// existing __CPROVER_start function:
206-
rebuild_lazy_goto_start_functiont rebuild_existing_start(
207-
options, *this, message_handler);
208-
entry_point_generation_failed=rebuild_existing_start();
204+
// Get the language annotation of the existing __CPROVER_start function.
205+
std::unique_ptr<languaget> language =
206+
get_entry_point_language(symbol_table, options, message_handler);
207+
208+
// To create a new entry point we must first remove the old one
209+
remove_existing_entry_point(symbol_table);
210+
211+
// Create the new entry-point
212+
entry_point_generation_failed =
213+
language->generate_support_functions(symbol_table);
214+
215+
// Remove the function from the goto functions so it is copied back in
216+
// from the symbol table during goto_convert
217+
if(!entry_point_generation_failed)
218+
unload(goto_functionst::entry_point());
209219
}
210220
else if(!binaries_provided_start)
211221
{

src/goto-programs/rebuild_goto_start_function.cpp

Lines changed: 2 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -19,50 +19,9 @@ Author: Thomas Kiley, thomas@diffblue.com
1919
#include <langapi/mode.h>
2020
#include <langapi/language.h>
2121

22-
#include <memory>
23-
24-
/// To rebuild the _start function in the event the program was compiled into
25-
/// GOTO with a different entry function selected.
26-
/// \param options: Command-line options
27-
/// \param goto_model: The goto functions (to replace the body of the _start
28-
/// function) and symbol table (to replace the _start function symbol) of the
29-
/// program.
30-
/// \param message_handler: The message handler to report any messages with
31-
template <typename maybe_lazy_goto_modelt>
32-
rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::
33-
rebuild_goto_start_function_baset(
34-
const optionst &options,
35-
maybe_lazy_goto_modelt &goto_model,
36-
message_handlert &message_handler)
37-
: messaget(message_handler), options(options), goto_model(goto_model)
38-
{
39-
}
40-
41-
/// To rebuild the _start function in the event the program was compiled into
42-
/// GOTO with a different entry function selected. It works by discarding the
43-
/// _start symbol and GOTO function and calling on the relevant languaget to
44-
/// generate the _start function again.
45-
/// \return Returns true if either the symbol is not found, or something went
46-
/// wrong with generating the start_function. False otherwise.
47-
template<typename maybe_lazy_goto_modelt>
48-
bool rebuild_goto_start_function_baset<maybe_lazy_goto_modelt>::operator()()
49-
{
50-
std::unique_ptr<languaget> language = get_entry_point_language(
51-
goto_model.symbol_table, options, get_message_handler());
22+
#include <goto-programs/goto_functions.h>
5223

53-
// To create a new entry point we must first remove the old one
54-
remove_existing_entry_point(goto_model.symbol_table);
55-
56-
bool return_code=
57-
language->generate_support_functions(goto_model.symbol_table);
58-
59-
// Remove the function from the goto functions so it is copied back in
60-
// from the symbol table during goto_convert
61-
if(!return_code)
62-
goto_model.unload(goto_functionst::entry_point());
63-
64-
return return_code;
65-
}
24+
#include <memory>
6625

6726
std::unique_ptr<languaget> get_entry_point_language(
6827
const symbol_table_baset &symbol_table,
@@ -109,6 +68,3 @@ void remove_existing_entry_point(symbol_table_baset &symbol_table)
10968
symbol_table.remove(entry_point_symbol);
11069
}
11170
}
112-
113-
template class rebuild_goto_start_function_baset<goto_modelt>;
114-
template class rebuild_goto_start_function_baset<lazy_goto_modelt>;

src/goto-programs/rebuild_goto_start_function.h

Lines changed: 6 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -12,39 +12,21 @@ Author: Thomas Kiley, thomas@diffblue.com
1212
#ifndef CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
1313
#define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
1414

15-
#include <util/message.h>
16-
class optionst;
17-
18-
#include "lazy_goto_model.h"
15+
#include <memory>
1916

17+
#include <util/irep.h>
2018

21-
class symbol_tablet;
22-
class goto_functionst;
19+
class languaget;
20+
class message_handlert;
21+
class optionst;
22+
class symbol_table_baset;
2323

2424
#define OPT_FUNCTIONS \
2525
"(function):"
2626

2727
#define HELP_FUNCTIONS \
2828
" --function name set main function name\n"
2929

30-
template<typename maybe_lazy_goto_modelt>
31-
class rebuild_goto_start_function_baset: public messaget
32-
{
33-
public:
34-
rebuild_goto_start_function_baset(
35-
const optionst &options,
36-
maybe_lazy_goto_modelt &goto_model,
37-
message_handlert &message_handler);
38-
39-
bool operator()();
40-
41-
private:
42-
irep_idt get_entry_point_mode() const;
43-
44-
const optionst &options;
45-
maybe_lazy_goto_modelt &goto_model;
46-
};
47-
4830
/// Eliminate the existing entry point function symbol and any symbols created
4931
/// in that scope from the \p symbol_table.
5032
void remove_existing_entry_point(symbol_table_baset &);
@@ -63,12 +45,4 @@ std::unique_ptr<languaget> get_entry_point_language(
6345
const optionst &options,
6446
message_handlert &message_handler);
6547

66-
// NOLINTNEXTLINE(readability/namespace) using required for templates
67-
using rebuild_goto_start_functiont =
68-
rebuild_goto_start_function_baset<goto_modelt>;
69-
70-
// NOLINTNEXTLINE(readability/namespace) using required for templates
71-
using rebuild_lazy_goto_start_functiont =
72-
rebuild_goto_start_function_baset<lazy_goto_modelt>;
73-
7448
#endif // CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H

0 commit comments

Comments
 (0)