cprover
|
Coverage Instrumentation for MC/DC. More...
#include "cover_instrument.h"
#include <langapi/language_util.h>
#include <algorithm>
#include <iterator>
#include "cover_util.h"
Go to the source code of this file.
Functions | |
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... | |
Coverage Instrumentation for MC/DC.
Definition in file cover_instrument_mcdc.cpp.
Definition at line 129 of file cover_instrument_mcdc.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.
Definition at line 164 of file cover_instrument_mcdc.cpp.
References collect_mcdc_controlling(), collect_operands(), is_condition(), and replacement_conjunction().
Referenced by cover_mcdc_instrumentert::instrument().
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.
Definition at line 22 of file cover_instrument_mcdc.cpp.
References collect_operands(), conjunction(), irept::id(), is_condition(), unary_exprt::op(), and to_not_expr().
Referenced by collect_mcdc_controlling().
To evaluate the value of expr ''src'', according to the atomic expr values.
Definition at line 394 of file cover_instrument_mcdc.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 526 of file cover_instrument_mcdc.cpp.
References is_mcdc_pair().
Referenced by minimize_mcdc_controlling().
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.
Definition at line 465 of file cover_instrument_mcdc.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.
Definition at line 551 of file cover_instrument_mcdc.cpp.
References collect_conditions(), and has_mcdc_pair().
Referenced by cover_mcdc_instrumentert::instrument().
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.
Definition at line 311 of file cover_instrument_mcdc.cpp.
References collect_conditions(), and sign_of_expr().
Referenced by cover_mcdc_instrumentert::instrument().
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 141 of file cover_instrument_mcdc.cpp.
References conjunction().
Referenced by collect_mcdc_controlling_nested().
The sign of expr ''e'' within the super-expr ''E''.
Definition at line 256 of file cover_instrument_mcdc.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 440 of file cover_instrument_mcdc.cpp.
References sign_of_expr().
Referenced by is_mcdc_pair().