CBMC
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | Friends | List of all members
symex_coveraget Class Reference

#include <symex_coverage.h>

+ Collaboration diagram for symex_coveraget:

Classes

struct  coverage_infot
 

Public Member Functions

 symex_coveraget (const namespacet &_ns)
 
void covered (goto_programt::const_targett from, goto_programt::const_targett to)
 
bool generate_report (const goto_functionst &goto_functions, const std::string &path) const
 

Protected Types

typedef std::map< goto_programt::const_targett, coverage_infot > coverage_innert
 
typedef std::map< goto_programt::const_targett, coverage_innert > coveraget
 

Protected Member Functions

bool output_report (const goto_functionst &goto_functions, std::ostream &os) const
 
void build_cobertura (const goto_functionst &goto_functions, xmlt &xml_coverage) const
 
void compute_overall_coverage (const goto_functionst &goto_functions, coverage_recordt &dest) const
 

Protected Attributes

const namespacet & ns
 
coveraget coverage
 

Friends

class goto_program_coverage_recordt
 

Detailed Description

Definition at line 28 of file symex_coverage.h.

Member Typedef Documentation

◆ coverage_innert

typedef std::map<goto_programt::const_targett, coverage_infot> symex_coveraget::coverage_innert
protected

Definition at line 68 of file symex_coverage.h.

◆ coveraget

typedef std::map<goto_programt::const_targett, coverage_innert> symex_coveraget::coveraget
protected

Definition at line 69 of file symex_coverage.h.

Constructor & Destructor Documentation

◆ symex_coveraget()

symex_coveraget::symex_coveraget ( const namespacet &  _ns)
inlineexplicit

Definition at line 31 of file symex_coverage.h.

Member Function Documentation

◆ build_cobertura()

void symex_coveraget::build_cobertura ( const goto_functionst &  goto_functions,
xmlt &  xml_coverage 
) const
protected

Definition at line 368 of file symex_coverage.cpp.

◆ compute_overall_coverage()

void symex_coveraget::compute_overall_coverage ( const goto_functionst &  goto_functions,
coverage_recordt &  dest 
) const
protected

Definition at line 291 of file symex_coverage.cpp.

◆ covered()

void symex_coveraget::covered ( goto_programt::const_targett  from,
goto_programt::const_targett  to 
)
inline

Definition at line 36 of file symex_coverage.h.

◆ generate_report()

bool symex_coveraget::generate_report ( const goto_functionst &  goto_functions,
const std::string &  path 
) const

Definition at line 427 of file symex_coverage.cpp.

◆ output_report()

bool symex_coveraget::output_report ( const goto_functionst &  goto_functions,
std::ostream &  os 
) const
protected

Definition at line 412 of file symex_coverage.cpp.

Friends And Related Function Documentation

◆ goto_program_coverage_recordt

friend class goto_program_coverage_recordt
friend

Definition at line 83 of file symex_coverage.h.

Member Data Documentation

◆ coverage

coveraget symex_coveraget::coverage
protected

Definition at line 70 of file symex_coverage.h.

◆ ns

const namespacet& symex_coveraget::ns
protected

Definition at line 50 of file symex_coverage.h.

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