cprover
cover.cpp File Reference

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"
Include dependency graph for cover.cpp:

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_configtget_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_programtgoto_program
 
goto_programt coverage_criteriont criterion
 
goto_programt coverage_criteriont message_handlertmessage_handler
 
cover_instrumenterst instrumenters
 

Detailed Description

Coverage Instrumentation.

Definition in file cover.cpp.

Function Documentation

◆ add()

goal_filters add ( util_make_unique< internal_goals_filtert message_handler)

◆ add_from_criterion()

instrumenters add_from_criterion ( criterion  ,
symbol_table  ,
goal_filters   
)

◆ DEPRECATED()

Instruments goto program for a given coverage criterion.

Parameters
symbol_tablethe symbol table
goto_programthe goto program
criterionthe coverage criterion
message_handlera message handler
Deprecated:
use instrument_cover_goals(goto_programt &goto_program, const cover_instrumenterst &instrumenters, message_handlert &message_handler, const irep_idt mode) instead

◆ get_cover_config()

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.

Parameters
optionscommand-line options
symbol_tableglobal symbol table
message_handlerused to log incorrect option specifications
Returns
a cover_configt on success, or null otherwise.

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().

◆ instrument_cover_goals() [1/6]

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.

Parameters
goto_programthe goto program
instrumentersthe instrumenters
modemode of the function to instrument (for instance ID_C or ID_java)
message_handlera 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() [2/6]

instrument_cover_goals ( goto_program  ,
instrumenters  ,
ID_unknown  ,
message_handler   
)

◆ instrument_cover_goals() [3/6]

static void instrument_cover_goals ( const cover_configt config,
const irep_idt function_id,
goto_functionst::goto_functiont function,
message_handlert message_handler 
)
static

Instruments a single goto program based on the given configuration.

Parameters
configconfiguration, produced using get_cover_config
function_idfunction name
functionfunction function to instrument
message_handlerlog 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().

◆ instrument_cover_goals() [4/6]

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.

Parameters
configconfiguration, produced using get_cover_config
functiongoto program to instrument
message_handlerlog output

Definition at line 305 of file cover.cpp.

References config, goto_modelt::get_goto_function(), instrument_cover_goals(), and message_handler.

◆ instrument_cover_goals() [5/6]

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.

Parameters
optionsthe options
symbol_tablethe symbol table
goto_functionsthe goto functions
message_handlera 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.

◆ instrument_cover_goals() [6/6]

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.

Parameters
optionsthe options
goto_modelthe goto model
message_handlera 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.

◆ parse_cover_options()

void parse_cover_options ( const cmdlinet cmdline,
optionst options 
)

◆ parse_coverage_criterion()

coverage_criteriont parse_coverage_criterion ( const std::string &  criterion_string)

Parses a coverage criterion.

Parameters
criterion_stringa string
Returns
a coverage criterion or throws an exception

Definition at line 130 of file cover.cpp.

References ASSERTION, BRANCH, CONDITION, COVER, DECISION, LOCATION, MCDC, and PATH.

Referenced by get_cover_config().

Variable Documentation

◆ criterion

◆ goto_program

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().

◆ instrumenters

cover_instrumenterst instrumenters

Definition at line 70 of file cover.cpp.

Referenced by get_cover_config(), and instrument_cover_goals().

◆ message_handler

Initial value:
{
goal_filterst goal_filters
A collection of goal filters to be applied in conjunction.
Definition: cover_filter.h:111

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().