cprover
|
Go to the source code of this file.
Classes | |
struct | cover_configt |
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) |
Instruments goto program for a given coverage criterion. More... | |
std::unique_ptr< cover_configt > | get_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... | |
Coverage Instrumentation
Definition in file cover.h.
|
strong |
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.
options | command-line options |
symbol_table | global symbol table |
message_handler | used to log incorrect option specifications |
void instrument_cover_goals | ( | const cover_configt & | config, |
goto_model_functiont & | function, | ||
message_handlert & | message_handler | ||
) |
bool instrument_cover_goals | ( | const optionst & | options, |
const symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions, | ||
message_handlert & | message_handler | ||
) |
bool instrument_cover_goals | ( | const optionst & | options, |
goto_modelt & | goto_model, | ||
message_handlert & | message_handler | ||
) |
void instrument_cover_goals | ( | const symbol_tablet & | , |
goto_functionst & | , | ||
coverage_criteriont | , | ||
message_handlert & | message_handler | ||
) |
void instrument_cover_goals | ( | const symbol_tablet & | symbol_table, |
goto_programt & | goto_program, | ||
coverage_criteriont | criterion, | ||
message_handlert & | message_handler | ||
) |
Instruments goto program for a given coverage criterion.
symbol_table | the symbol table |
goto_program | the goto program |
criterion | the coverage criterion |
message_handler | a message handler |