-
Notifications
You must be signed in to change notification settings - Fork 273
/
Copy pathrebuild_goto_start_function.cpp
68 lines (52 loc) · 1.95 KB
/
rebuild_goto_start_function.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
/*******************************************************************\
Module: Goto Programs
Author: Thomas Kiley, [email protected]
\*******************************************************************/
/// \file
/// Goto Programs Author: Thomas Kiley, [email protected]
#include "rebuild_goto_start_function.h"
#include <util/prefix.h>
#include <util/symbol_table_base.h>
#include <goto-programs/goto_functions.h>
#include <langapi/language.h>
#include <langapi/mode.h>
#include <memory>
std::unique_ptr<languaget> get_entry_point_language(
const symbol_table_baset &symbol_table,
const optionst &options,
message_handlert &message_handler)
{
const irep_idt &mode = get_entry_point_mode(symbol_table);
// Get the relevant languaget to generate the new entry point with.
std::unique_ptr<languaget> language = get_language_from_mode(mode);
// This might fail if the driver program hasn't registered that language.
INVARIANT(language, "No language found for mode: " + id2string(mode));
language->set_language_options(options, message_handler);
return language;
}
const irep_idt &get_entry_point_mode(const symbol_table_baset &symbol_table)
{
const symbolt ¤t_entry_point =
symbol_table.lookup_ref(goto_functionst::entry_point());
return current_entry_point.mode;
}
void remove_existing_entry_point(symbol_table_baset &symbol_table)
{
// Remove the function itself
symbol_table.remove(goto_functionst::entry_point());
// And any symbols created in the scope of the entry point
std::vector<irep_idt> entry_point_symbols;
for(const auto &symbol_entry : symbol_table.symbols)
{
const bool is_entry_point_symbol=
has_prefix(
id2string(symbol_entry.first),
id2string(goto_functionst::entry_point()));
if(is_entry_point_symbol)
entry_point_symbols.push_back(symbol_entry.first);
}
for(const irep_idt &entry_point_symbol : entry_point_symbols)
{
symbol_table.remove(entry_point_symbol);
}
}