cprover
|
Coverage Instrumentation. More...
#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 <util/deprecate.h>
#include <goto-programs/remove_skip.h>
#include "cover_basic_blocks.h"
Go to the source code of this file.
Functions | |
void | instrument_cover_goals (goto_programt &goto_program, const cover_instrumenterst &instrumenters, const irep_idt &mode, message_handlert &message_handler) |
Applies instrumenters to given goto program. More... | |
DEPRECATED ("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table | |
Instruments goto program for a given coverage criterion. More... | |
goal_filters | add (util_make_unique< internal_goals_filtert >(message_handler)) |
instrumenters | add_from_criterion (criterion, symbol_table, goal_filters) |
instrument_cover_goals (goto_program, instrumenters, ID_unknown, message_handler) | |
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... | |
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. More... | |
static void | instrument_cover_goals (const cover_configt &config, const irep_idt &function_id, 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 &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 optionst &options, 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 optionst &options, goto_modelt &goto_model, message_handlert &message_handler) |
Instruments a goto model based on given command line options. More... | |
Variables | |
goto_programt & | goto_program |
goto_programt coverage_criteriont | criterion |
goto_programt coverage_criteriont message_handlert & | message_handler |
cover_instrumenterst | instrumenters |
Coverage Instrumentation.
Definition in file cover.cpp.
goal_filters add | ( | util_make_unique< internal_goals_filtert > | message_handler | ) |
Referenced by linker_script_merget::ls_data2instructions(), and yyansi_cparse().
instrumenters add_from_criterion | ( | criterion | , |
symbol_table | , | ||
goal_filters | |||
) |
DEPRECATED | ( | "use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead" | ) | const & |
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 |
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 | ( | goto_programt & | goto_program, |
const cover_instrumenterst & | instrumenters, | ||
const irep_idt & | mode, | ||
message_handlert & | message_handler | ||
) |
Applies instrumenters to given 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 |
Definition at line 33 of file cover.cpp.
References goto_program, instrumenters, message_handler, and cover_blocks_baset::report_block_anomalies().
Referenced by instrument_cover_goals(), jbmc_parse_optionst::process_goto_function(), jbmc_parse_optionst::process_goto_functions(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
instrument_cover_goals | ( | goto_program | , |
instrumenters | , | ||
ID_unknown | , | ||
message_handler | |||
) |
|
static |
Instruments a single goto program based on the given configuration.
config | configuration, produced using get_cover_config |
function_id | function name |
function | function function to instrument |
message_handler | log output |
Definition at line 256 of file cover.cpp.
References ASSUME, config, cover_instrument_end_of_function(), goto_functionst::entry_point(), Forall_goto_program_instructions, instrument_cover_goals(), message_handler, and remove_skip().
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().
coverage_criteriont parse_coverage_criterion | ( | const std::string & | criterion_string | ) |
goto_programt coverage_criteriont criterion |
Definition at line 63 of file cover.cpp.
Referenced by cover_instrumenterst::add_from_criterion(), reachability_slicert::fixedpoint_from_assertions(), reachability_slicert::fixedpoint_to_assertions(), full_slicer(), reachability_slicert::get_sources(), reachability_slicert::operator()(), and full_slicert::operator()().
goto_programt& goto_program |
Definition at line 63 of file cover.cpp.
Referenced by uninitializedt::add_assertions(), remove_exceptionst::add_exception_dispatch_sequence(), w_guardst::add_initialization(), shared_bufferst::add_initialization(), invariant_propagationt::add_objects(), goto_inlinet::goto_inline_logt::add_segment(), add_to_json(), add_to_xml(), value_set_analysis_fit::add_vars(), value_set_analysis_fivrt::add_vars(), value_set_analysis_fivrnst::add_vars(), all_unreachable(), code_contractst::apply_contract(), shared_bufferst::assignment(), local_cfgt::build(), build_dead_map_from_ai(), call_grapht::call_grapht(), check_and_replace_target(), goto_unwindt::unwind_logt::cleanup(), goto_inlinet::goto_inline_logt::cleanup(), concurrency_instrumentationt::collect(), uncaught_exceptions_analysist::collect_uncaught_exceptions(), compute_address_taken_functions(), goto_program_coverage_recordt::compute_coverage_lines(), cfg_baset< cfg_nodet >::compute_edges(), cfg_baset< cfg_nodet >::compute_edges_catch(), cfg_baset< cfg_nodet >::compute_edges_function_call(), procedure_local_cfg_baset< nodet, goto_programt, goto_programt::targett >::compute_edges_function_call(), cfg_baset< cfg_nodet >::compute_edges_goto(), cfg_baset< cfg_nodet >::compute_edges_start_thread(), concurrent_cfg_baset< T, P, I >::compute_edges_start_thread(), value_set_analysis_templatet< VSDT >::convert(), convert(), goto_difft::convert_function_json(), convert_nondet(), convert_properties_json(), goto_unwindt::copy_segment(), cover_instrument_end_of_function(), shared_bufferst::delay_read(), goto_program_dereferencet::dereference_program(), shared_bufferst::det_flush(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), document_propertiest::doit(), goto_instrument_parse_optionst::doit(), ai_baset::entry_state(), find_property(), remove_exceptionst::find_universal_exception(), goto_convertt::finish_computed_gotos(), flow_insensitive_analysis_baset::fixedpoint(), static_analysis_baset::fixedpoint(), ai_baset::fixedpoint(), shared_bufferst::flush_read(), remove_exceptionst::function_or_callees_may_throw(), static_analysis_baset::generate_states(), function_modifiest::get_modifies_function(), goto_checkt::goto_check(), goto_function_inline(), goto_function_inline_and_log(), goto_inline(), goto_inlinet::goto_inline_nontransitive(), goto_inlinet::goto_inline_transitive(), goto_partial_inline(), goto_rw(), has_start_thread(), goto_convert_functionst::hide(), value_set_analysis_fit::initialize(), value_set_analysis_fivrt::initialize(), invariant_propagationt::initialize(), value_set_analysis_fivrnst::initialize(), static_analysis_baset::initialize(), dependence_grapht::initialize(), ai_baset::initialize(), property_checkert::initialize_property_map(), insert_nondet_init_code(), concurrency_instrumentationt::instrument(), cover_location_instrumentert::instrument(), cover_branch_instrumentert::instrument(), cover_condition_instrumentert::instrument(), cover_decision_instrumentert::instrument(), cover_mcdc_instrumentert::instrument(), instrument_cover_goals(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_exceptions(), remove_exceptionst::instrument_function_call(), instrument_preconditions(), remove_exceptionst::instrument_throw(), interrupt(), introduce_temporaries(), is_empty(), label_properties(), list_calls_and_arguments(), list_functions(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new(), make_assertions_false(), mmio(), mutex_init_instrumentation(), shared_bufferst::nondet_flush(), nondet_volatile(), remove_virtual_functionst::operator()(), remove_calls_no_bodyt::operator()(), cover_instrumenter_baset::operator()(), remove_function_pointerst::operator()(), goto_unwindt::operator()(), cover_instrumenterst::operator()(), remove_exceptionst::operator()(), flow_insensitive_analysis_baset::operator()(), static_analysis_baset::operator()(), ai_baset::operator()(), cfg_baset< cfg_nodet >::operator()(), value_set_analysis_fivrt::output(), value_set_analysis_fivrnst::output(), flow_insensitive_analysis_baset::output(), static_analysis_baset::output(), ai_baset::output(), change_impactt::output_change_impact(), output_dead_plain(), goto_difft::output_function(), goto_inlinet::output_inline_map(), change_impactt::output_instruction(), ai_baset::output_json(), ai_baset::output_xml(), goto_program_dereferencet::pointer_checks(), pointer_checks(), race_check(), remove_calls_no_bodyt::remove_call_no_body(), remove_exceptions(), remove_function_pointerst::remove_function_pointer(), remove_function_pointers(), remove_function_pointerst::remove_function_pointers(), remove_instanceof(), remove_java_new(), remove_pointers(), remove_preconditions(), remove_skip(), remove_unreachable(), remove_virtual_functionst::remove_virtual_function(), remove_virtual_function(), remove_virtual_functionst::remove_virtual_functions(), replace_java_nondet(), remove_returnst::replace_returns(), cover_basic_blockst::report_block_anomalies(), remove_returnst::restore_returns(), set_properties(), show_call_sequences(), show_locations(), show_loop_ids(), show_loop_ids_json(), show_properties(), show_value_sets(), invariant_propagationt::simplify(), skip_loops(), slice_global_inits(), stack_depth(), static_unreachable_instructions(), thread_exit_instrumentation(), remove_returnst::undo_function_calls(), unreachable_instructions(), goto_unwindt::unwind(), static_analysis_baset::update(), value_sets_to_xml(), flow_insensitive_analysis_baset::visit(), static_analysis_baset::visit(), ai_baset::visit(), shared_bufferst::cfg_visitort::weak_memory(), shared_bufferst::write(), and dott::write_dot_subgraph().
cover_instrumenterst instrumenters |
Definition at line 70 of file cover.cpp.
Referenced by get_cover_config(), and instrument_cover_goals().
goto_programt coverage_criteriont message_handlert& message_handler |
Definition at line 66 of file cover.cpp.
Referenced by accelerate_functions(), add_library(), ansi_c_entry_point(), ansi_c_typecheck(), c_preprocess(), c_preprocess_arm(), c_preprocess_codewarrior(), c_preprocess_gcc_clang(), c_preprocess_none(), c_preprocess_visual_studio(), mmcc_parse_optionst::convert(), convert(), convert_nondet(), cpp_typecheck(), cprover_c_library_factory(), cprover_cpp_library_factory(), generate_ansi_c_start_function(), generate_class_stub(), generate_function_bodies(), generate_function_bodies_factory(), generate_java_start_function(), get_cover_config(), get_main_symbol(), get_module(), get_module_by_name(), xml_interfacet::get_xml_options(), goto_convert(), goto_function_inline(), goto_function_inline_and_log(), goto_inline(), goto_partial_inline(), hybrid_binary(), initialize_goto_model(), insert_nondet_init_code(), instrument_cover_goals(), interpreter(), java_bytecode_convert_method(), java_bytecode_convert_method_lazy(), java_bytecode_instrument(), java_bytecode_instrument_symbol(), java_bytecode_parse(), java_bytecode_typecheck(), java_bytecode_typecheck_updated_symbols(), java_entry_point(), java_generate_simple_method_stub(), java_generate_simple_method_stubs(), java_static_lifetime_init(), jsil_convert(), jsil_entry_point(), jsil_typecheck(), link_goto_model(), link_to_library(), linking(), linker_script_merget::ls_data2instructions(), member_type_lazy(), model_argc_argv(), nondet_initializer(), parse_json(), parse_xml(), read_bin_goto_object(), read_goto_binary(), read_graphml(), read_object_and_link(), remove_function(), remove_functions(), remove_java_new(), remove_unused_functions(), cover_basic_blockst::report_block_anomalies(), show_class_hierarchy(), show_goto_functions(), show_properties(), show_properties_json(), skip_loops(), solver(), splice_call(), static_lifetime_init(), static_simplifier(), static_verifier(), string_abstraction(), string_instrumentation(), taint_analysis(), taint_parser(), test_c_preprocessor(), weak_memory(), write_goto_binary(), and zero_initializer().