cprover
|
Coverage Instrumentation. More...
Go to the source code of this file.
Functions | |
void | instrument_cover_goals (const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont) |
void | instrument_cover_goals (const symbol_tablet &symbol_table, goto_functionst &goto_functions, coverage_criteriont) |
bool | instrument_cover_goals (const cmdlinet &cmdline, const symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &msgh) |
Coverage Instrumentation.
Definition in file cover.h.
|
strong |
void instrument_cover_goals | ( | const symbol_tablet & | symbol_table, |
goto_programt & | goto_program, | ||
coverage_criteriont | |||
) |
Definition at line 832 of file cover.cpp.
References code_function_callt::arguments(), as_string(), ASSERT, ASSERTION, basic_blocks(), BRANCH, collect_conditions(), collect_decisions(), collect_mcdc_controlling_nested(), comment(), CONDITION, COVER, DECISION, dstringt::empty(), Forall_goto_program_instructions, from_expr(), code_function_callt::function(), source_locationt::get_file(), irept::id(), id2string(), goto_program_templatet< codeT, guardT >::insert_before(), goto_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, source_locationt::is_built_in(), is_condition(), LOCATION, MCDC, minimize_mcdc_controlling(), PATH, remove_repetition(), source_locationt::set_comment(), to_code_function_call(), and to_symbol_expr().
Referenced by instrument_cover_goals(), symex_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
void instrument_cover_goals | ( | const symbol_tablet & | symbol_table, |
goto_functionst & | goto_functions, | ||
coverage_criteriont | |||
) |
Definition at line 1137 of file cover.cpp.
References goto_functions_templatet< bodyT >::entry_point(), Forall_goto_functions, and instrument_cover_goals().
bool instrument_cover_goals | ( | const cmdlinet & | cmdline, |
const symbol_tablet & | symbol_table, | ||
goto_functionst & | goto_functions, | ||
message_handlert & | msgh | ||
) |
Definition at line 1153 of file cover.cpp.
References ASSERTION, ASSUME, BRANCH, CONDITION, COVER, DECISION, messaget::eom(), messaget::error(), Forall_goto_functions, Forall_goto_program_instructions, cmdlinet::get_values(), instrument_cover_goals(), LOCATION, MCDC, PATH, messaget::status(), and goto_functions_templatet< bodyT >::update().