cprover
|
Coverage Instrumentation. More...
Go to the source code of this file.
Classes | |
struct | cover_configt |
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 |
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().
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 | ||
) |
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.
config | configuration, produced using get_cover_config |
function | goto program to instrument |
message_handler | log output |
Definition at line 305 of file cover.cpp.
References config, goto_modelt::get_goto_function(), instrument_cover_goals(), and message_handler.
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.
options | the options |
symbol_table | the symbol table |
goto_functions | the goto functions |
message_handler | a 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.
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.
options | the options |
goto_model | the goto model |
message_handler | a 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.
Parses coverage-related command line options.
cmdline | the command line |
options | the options |
Definition at line 163 of file cover.cpp.
References config, cmdlinet::get_value(), cmdlinet::get_values(), cmdlinet::isset(), configt::main, and optionst::set_option().
Referenced by jdiff_parse_optionst::get_command_line_options(), goto_diff_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_command_line_options(), and jbmc_parse_optionst::get_command_line_options().