cprover
cover.cpp File Reference
#include "cover.h"
#include <util/config.h>
#include <util/message.h>
#include <util/make_unique.h>
#include <util/cmdline.h>
#include <util/options.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

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)
 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
optionscommand-line options
main_function_idsymbol of the user-specified main program function
symbol_tableglobal symbol table
message_handlerused to log incorrect option specifications
Returns
a cover_configt on success, or null otherwise.

Definition at line 234 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
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 171 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_configconfiguration, produced using get_cover_config
symbol_tablethe symbol table
goto_functionsthe goto functions
message_handlera message handler

Definition at line 353 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_configconfiguration, produced using get_cover_config
function_symbolsymbol of the function to be instrumented
functionfunction to instrument
message_handlerlog output

Definition at line 273 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_configconfiguration, produced using get_cover_config
functiongoto program to instrument
message_handlerlog output

Definition at line 332 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_configconfiguration, produced using get_cover_config
goto_modelthe goto model
message_handlera message handler

Definition at line 390 of file cover.cpp.

◆ instrument_cover_goals() [5/5]

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 
)

Applies instrumenters to given goto program.

Parameters
function_idname of goto_program
goto_programthe goto program
instrumentersthe instrumenters
modemode of the function to instrument (for instance ID_C or ID_java)
message_handlera message handler

Definition at line 33 of file cover.cpp.

◆ parse_cover_options()

void parse_cover_options ( const cmdlinet cmdline,
optionst options 
)

Parses coverage-related command line options.

Parameters
cmdlinethe command line
optionsthe options

Definition at line 137 of file cover.cpp.

◆ parse_coverage_criterion()

coverage_criteriont parse_coverage_criterion ( const std::string &  criterion_string)

Parses a coverage criterion.

Parameters
criterion_stringa string
Returns
a coverage criterion or throws an exception

Definition at line 104 of file cover.cpp.