10 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H 11 #define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H 13 #include <unordered_set> 43 typedef std::pair<goto_programt::targett, bool>
callt;
59 const bool force_full=
false);
64 const bool force_full=
false);
107 const unsigned begin_location_number,
108 const unsigned end_location_number,
109 const unsigned call_location_number,
138 const bool force_full);
143 const bool force_full);
163 const bool transitive,
164 const bool force_full,
206 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H std::pair< goto_programt::targett, bool > callt
std::list< callt > call_listt
void add_segment(const goto_programt &goto_program, const unsigned begin_location_number, const unsigned end_location_number, const unsigned call_location_number, const irep_idt function)
goto_inline_logt inline_log
bool is_ignored(const irep_idt id) const
Goto Programs with Functions.
void cleanup(const goto_programt &goto_program)
std::unordered_set< irep_idt > no_body_sett
void replace_return(goto_programt &body, const exprt &lhs)
void parameter_destruction(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest)
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
std::map< irep_idt, call_listt > inline_mapt
jsont output_inline_log_json() const
instructionst::iterator targett
recursion_sett recursion_set
std::unordered_set< irep_idt > recursion_sett
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
::goto_functiont goto_functiont
std::map< goto_programt::const_targett, goto_inline_log_infot > log_mapt
A collection of goto functions.
bool check_inline_map(const inline_mapt &inline_map) const
std::map< irep_idt, goto_functiont > function_mapt
unsigned call_location_number
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void insert_function_body(const goto_functiont &f, goto_programt &dest, goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)
goto_programt::const_targett end
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
goto_inlinet(goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true)
std::vector< exprt > operandst
A goto function, consisting of function type (see type), function body (see body), and parameter identifiers (see parameter_identifiers).
const bool adjust_function
A generic container class for the GOTO intermediate representation of one function.
goto_functionst & goto_functions
finished_sett finished_set
void output_cache(std::ostream &out) const
goto_functionst::function_mapt cachet
unsigned end_location_number
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, const exprt::operandst &arguments, goto_programt &dest)
Base class for all expressions.
void copy_from(const goto_programt &from, const goto_programt &to)
Expression to hold a symbol (variable)
unsigned begin_location_number
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
goto_functionst::goto_functiont goto_functiont
std::unordered_set< irep_idt > finished_sett
message_handlert * message_handler
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
jsont output_inline_log_json()