Coverage Instrumentation. More...

#include "cover.h"
#include <util/message.h>
#include <util/cmdline.h>
#include <util/options.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include "cover_basic_blocks.h"

Include dependency graph for cover.cpp:

Go to the source code of this file.

Functions
static void	instrument_cover_goals (const irep_idt &function_id, goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler, const cover_instrumenter_baset::assertion_factoryt &make_assertion)
	Applies instrumenters to given goto program. More...

coverage_criteriont	parse_coverage_criterion (const std::string &criterion_string)
	Parses a coverage criterion. More...

void	parse_cover_options (const cmdlinet &cmdline, optionst &options)
	Parses coverage-related command line options. More...

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. More...

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. More...

static void	instrument_cover_goals (const cover_configt &cover_config, const symbolt &function_symbol, goto_functionst::goto_functiont &function, message_handlert &message_handler)
	Instruments a single goto program based on the given configuration. More...

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. More...

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. More...

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. More...

Detailed Description

Coverage Instrumentation.

Definition in file cover.cpp.

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]

static void instrument_cover_goals	(	const cover_configt &	cover_config,
		const symbolt &	function_symbol,
		goto_functionst::goto_functiont &	function,
		message_handlert &	message_handler
	)

static

Instruments a single goto program based on the given configuration.

Parameters

cover_config	configuration, produced using get_cover_config
function_symbol	symbol of the function to be instrumented
function	function to instrument
message_handler	log output

Definition at line 286 of file cover.cpp.

◆ instrument_cover_goals() [3/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() [4/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() [5/5]

static void instrument_cover_goals	(	const irep_idt &	function_id,
		goto_programt &	goto_program,
		const cover_instrumenterst &	instrumenters,
		const irep_idt &	mode,
		message_handlert &	message_handler,
		const cover_instrumenter_baset::assertion_factoryt &	make_assertion
	)

static

Applies instrumenters to given goto program.

Parameters

function_id	name of `goto_program`
goto_program	the goto program
instrumenters	the instrumenters
mode	mode of the function to instrument (for instance ID_C or ID_java)
message_handler	a message handler
make_assertion	A function which takes an expression, with a source location and makes an assertion based on that expression. The expression asserted is expected to include the expression passed in, but may include other additional conditions.

Definition at line 36 of file cover.cpp.

◆ 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.

◆ parse_coverage_criterion()

coverage_criteriont parse_coverage_criterion ( const std::string & criterion_string )

Parses a coverage criterion.

Parameters

criterion_string a string

Returns: a coverage criterion or throws an exception

Definition at line 108 of file cover.cpp.

Functions

Detailed Description

Function Documentation

◆ get_cover_config() [1/2]

◆ get_cover_config() [2/2]

◆ instrument_cover_goals() [1/5]

◆ instrument_cover_goals() [2/5]

◆ instrument_cover_goals() [3/5]

◆ instrument_cover_goals() [4/5]

◆ instrument_cover_goals() [5/5]

◆ parse_cover_options()

◆ parse_coverage_criterion()