cprover
|
Coverage Instrumentation. More...
#include "cover.h"
#include <algorithm>
#include <iterator>
#include <util/prefix.h>
#include <util/message.h>
Go to the source code of this file.
Classes | |
class | basic_blockst |
Functions | |
const char * | as_string (coverage_criteriont c) |
bool | is_condition (const exprt &src) |
void | collect_conditions_rec (const exprt &src, std::set< exprt > &dest) |
std::set< exprt > | collect_conditions (const exprt &src) |
std::set< exprt > | collect_conditions (const goto_programt::const_targett t) |
void | collect_operands (const exprt &src, std::vector< exprt > &dest) |
void | collect_mcdc_controlling_rec (const exprt &src, const std::vector< exprt > &conditions, std::set< exprt > &result) |
To recursively collect controlling exprs for for mcdc coverage. More... | |
std::set< exprt > | collect_mcdc_controlling (const std::set< exprt > &decisions) |
std::set< exprt > | replacement_conjunction (const std::set< exprt > &replacement_exprs, const std::vector< exprt > &operands, const std::size_t i) |
To replace the i-th expr of ''operands'' with each expr inside ''replacement_exprs''. More... | |
std::set< exprt > | collect_mcdc_controlling_nested (const std::set< exprt > &decisions) |
This nested method iteratively applies ''collect_mcdc_controlling'' to every non-atomic expr within a decision. More... | |
std::set< signed > | sign_of_expr (const exprt &e, const exprt &E) |
The sign of expr ''e'' within the super-expr ''E''. More... | |
void | remove_repetition (std::set< exprt > &exprs) |
After the ''collect_mcdc_controlling_nested'', there can be the recurrence of the same expr in the resulted set of exprs, and this method will remove the repetitive ones. More... | |
bool | eval_expr (const std::map< exprt, signed > &atomic_exprs, const exprt &src) |
To evaluate the value of expr ''src'', according to the atomic expr values. More... | |
std::map< exprt, signed > | values_of_atomic_exprs (const exprt &e, const std::set< exprt > &conditions) |
To obtain values of atomic exprs within the super expr. More... | |
bool | is_mcdc_pair (const exprt &e1, const exprt &e2, const exprt &c, const std::set< exprt > &conditions, const exprt &decision) |
To check if the two input controlling exprs are mcdc pairs regarding an atomic expr ''c''. More... | |
bool | has_mcdc_pair (const exprt &c, const std::set< exprt > &expr_set, const std::set< exprt > &conditions, const exprt &decision) |
To check if we can find the mcdc pair of the input ''expr_set'' regarding the atomic expr ''c''. More... | |
void | minimize_mcdc_controlling (std::set< exprt > &controlling, const exprt &decision) |
This method minimizes the controlling conditions for mcdc coverage. More... | |
void | collect_decisions_rec (const exprt &src, std::set< exprt > &dest) |
std::set< exprt > | collect_decisions (const exprt &src) |
std::set< exprt > | collect_decisions (const goto_programt::const_targett t) |
void | instrument_cover_goals (const symbol_tablet &symbol_table, goto_programt &goto_program, coverage_criteriont criterion) |
void | instrument_cover_goals (const symbol_tablet &symbol_table, goto_functionst &goto_functions, coverage_criteriont criterion) |
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.cpp.
const char* as_string | ( | coverage_criteriont | c | ) |
Definition at line 71 of file cover.cpp.
References ASSERTION, BRANCH, CONDITION, COVER, DECISION, LOCATION, MCDC, and PATH.
Referenced by java_bytecode_convert_methodt::convert_instructions(), goto_convertt::do_function_call_symbol(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_struct_init(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), id2string(), instrument_cover_goals(), name2string(), and locst::output().
Definition at line 114 of file cover.cpp.
References collect_conditions_rec().
Referenced by collect_conditions(), instrument_cover_goals(), minimize_mcdc_controlling(), and remove_repetition().
std::set<exprt> collect_conditions | ( | const goto_programt::const_targett | t | ) |
Definition at line 121 of file cover.cpp.
References ASSERT, ASSIGN, collect_conditions(), FUNCTION_CALL, and GOTO.
Definition at line 100 of file cover.cpp.
References irept::id(), is_condition(), exprt::is_constant(), and exprt::operands().
Referenced by collect_conditions().
Definition at line 805 of file cover.cpp.
References collect_decisions_rec().
Referenced by collect_decisions(), and instrument_cover_goals().
std::set<exprt> collect_decisions | ( | const goto_programt::const_targett | t | ) |
Definition at line 812 of file cover.cpp.
References ASSERT, ASSIGN, collect_decisions(), FUNCTION_CALL, and GOTO.
Definition at line 776 of file cover.cpp.
References irept::id(), exprt::is_constant(), exprt::op0(), exprt::operands(), and exprt::type().
Referenced by collect_decisions().
Definition at line 263 of file cover.cpp.
References collect_mcdc_controlling_rec().
Referenced by collect_mcdc_controlling_nested().
This nested method iteratively applies ''collect_mcdc_controlling'' to every non-atomic expr within a decision.
The final controlling conditions resulted from ''src'' will be stored in ''s1''; ''s2'' is usd to hold the temporary expansion.
To expand an operand if it is not atomic, and label the ''changed'' flag; the resulted expansion of such an operand is stored in ''res''.
Definition at line 298 of file cover.cpp.
References collect_mcdc_controlling(), collect_operands(), is_condition(), and replacement_conjunction().
Referenced by instrument_cover_goals().
void collect_mcdc_controlling_rec | ( | const exprt & | src, |
const std::vector< exprt > & | conditions, | ||
std::set< exprt > & | result | ||
) |
To recursively collect controlling exprs for for mcdc coverage.
It may happen that ''is_condition(src)'' is valid, but we ignore this case here as it can be handled by the routine decision/condition detection.
Definition at line 153 of file cover.cpp.
References collect_operands(), conjunction(), irept::id(), is_condition(), not_exprt::op(), and to_not_expr().
Referenced by collect_mcdc_controlling().
Definition at line 141 of file cover.cpp.
References irept::id(), and exprt::operands().
Referenced by collect_mcdc_controlling_nested(), collect_mcdc_controlling_rec(), eval_expr(), and sign_of_expr().
To evaluate the value of expr ''src'', according to the atomic expr values.
Definition at line 539 of file cover.cpp.
References collect_operands(), irept::id(), and exprt::make_not().
Referenced by is_mcdc_pair().
bool has_mcdc_pair | ( | const exprt & | c, |
const std::set< exprt > & | expr_set, | ||
const std::set< exprt > & | conditions, | ||
const exprt & | decision | ||
) |
To check if we can find the mcdc pair of the input ''expr_set'' regarding the atomic expr ''c''.
Definition at line 675 of file cover.cpp.
References is_mcdc_pair().
Referenced by minimize_mcdc_controlling().
void instrument_cover_goals | ( | const symbol_tablet & | symbol_table, |
goto_programt & | goto_program, | ||
coverage_criteriont | criterion | ||
) |
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 | criterion | ||
) |
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().
bool is_condition | ( | const exprt & | src | ) |
Definition at line 87 of file cover.cpp.
References irept::id(), and exprt::type().
Referenced by collect_conditions_rec(), collect_mcdc_controlling_nested(), collect_mcdc_controlling_rec(), instrument_cover_goals(), and sign_of_expr().
bool is_mcdc_pair | ( | const exprt & | e1, |
const exprt & | e2, | ||
const exprt & | c, | ||
const std::set< exprt > & | conditions, | ||
const exprt & | decision | ||
) |
To check if the two input controlling exprs are mcdc pairs regarding an atomic expr ''c''.
A mcdc pair of (e1, e2) regarding ''c'' means that ''e1'' and ''e2'' result in different ''decision'' values, and this is caused by the different choice of ''c'' value.
A mcdc pair of controlling exprs regarding ''c'' can have different values for only one atomic expr, i.e., ''c''. Otherwise, they are not a mcdc pair.
Definition at line 614 of file cover.cpp.
References eval_expr(), and values_of_atomic_exprs().
Referenced by has_mcdc_pair().
This method minimizes the controlling conditions for mcdc coverage.
The minimum is in a sense that by deleting any controlling condition in the set, the mcdc coverage for the decision will be not complete.
Iteratively, we test that after removing an item ''x'' from the ''controlling'', can a complete mcdc coverage over ''decision'' still be reserved?
If yes, we update ''controlling'' with the ''new_controlling'' without ''x''; otherwise, we should keep ''x'' within ''controlling''.
If in the end all elements ''x'' in ''controlling'' are reserved, this means that current ''controlling'' set is minimum and the ''while'' loop should be broken out of.
Note: implementation here for the above procedure is not (meant to be) optimal.
If there is no mcdc pair for an atomic condition ''c'', then ''x'' should not be removed from the original ''controlling'' set
Definition at line 700 of file cover.cpp.
References collect_conditions(), and has_mcdc_pair().
Referenced by instrument_cover_goals().
void remove_repetition | ( | std::set< exprt > & | exprs | ) |
After the ''collect_mcdc_controlling_nested'', there can be the recurrence of the same expr in the resulted set of exprs, and this method will remove the repetitive ones.
To check if ''x'' is identical with some expr in ''new_exprs''. Two exprs ''x'' and ''y'' are identical iff they have the same sign for every atomic condition ''c''.
If ''x'' is found identical w.r.t some expr in ''new_conditions, we label it and break.
Definition at line 452 of file cover.cpp.
References collect_conditions(), and sign_of_expr().
Referenced by instrument_cover_goals().
std::set<exprt> replacement_conjunction | ( | const std::set< exprt > & | replacement_exprs, |
const std::vector< exprt > & | operands, | ||
const std::size_t | i | ||
) |
To replace the i-th expr of ''operands'' with each expr inside ''replacement_exprs''.
Definition at line 276 of file cover.cpp.
References conjunction().
Referenced by collect_mcdc_controlling_nested().
The sign of expr ''e'' within the super-expr ''E''.
In the general case, we analyze each operand of ''E''.
Definition at line 395 of file cover.cpp.
References collect_operands(), irept::id(), is_condition(), exprt::make_not(), and exprt::op0().
Referenced by remove_repetition(), and values_of_atomic_exprs().
std::map<exprt, signed> values_of_atomic_exprs | ( | const exprt & | e, |
const std::set< exprt > & | conditions | ||
) |
To obtain values of atomic exprs within the super expr.
Definition at line 586 of file cover.cpp.
References sign_of_expr().
Referenced by is_mcdc_pair().