CBMC
|
Coverage Instrumentation. More...
Go to the source code of this file.
Classes | |
struct | cover_configt |
Macros | |
#define | OPT_COVER |
#define | HELP_COVER |
Enumerations | |
enum class | coverage_criteriont { ASSUME , LOCATION , BRANCH , DECISION , CONDITION , PATH , MCDC , ASSERTION , 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... | |
Coverage Instrumentation.
Definition in file cover.h.
#define HELP_COVER |
#define OPT_COVER |
|
strong |
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.
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 |
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.
options | command-line options |
symbol_table | global symbol table |
message_handler | used to log incorrect option specifications |
bool instrument_cover_goals | ( | const cover_configt & | cover_config, |
const symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions, | ||
message_handlert & | message_handler | ||
) |
void instrument_cover_goals | ( | const cover_configt & | cover_config, |
goto_model_functiont & | function, | ||
message_handlert & | message_handler | ||
) |
bool instrument_cover_goals | ( | const cover_configt & | cover_config, |
goto_modelt & | goto_model, | ||
message_handlert & | message_handler | ||
) |
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 | ||
) |