cprover
cover.h File Reference

Coverage Instrumentation. More...

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
 

Enumerations

enum  coverage_criteriont {
  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 &, goto_functionst &, coverage_criteriont, message_handlert &message_handler)
 
void instrument_cover_goals (const symbol_tablet &, goto_programt &, coverage_criteriont, message_handlert &message_handler)
 
std::unique_ptr< cover_configtget_cover_config (const optionst &, 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 optionst &, const symbol_tablet &, goto_functionst &, message_handlert &)
 Instruments goto functions based on given command line options. More...
 
bool instrument_cover_goals (const optionst &, goto_modelt &, message_handlert &)
 Instruments a goto model based on given command line options. More...
 

Detailed Description

Coverage Instrumentation.

Definition in file cover.h.

Enumeration Type Documentation

◆ coverage_criteriont

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

Definition at line 25 of file cover.h.

Function Documentation

◆ get_cover_config()

std::unique_ptr<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.

Parameters
optionscommand-line options
symbol_tableglobal symbol table
message_handlerused to log incorrect option specifications
Returns
a cover_configt on success, or null otherwise.

Definition at line 187 of file cover.cpp.

References goal_filterst::add(), cover_instrumenterst::add_from_criterion(), ASSERTION, config, messaget::eom(), messaget::error(), optionst::get_bool_option(), optionst::get_list_option(), optionst::get_option(), instrumenters, message_handler, parse_coverage_criterion(), and goto_modelt::symbol_table.

Referenced by jbmc_parse_optionst::doit(), and instrument_cover_goals().

◆ instrument_cover_goals() [1/5]

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

◆ instrument_cover_goals() [2/5]

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

◆ instrument_cover_goals() [3/5]

void instrument_cover_goals ( const cover_configt config,
goto_model_functiont function,
message_handlert message_handler 
)

Instruments a single goto program based on the given configuration.

Parameters
configconfiguration, produced using get_cover_config
functiongoto program to instrument
message_handlerlog output

Definition at line 305 of file cover.cpp.

References config, goto_modelt::get_goto_function(), instrument_cover_goals(), and message_handler.

◆ instrument_cover_goals() [4/5]

bool instrument_cover_goals ( const optionst options,
const symbol_tablet symbol_table,
goto_functionst goto_functions,
message_handlert message_handler 
)

Instruments goto functions based on given command line options.

Parameters
optionsthe options
symbol_tablethe symbol table
goto_functionsthe goto functions
message_handlera message handler

Definition at line 324 of file cover.cpp.

References goto_functionst::compute_location_numbers(), config, goto_functionst::entry_point(), messaget::eom(), messaget::error(), Forall_goto_functions, goto_functionst::function_map, get_cover_config(), goto_modelt::goto_functions, instrument_cover_goals(), symbol_table_baset::lookup(), message_handler, symbolt::mode, messaget::status(), and goto_modelt::symbol_table.

◆ instrument_cover_goals() [5/5]

bool instrument_cover_goals ( const optionst options,
goto_modelt goto_model,
message_handlert message_handler 
)

Instruments a goto model based on given command line options.

Parameters
optionsthe options
goto_modelthe goto model
message_handlera message handler

Definition at line 365 of file cover.cpp.

References goto_modelt::goto_functions, instrument_cover_goals(), message_handler, and goto_modelt::symbol_table.

◆ parse_cover_options()

void parse_cover_options ( const cmdlinet cmdline,
optionst options 
)