cover.h File Reference

#include "cover_filter.h"
#include "cover_instrument.h"
#include "util/make_unique.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	coverage_criteriont {   coverage_criteriont::ASSUME, coverage_criteriont::LOCATION, coverage_criteriont::BRANCH, coverage_criteriont::DECISION,   coverage_criteriont::CONDITION, coverage_criteriont::PATH, coverage_criteriont::MCDC, coverage_criteriont::ASSERTION,   coverage_criteriont::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. More...
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. More...
void	instrument_cover_goals (const cover_configt &, goto_model_functiont &, message_handlert &)
	Instruments a single goto program based on the given configuration. More...
void	parse_cover_options (const cmdlinet &, optionst &)
	Parses coverage-related command line options. More...
bool	instrument_cover_goals (const cover_configt &, const symbol_tablet &, goto_functionst &, message_handlert &)
	Instruments goto functions based on given command line options. More...
bool	instrument_cover_goals (const cover_configt &, goto_modelt &, message_handlert &)
	Instruments a goto model based on given command line options. More...

Detailed Description

Coverage Instrumentation

Definition in file cover.h.

Macro Definition Documentation

HELP_COVER

#define HELP_COVER

Value:

  " --cover CC                   create test-suite with coverage criterion "   \
  "CC,\n"                                                                      \
  "                              where CC is one of assertion[s], "            \
  "assume[s],\n"                                                               \
  "                              branch[es], condition[s], cover, "            \
  "decision[s],\n"                                                             \
  "                              location[s], or mcdc\n"                       \
  " --cover-failed-assertions    do not stop coverage checking at failed "     \
  "assertions\n"                                                               \
  "                              (this is the default for --cover "            \
  "assertions)\n"                                                              \
  " --show-test-suite            print test suite for coverage criterion "     \
  "(requires --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 coverage_criteriont

strong

Enumerator
ASSUME
LOCATION
BRANCH
DECISION
CONDITION
PATH
MCDC
ASSERTION
COVER

Definition at line 47 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 252 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 186 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 380 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 359 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 417 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 148 of file cover.cpp.