Coverage Instrumentation.
More...
Go to the source code of this file.
|
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.
|
|
coverage_criteriont | parse_coverage_criterion (const std::string &criterion_string) |
| Parses a coverage criterion.
|
|
void | parse_cover_options (const cmdlinet &cmdline, optionst &options) |
| Parses coverage-related command line options.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
Coverage Instrumentation.
Definition in file cover.cpp.
◆ get_cover_config() [1/2]
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]
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]
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]
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]
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]
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]
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()
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()
Parses a coverage criterion.
- Parameters
-
- Returns
- a coverage criterion or throws an exception
Definition at line 108 of file cover.cpp.