CBMC
Classes | Public Types | Public Member Functions | Public Attributes | List of all members
goto_inlinet::goto_inline_logt Class Reference

#include <goto_inline_class.h>

+ Collaboration diagram for goto_inlinet::goto_inline_logt:

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
 

Detailed Description

Definition at line 97 of file goto_inline_class.h.

Member Typedef Documentation

◆ log_mapt

typedef std::map< goto_programt::const_targett, goto_inline_log_infot> goto_inlinet::goto_inline_logt::log_mapt

Definition at line 131 of file goto_inline_class.h.

Member Function Documentation

◆ add_segment()

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 744 of file goto_inline_class.cpp.

◆ cleanup() [1/2]

void goto_inlinet::goto_inline_logt::cleanup ( const goto_functionst::function_mapt &  function_map)

Definition at line 730 of file goto_inline_class.cpp.

◆ cleanup() [2/2]

void goto_inlinet::goto_inline_logt::cleanup ( const goto_programt &  goto_program)

Definition at line 723 of file goto_inline_class.cpp.

◆ copy_from()

void goto_inlinet::goto_inline_logt::copy_from ( const goto_programt &  from,
const goto_programt &  to 
)

Definition at line 773 of file goto_inline_class.cpp.

◆ output_inline_log_json()

jsont goto_inlinet::goto_inline_logt::output_inline_log_json ( ) const

Definition at line 819 of file goto_inline_class.cpp.

Member Data Documentation

◆ log_map

log_mapt goto_inlinet::goto_inline_logt::log_map

Definition at line 133 of file goto_inline_class.h.

The documentation for this class was generated from the following files: