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>
42 typedef std::pair<goto_programt::targett, bool>
callt;
58 const bool force_full=
false);
63 const bool force_full=
false);
106 const unsigned begin_location_number,
107 const unsigned end_location_number,
108 const unsigned call_location_number,
137 const bool force_full);
142 const bool force_full);
162 const bool transitive,
163 const bool force_full,
204 #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 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)
void parameter_destruction(const goto_programt::targett target, const goto_functiont::parameter_identifierst ¶meter_identifiers, goto_programt &dest)
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
void parameter_assignments(const goto_programt::targett target, const irep_idt &function_name, const goto_functiont::parameter_identifierst ¶meter_identifiers, const exprt::operandst &arguments, goto_programt &dest)
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
Goto Programs with Functions.
goto_inline_logt inline_log
A generic container class for the GOTO intermediate representation of one function.
std::vector< irep_idt > parameter_identifierst
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