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);
112 const unsigned begin_location_number,
113 const unsigned end_location_number,
114 const unsigned call_location_number,
143 const bool force_full);
148 const bool force_full);
168 const bool transitive,
169 const bool force_full,
179 const exprt &constrain);
191 const exprt &constrain);
220 #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H std::map< irep_idt, goto_functiont > function_mapt
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
static bool is_bp_call(goto_programt::const_targett target)
Goto Programs with Functions.
void cleanup(const goto_programt &goto_program)
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments, exprt &constrain)
void parameter_destruction(const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest)
std::unordered_set< irep_idt, irep_id_hash > recursion_sett
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
instructionst::const_iterator const_targett
jsont output_inline_log_json() const
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, const exprt &constrain)
recursion_sett recursion_set
std::unordered_set< irep_idt, irep_id_hash > no_body_sett
void replace_return(goto_programt &body, const exprt &lhs, const exprt &constrain)
void expand_function_call(goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target)
std::map< goto_programt::const_targett, goto_inline_log_infot > log_mapt
bool check_inline_map(const inline_mapt &inline_map) const
unsigned call_location_number
goto_function_templatet< goto_programt > goto_functiont
goto_programt::const_targett end
const goto_functiont & goto_inline_transitive(const irep_idt identifier, const goto_functiont &goto_function, const bool force_full)
goto_inlinet(goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true)
std::vector< exprt > operandst
const bool adjust_function
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
goto_functionst & goto_functions
finished_sett finished_set
void output_cache(std::ostream &out) const
goto_functionst::function_mapt cachet
std::unordered_set< irep_idt, irep_id_hash > finished_sett
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
static bool is_call(goto_programt::const_targett target)
message_handlert * message_handler
void output_inline_map(std::ostream &out, const inline_mapt &inline_map)
void insert_function_nobody(goto_programt &dest, const exprt &lhs, goto_programt::targett target, const symbol_exprt &function, const exprt::operandst &arguments)
instructionst::iterator targett
jsont output_inline_log_json()