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 91 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 125 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 974 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_program_templatet< codeT, guardT >::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, and goto_program_templatet< codeT, guardT >::instructions.
Referenced by goto_inlinet::insert_function_body().
void goto_inlinet::goto_inline_logt::cleanup | ( | const goto_programt & | goto_program | ) |
Definition at line 952 of file goto_inline_class.cpp.
References forall_goto_program_instructions, 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 959 of file goto_inline_class.cpp.
void goto_inlinet::goto_inline_logt::copy_from | ( | const goto_programt & | from, |
const goto_programt & | to | ||
) |
Definition at line 1001 of file goto_inline_class.cpp.
References goto_program_templatet< codeT, guardT >::instructions.
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 1041 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(), and json_arrayt::push_back().
Referenced by goto_inlinet::output_inline_log_json().
log_mapt goto_inlinet::goto_inline_logt::log_map |
Definition at line 127 of file goto_inline_class.h.
Referenced by cleanup().