cover.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Coverage Instrumentation
 
Author: Daniel Kroening
 
Date: May 2016
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_INSTRUMENT_COVER_H
#define CPROVER_GOTO_INSTRUMENT_COVER_H
 
#include "cover_filter.h"
#include "cover_instrument.h"
 
class cmdlinet;
class goto_modelt;
class goto_model_functiont;
class message_handlert;
class optionst;
class symbol_tablet;
 
#define OPT_COVER                                                              \
  "(cover):"                                                                   \
  "(cover-failed-assertions)"                                                  \
  "(show-test-suite)"
 
#define HELP_COVER                                                             \
  " {y--cover} {uCC} \t "                                                      \
  "create test-suite with coverage criterion {uCC}, where {uCC} is one of "    \
  "{yassertion}[{ys}], {yassume}[{ys}], {ybranch}[{yes}], "                    \
  "{ycondition}[{ys}], {ycover}, {ydecision}[{ys}], {ylocation}[{ys}], "       \
  "or {ymcdc}\n"                                                               \
  " {y--cover-failed-assertions} \t "                                          \
  "do not stop coverage checking at failed assertions (this is the default "   \
  "for {y--cover} {yassertions})\n"                                            \
  " {y--show-test-suite} \t "                                                  \
  "print test suite for coverage criterion (requires {y--cover})\n"
 
enum class coverage_criteriont
{
  ASSUME,
  LOCATION,
  BRANCH,
  DECISION,
  CONDITION,
  PATH,
  MCDC,
  ASSERTION,
  COVER // __CPROVER_cover(x) annotations
};
 
struct cover_configt
{
  bool keep_assertions;
  bool cover_failed_assertions;
  bool traces_must_terminate;
  irep_idt mode;
  function_filterst function_filters;
  // cover instruments point to goal_filters, so they must be stored on the heap
  std::unique_ptr<goal_filterst> goal_filters =
    std::make_unique<goal_filterst>();
  cover_instrumenterst cover_instrumenters;
  cover_instrumenter_baset::assertion_factoryt make_assertion =
    goto_programt::make_assertion;
};
 
void instrument_cover_goals(
  const symbol_tablet &,
  const cover_configt &,
  goto_functionst &,
  coverage_criteriont,
  message_handlert &message_handler);
 
void instrument_cover_goals(
  const symbol_tablet &,
  const cover_configt &,
  goto_programt &,
  coverage_criteriont,
  message_handlert &message_handler);
 
cover_configt
get_cover_config(const optionst &, const symbol_tablet &, message_handlert &);
 
cover_configt get_cover_config(
  const optionst &,
  const irep_idt &main_function_id,
  const symbol_tablet &,
  message_handlert &);
 
void instrument_cover_goals(
  const cover_configt &,
  goto_model_functiont &,
  message_handlert &);
 
void parse_cover_options(const cmdlinet &, optionst &);
 
bool instrument_cover_goals(
  const cover_configt &,
  const symbol_tablet &,
  goto_functionst &,
  message_handlert &);
 
bool instrument_cover_goals(
  const cover_configt &,
  goto_modelt &,
  message_handlert &);
 
#endif // CPROVER_GOTO_INSTRUMENT_COVER_H