CBMC
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
goto_program_coverage_recordt Class Reference
+ Inheritance diagram for goto_program_coverage_recordt:
+ Collaboration diagram for goto_program_coverage_recordt:

Classes

struct  coverage_conditiont
 
struct  coverage_linet
 

Public Member Functions

 goto_program_coverage_recordt (const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, const symex_coveraget::coveraget &coverage)
 
const irep_idt & get_file () const
 
- Public Member Functions inherited from coverage_recordt
 coverage_recordt (const std::string &node_id)
 

Protected Types

typedef std::map< unsigned, coverage_linet > coverage_lines_mapt
 

Protected Member Functions

void compute_coverage_lines (const goto_programt &goto_program, const symex_coveraget::coveraget &coverage, coverage_lines_mapt &dest)
 

Protected Attributes

irep_idt file_name
 

Additional Inherited Members

- Public Attributes inherited from coverage_recordt
xmlt xml
 
std::size_t lines_covered
 
std::size_t lines_total
 
std::size_t branches_covered
 
std::size_t branches_total
 

Detailed Description

Definition at line 50 of file symex_coverage.cpp.

Member Typedef Documentation

◆ coverage_lines_mapt

typedef std::map<unsigned, coverage_linet> goto_program_coverage_recordt::coverage_lines_mapt
protected

Definition at line 87 of file symex_coverage.cpp.

Constructor & Destructor Documentation

◆ goto_program_coverage_recordt()

goto_program_coverage_recordt::goto_program_coverage_recordt ( const namespacet &  ns,
const irep_idt &  function_id,
const goto_programt &  goto_program,
const symex_coveraget::coveraget &  coverage 
)

Definition at line 128 of file symex_coverage.cpp.

Member Function Documentation

◆ compute_coverage_lines()

void goto_program_coverage_recordt::compute_coverage_lines ( const goto_programt &  goto_program,
const symex_coveraget::coveraget &  coverage,
coverage_lines_mapt &  dest 
)
protected

Definition at line 204 of file symex_coverage.cpp.

◆ get_file()

const irep_idt& goto_program_coverage_recordt::get_file ( ) const
inline

Definition at line 59 of file symex_coverage.cpp.

Member Data Documentation

◆ file_name

irep_idt goto_program_coverage_recordt::file_name
protected

Definition at line 65 of file symex_coverage.cpp.

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