cprover
|
#include <goto_inline_class.h>
Classes | |
class | goto_inline_log_infot |
Public Types | |
typedef std::map< goto_programt::const_targett, goto_inline_log_infot > | log_mapt |
Public Member Functions | |
void | cleanup (const goto_programt &goto_program) |
void | cleanup (const goto_functionst::function_mapt &function_map) |
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) |
void | copy_from (const goto_programt &from, const goto_programt &to) |
jsont | output_inline_log_json () const |
Public Attributes | |
log_mapt | log_map |
Definition at line 86 of file goto_inline_class.h.
typedef std::map< goto_programt::const_targett, goto_inline_log_infot> goto_inlinet::goto_inline_logt::log_mapt |
Definition at line 120 of file goto_inline_class.h.
void goto_inlinet::goto_inline_logt::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 | ||
) |
Definition at line 819 of file goto_inline_class.cpp.
References goto_inlinet::goto_inline_logt::goto_inline_log_infot::begin_location_number, goto_inlinet::goto_inline_logt::goto_inline_log_infot::call_location_number, goto_programt::empty(), goto_inlinet::goto_inline_logt::goto_inline_log_infot::end, goto_inlinet::goto_inline_logt::goto_inline_log_infot::end_location_number, goto_inlinet::goto_inline_logt::goto_inline_log_infot::function, goto_program, goto_programt::instructions, and PRECONDITION.
Referenced by goto_inlinet::insert_function_body().
void goto_inlinet::goto_inline_logt::cleanup | ( | const goto_programt & | goto_program | ) |
Definition at line 798 of file goto_inline_class.cpp.
References forall_goto_program_instructions, goto_program, and log_map.
Referenced by goto_inlinet::expand_function_call(), and goto_inlinet::output_inline_log_json().
void goto_inlinet::goto_inline_logt::cleanup | ( | const goto_functionst::function_mapt & | function_map | ) |
Definition at line 805 of file goto_inline_class.cpp.
References goto_functiont::body, and goto_functiont::body_available().
void goto_inlinet::goto_inline_logt::copy_from | ( | const goto_programt & | from, |
const goto_programt & | to | ||
) |
Definition at line 846 of file goto_inline_class.cpp.
References goto_inlinet::goto_inline_logt::goto_inline_log_infot::end, goto_programt::instructions, and PRECONDITION.
Referenced by goto_inlinet::goto_inline_transitive(), and goto_inlinet::insert_function_body().
jsont goto_inlinet::goto_inline_logt::output_inline_log_json | ( | ) | const |
Definition at line 886 of file goto_inline_class.cpp.
References goto_inlinet::goto_inline_logt::goto_inline_log_infot::begin_location_number, dstringt::c_str(), goto_inlinet::goto_inline_logt::goto_inline_log_infot::call_location_number, goto_inlinet::goto_inline_logt::goto_inline_log_infot::end, goto_inlinet::goto_inline_logt::goto_inline_log_infot::end_location_number, goto_inlinet::goto_inline_logt::goto_inline_log_infot::function, jsont::make_array(), jsont::make_object(), json_arrayt::push_back(), and to_string().
Referenced by goto_inlinet::output_inline_log_json().
log_mapt goto_inlinet::goto_inline_logt::log_map |
Definition at line 122 of file goto_inline_class.h.
Referenced by cleanup().