cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
rebuild_goto_start_function.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Goto Programs
4
5
Author: Thomas Kiley, thomas@diffblue.com
6
7
\*******************************************************************/
8
11
12
#include "
rebuild_goto_start_function.h
"
13
14
#include <
util/prefix.h
>
15
#include <
util/symbol_table_base.h
>
16
17
#include <
goto-programs/goto_functions.h
>
18
19
#include <
langapi/language.h
>
20
#include <
langapi/mode.h
>
21
22
#include <memory>
23
24
std::unique_ptr<languaget>
get_entry_point_language
(
25
const
symbol_table_baset
&symbol_table,
26
const
optionst
&options,
27
message_handlert
&message_handler)
28
{
29
const
irep_idt
&mode =
get_entry_point_mode
(symbol_table);
30
31
// Get the relevant languaget to generate the new entry point with.
32
std::unique_ptr<languaget> language =
get_language_from_mode
(mode);
33
// This might fail if the driver program hasn't registered that language.
34
INVARIANT
(language,
"No language found for mode: "
+
id2string
(mode));
35
language->set_language_options(options, message_handler);
36
return
language;
37
}
38
39
const
irep_idt
&
get_entry_point_mode
(
const
symbol_table_baset
&symbol_table)
40
{
41
const
symbolt
¤t_entry_point =
42
symbol_table.
lookup_ref
(
goto_functionst::entry_point
());
43
return
current_entry_point.
mode
;
44
}
45
46
void
remove_existing_entry_point
(
symbol_table_baset
&symbol_table)
47
{
48
// Remove the function itself
49
symbol_table.
remove
(
goto_functionst::entry_point
());
50
51
// And any symbols created in the scope of the entry point
52
std::vector<irep_idt> entry_point_symbols;
53
for
(
const
auto
&symbol_entry : symbol_table.
symbols
)
54
{
55
const
bool
is_entry_point_symbol=
56
has_prefix
(
57
id2string
(symbol_entry.first),
58
id2string
(
goto_functionst::entry_point
()));
59
60
if
(is_entry_point_symbol)
61
entry_point_symbols.push_back(symbol_entry.first);
62
}
63
64
for
(
const
irep_idt
&entry_point_symbol : entry_point_symbols)
65
{
66
symbol_table.
remove
(entry_point_symbol);
67
}
68
}
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition
goto_functions.h:97
message_handlert
Definition
message.h:27
optionst
Definition
options.h:23
symbol_table_baset
The symbol table base class interface.
Definition
symbol_table_base.h:23
symbol_table_baset::remove
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Definition
symbol_table_base.cpp:27
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition
symbol_table_base.h:31
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition
symbol_table_base.h:105
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::mode
irep_idt mode
Language mode.
Definition
symbol.h:49
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition
converter.cpp:13
goto_functions.h
Goto Programs with Functions.
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
language.h
Abstract interface to support a programming language.
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition
mode.cpp:51
mode.h
prefix.h
remove_existing_entry_point
void remove_existing_entry_point(symbol_table_baset &symbol_table)
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
Definition
rebuild_goto_start_function.cpp:46
get_entry_point_mode
const irep_idt & get_entry_point_mode(const symbol_table_baset &symbol_table)
Find out the mode of the current entry point to determine the mode of the replacement entry point.
Definition
rebuild_goto_start_function.cpp:39
get_entry_point_language
std::unique_ptr< languaget > get_entry_point_language(const symbol_table_baset &symbol_table, const optionst &options, message_handlert &message_handler)
Find the language corresponding to the __CPROVER_start function.
Definition
rebuild_goto_start_function.cpp:24
rebuild_goto_start_function.h
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition
invariant.h:423
symbol_table_base.h
Author: Diffblue Ltd.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
goto-programs
rebuild_goto_start_function.cpp
Generated by
1.17.0