cprover
remove_returns.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Remove function returns
4
5
Author: Daniel Kroening
6
7
Date: September 2009
8
9
\*******************************************************************/
10
13
14
#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
15
#define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
16
17
#include <functional>
18
19
#include <
util/std_types.h
>
20
21
#define RETURN_VALUE_SUFFIX "#return_value"
22
23
class
goto_functionst
;
24
class
goto_model_functiont
;
25
class
goto_modelt
;
26
class
symbol_table_baset
;
27
28
// Turns 'return x' into an assignment to fkt#return_value,
29
// unless the function returns void,
30
// and a 'goto the_end_of_the_function'.
31
32
void
remove_returns
(
symbol_table_baset
&,
goto_functionst
&);
33
34
typedef
std::function<bool(
const
irep_idt
&)>
function_is_stubt
;
35
36
void
remove_returns
(
goto_model_functiont
&,
function_is_stubt
);
37
38
void
remove_returns
(
goto_modelt
&);
39
40
// reverse the above operations
41
void
restore_returns
(
symbol_table_baset
&,
goto_functionst
&);
42
43
void
restore_returns
(
goto_modelt
&);
44
45
code_typet
original_return_type
(
46
const
symbol_table_baset
&symbol_table,
47
const
irep_idt
&function_id);
48
49
#endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:35
goto_modelt
Definition:
goto_model.h:24
function_is_stubt
std::function< bool(const irep_idt &)> function_is_stubt
Definition:
remove_returns.h:34
original_return_type
code_typet original_return_type(const symbol_table_baset &symbol_table, const irep_idt &function_id)
Get code type of a function that has had remove_returns run upon it.
Definition:
remove_returns.cpp:300
symbol_table_baset
The symbol table base class interface.
Definition:
symbol_table_base.h:21
std_types.h
code_typet
Base type of functions.
Definition:
std_types.h:751
remove_returns
void remove_returns(symbol_table_baset &, goto_functionst &)
removes returns
Definition:
remove_returns.cpp:261
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:22
restore_returns
void restore_returns(symbol_table_baset &, goto_functionst &)
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition:
goto_model.h:153
goto-programs
remove_returns.h
Generated by
1.8.16