cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
rebuild_goto_start_function.h
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
#ifndef CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
13
#define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
14
15
#include <memory>
16
17
#include <
util/irep.h
>
18
19
class
languaget
;
20
class
message_handlert
;
21
class
optionst
;
22
class
symbol_table_baset
;
23
26
void
remove_existing_entry_point
(
symbol_table_baset
&);
27
31
const
irep_idt
&
get_entry_point_mode
(
const
symbol_table_baset
&);
32
37
std::unique_ptr<languaget>
get_entry_point_language
(
38
const
symbol_table_baset
&symbol_table,
39
const
optionst
&options,
40
message_handlert
&message_handler);
41
42
#endif
// CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
languaget
Definition
language.h:37
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
irep.h
remove_existing_entry_point
void remove_existing_entry_point(symbol_table_baset &)
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 &)
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
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
goto-programs
rebuild_goto_start_function.h
Generated by
1.17.0