Go to the documentation of this file.
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
Class that provides messages with a built-in verbosity 'level'.
unsigned begin_location_number
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void parameter_destruction(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest)
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)
jsont output_inline_log_json()
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)
unsigned call_location_number
void replace_return(goto_programt &body, const exprt &lhs)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
std::unordered_set< irep_idt > recursion_sett
Base class for all expressions.
void goto_inline(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
void cleanup(const goto_programt &goto_program)
Expression to hold a symbol (variable)
unsigned end_location_number
std::pair< goto_programt::targett, bool > callt
const bool adjust_function
void goto_inline_nontransitive(const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
recursion_sett recursion_set
goto_functionst::function_mapt cachet
std::map< irep_idt, goto_functiont > function_mapt
std::map< goto_programt::const_targett, goto_inline_log_infot > log_mapt
jsont output_inline_log_json() const
std::unordered_set< irep_idt > no_body_sett
goto_inlinet(goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true)
goto_programt::const_targett end
goto_functionst & goto_functions
A goto function, consisting of function type (see type), function body (see body),...
std::vector< exprt > operandst
std::unordered_set< irep_idt > finished_sett
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
std::map< irep_idt, call_listt > inline_mapt
::goto_functiont goto_functiont
A collection of goto functions.
message_handlert * message_handler
finished_sett finished_set
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
bool check_inline_map(const inline_mapt &inline_map) const
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)
goto_inline_logt inline_log
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
bool is_ignored(const irep_idt id) const
void copy_from(const goto_programt &from, const goto_programt &to)
void output_cache(std::ostream &out) const
instructionst::iterator targett
goto_functionst::goto_functiont goto_functiont