cprover
|
#include <goto_function.h>
Public Types | |
typedef std::vector< irep_idt > | parameter_identifierst |
Public Member Functions | |
bool | body_available () const |
bool | is_inlined () const |
bool | is_hidden () const |
void | make_hidden () |
goto_functiont () | |
void | clear () |
void | update_instructions_function (const irep_idt &function_id) |
update the function member in each instruction More... | |
void | swap (goto_functiont &other) |
void | copy_from (const goto_functiont &other) |
goto_functiont (const goto_functiont &)=delete | |
goto_functiont & | operator= (const goto_functiont &)=delete |
goto_functiont (goto_functiont &&other) | |
goto_functiont & | operator= (goto_functiont &&other) |
Public Attributes | |
goto_programt | body |
code_typet | type |
parameter_identifierst | parameter_identifiers |
Definition at line 20 of file goto_function.h.
typedef std::vector<irep_idt> goto_functiont::parameter_identifierst |
Definition at line 26 of file goto_function.h.
|
inline |
Definition at line 49 of file goto_function.h.
|
delete |
|
inline |
Definition at line 85 of file goto_function.h.
|
inline |
Definition at line 29 of file goto_function.h.
References body, and goto_programt::instructions.
Referenced by goto_inlinet::goto_inline_logt::cleanup(), goto_inlinet::expand_function_call(), goto_inline(), goto_inlinet::goto_inline_nontransitive(), goto_inlinet::goto_inline_transitive(), goto_partial_inline(), goto_inlinet::insert_function_body(), and goto_inlinet::output_inline_map().
|
inline |
Definition at line 53 of file goto_function.h.
References body, irept::clear(), goto_programt::clear(), parameter_identifiers, and type.
|
inline |
Definition at line 75 of file goto_function.h.
References body, goto_programt::copy_from(), parameter_identifiers, and type.
Referenced by goto_inlinet::goto_inline_transitive().
|
inline |
Definition at line 39 of file goto_function.h.
References irept::get_bool(), and type.
Referenced by goto_inlinet::insert_function_body().
|
inline |
Definition at line 34 of file goto_function.h.
References irept::get_bool(), and type.
Referenced by goto_partial_inline().
|
inline |
Definition at line 44 of file goto_function.h.
References irept::set(), and type.
|
delete |
|
inline |
Definition at line 92 of file goto_function.h.
References body, parameter_identifiers, and type.
|
inline |
Definition at line 68 of file goto_function.h.
References body, parameter_identifiers, irept::swap(), goto_programt::swap(), and type.
|
inline |
update the function member in each instruction
function_id | the function_id used for assigning empty function members |
Definition at line 63 of file goto_function.h.
References body, and goto_programt::update_instructions_function().
goto_programt goto_functiont::body |
Definition at line 23 of file goto_function.h.
Referenced by body_available(), localst::build(), dirtyt::build(), goto_inlinet::goto_inline_logt::cleanup(), clear(), copy_from(), goto_inlinet::expand_function_call(), get_local_identifiers(), goto_checkt::goto_check(), goto_inline(), goto_inlinet::goto_inline_nontransitive(), goto_inlinet::goto_inline_transitive(), goto_partial_inline(), havoc_loopst::havoc_loop(), goto_inlinet::insert_function_body(), instrumentert::is_cfg_spurious(), operator=(), local_bitvector_analysist::output(), local_may_aliast::output(), goto_inlinet::output_inline_map(), k_inductiont::process_loop(), swap(), and update_instructions_function().
parameter_identifierst goto_functiont::parameter_identifiers |
Definition at line 27 of file goto_function.h.
Referenced by clear(), copy_from(), operator=(), and swap().
code_typet goto_functiont::type |
Definition at line 24 of file goto_function.h.
Referenced by localst::build(), local_may_aliast::build(), clear(), copy_from(), get_local_identifiers(), goto_inlinet::insert_function_body(), is_hidden(), is_inlined(), make_hidden(), operator=(), and swap().