symex_coverage.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Record and print code coverage of symbolic execution
 
Author: Michael Tautschnig
 
Date: March 2016
 
\*******************************************************************/
 
 
#ifndef CPROVER_CBMC_SYMEX_COVERAGE_H
#define CPROVER_CBMC_SYMEX_COVERAGE_H
 
#include <iosfwd>
#include <map>
#include <string>
 
#include <goto-programs/goto_program.h>
 
class coverage_recordt;
class goto_functionst;
class namespacet;
class xmlt;
 
class symex_coveraget
{
public:
  explicit symex_coveraget(const namespacet &_ns) : ns(_ns)
  {
  }
 
  void
  covered(goto_programt::const_targett from, goto_programt::const_targett to)
  {
    std::pair<coverage_innert::iterator, bool> entry =
      coverage[from].insert({to, coverage_infot(from, to, 1)});
 
    if(!entry.second)
      ++(entry.first->second.num_executions);
  }
 
  bool generate_report(
    const goto_functionst &goto_functions,
    const std::string &path) const;
 
protected:
  const namespacet &ns;
 
  struct coverage_infot
  {
    coverage_infot(
      goto_programt::const_targett _from,
      goto_programt::const_targett _to,
      unsigned _num_executions)
      : location(_from), num_executions(_num_executions), succ(_to)
    {
    }
 
    goto_programt::const_targett location;
    unsigned num_executions;
    goto_programt::const_targett succ;
  };
 
  typedef std::map<
    goto_programt::const_targett,
    coverage_infot,
    goto_programt::target_less_than>
    coverage_innert;
  typedef std::map<
    goto_programt::const_targett,
    coverage_innert,
    goto_programt::target_less_than>
    coveraget;
  coveraget coverage;
 
  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;
 
  friend class goto_program_coverage_recordt;
};
 
#endif // CPROVER_CBMC_SYMEX_COVERAGE_H