CBMC
Loading...
Searching...
No Matches
Classes | Macros | Enumerations | Functions
cover.h File Reference

Coverage Instrumentation. More...

#include "cover_filter.h"
#include "cover_instrument.h"
+ Include dependency graph for cover.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct   cover_configt
 

Macros

#define  OPT_COVER
 
#define  HELP_COVER
 

Enumerations

enum class   coverage_criteriont {
  ASSUME , LOCATION , BRANCH , DECISION ,
  CONDITION , PATH , MCDC , ASSERTION ,
  COVER
}
 

Functions

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 &)
  Build data structures controlling coverage from command-line options.
 
cover_configt  get_cover_config (const optionst &, const irep_idt &main_function_id, const symbol_tablet &, message_handlert &)
  Build data structures controlling coverage from command-line options.
 
void  instrument_cover_goals (const cover_configt &, goto_model_functiont &, message_handlert &)
  Instruments a single goto program based on the given configuration.
 
void  parse_cover_options (const cmdlinet &, optionst &)
  Parses coverage-related command line options.
 
bool  instrument_cover_goals (const cover_configt &, const symbol_tablet &, goto_functionst &, message_handlert &)
  Instruments goto functions based on given command line options.
 
bool  instrument_cover_goals (const cover_configt &, goto_modelt &, message_handlert &)
  Instruments a goto model based on given command line options.
 

Detailed Description

Coverage Instrumentation.

Definition in file cover.h.

Macro Definition Documentation

◆  HELP_COVER

#define HELP_COVER
Value:
" {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"

Definition at line 32 of file cover.h.

◆  OPT_COVER

#define OPT_COVER
Value:
"(cover):" \
"(cover-failed-assertions)" \
"(show-test-suite)"

Definition at line 27 of file cover.h.

Enumeration Type Documentation

◆  coverage_criteriont

enum class coverage_criteriont
strong
Enumerator
ASSUME 
LOCATION 
BRANCH 
DECISION 
CONDITION 
PATH 
MCDC 
ASSERTION 
COVER 

Definition at line 44 of file cover.h.

Function Documentation

◆  get_cover_config() [1/2]

cover_configt get_cover_config ( const optionst &  options,
const irep_idt &  main_function_id,
const symbol_tablet &  symbol_table,
message_handlert &  message_handler 
)

Build data structures controlling coverage from command-line options.

Include options that depend on the main function specified by the user.

Parameters
options command-line options
main_function_id symbol of the user-specified main program function
symbol_table global symbol table
message_handler used to log incorrect option specifications
Returns
a cover_configt on success, or null otherwise.

Definition at line 247 of file cover.cpp.

◆  get_cover_config() [2/2]

cover_configt get_cover_config ( const optionst &  options,
const symbol_tablet &  symbol_table,
message_handlert &  message_handler 
)

Build data structures controlling coverage from command-line options.

Do not include the options that depend on the main function specified by the user.

Parameters
options command-line options
symbol_table global symbol table
message_handler used to log incorrect option specifications
Returns
a cover_configt on success, or null otherwise.

Definition at line 181 of file cover.cpp.

◆  instrument_cover_goals() [1/5]

bool instrument_cover_goals ( const cover_configt &  cover_config,
const symbol_tablet &  symbol_table,
goto_functionst &  goto_functions,
message_handlert &  message_handler 
)

Instruments goto functions based on given command line options.

Parameters
cover_config configuration, produced using get_cover_config
symbol_table the symbol table
goto_functions the goto functions
message_handler a message handler

Definition at line 375 of file cover.cpp.

◆  instrument_cover_goals() [2/5]

void instrument_cover_goals ( const cover_configt &  cover_config,
goto_model_functiont &  function,
message_handlert &  message_handler 
)

Instruments a single goto program based on the given configuration.

Parameters
cover_config configuration, produced using get_cover_config
function goto program to instrument
message_handler log output

Definition at line 354 of file cover.cpp.

◆  instrument_cover_goals() [3/5]

bool instrument_cover_goals ( const cover_configt &  cover_config,
goto_modelt &  goto_model,
message_handlert &  message_handler 
)

Instruments a goto model based on given command line options.

Parameters
cover_config configuration, produced using get_cover_config
goto_model the goto model
message_handler a message handler

Definition at line 412 of file cover.cpp.

◆  instrument_cover_goals() [4/5]

void instrument_cover_goals ( const symbol_tablet &  ,
const cover_configt &  ,
goto_functionst &  ,
coverage_criteriont  ,
message_handlert &  message_handler 
)

◆  instrument_cover_goals() [5/5]

void instrument_cover_goals ( const symbol_tablet &  ,
const cover_configt &  ,
goto_programt &  ,
coverage_criteriont  ,
message_handlert &  message_handler 
)

◆  parse_cover_options()

void parse_cover_options ( const cmdlinet &  cmdline,
optionst &  options 
)

Parses coverage-related command line options.

Parameters
cmdline the command line
options the options

Definition at line 143 of file cover.cpp.

AltStyle によって変換されたページ (->オリジナル) /