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 <
goto-programs/goto_model.h
>
18
19
#define RETURN_VALUE_SUFFIX "#return_value"
20
21
// Turns 'return x' into an assignment to fkt#return_value,
22
// unless the function returns void,
23
// and a 'goto the_end_of_the_function'.
24
25
void
remove_returns
(
symbol_tablet
&,
goto_functionst
&);
26
27
void
remove_returns
(
goto_modelt
&);
28
29
// reverse the above operations
30
void
restore_returns
(
symbol_tablet
&,
goto_functionst
&);
31
32
code_typet
original_return_type
(
33
const
symbol_tablet
&symbol_table,
34
const
irep_idt
&function_id);
35
36
#endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H
code_typet
Base type of functions.
Definition:
std_types.h:734
restore_returns
void restore_returns(symbol_tablet &, goto_functionst &)
restores return statements
Definition:
remove_returns.cpp:392
goto_modelt
Definition:
goto_model.h:22
original_return_type
code_typet original_return_type(const symbol_tablet &symbol_table, const irep_idt &function_id)
Definition:
remove_returns.cpp:217
goto_model.h
Symbol Table + CFG.
remove_returns
void remove_returns(symbol_tablet &, goto_functionst &)
removes returns
Definition:
remove_returns.cpp:202
symbol_tablet
The symbol table.
Definition:
symbol_table.h:52
goto_functionst
Definition:
goto_functions.h:20
dstringt
Definition:
dstring.h:21
goto-programs
remove_returns.h
Generated by
1.8.14