24 const std::vector<exprt> &conditions,
25 std::set<exprt> &result)
28 if(src.
id() == ID_and || src.
id() == ID_or)
30 std::vector<exprt> operands;
33 if(operands.size() == 1)
35 exprt e = *operands.begin();
38 else if(!operands.empty())
40 for(std::size_t i = 0; i < operands.size(); i++)
42 const exprt op = operands[i];
48 std::vector<exprt> others1, others2;
49 if(!conditions.empty())
55 for(std::size_t j = 0; j < operands.size(); j++)
57 others1.push_back(
not_exprt(operands[j]));
59 others2.push_back(
not_exprt(operands[j]));
61 others2.push_back((operands[j]));
69 std::vector<exprt> o = operands;
72 std::vector<exprt> new_conditions = conditions;
82 std::vector<exprt> others;
83 others.reserve(operands.size() - 1);
85 for(std::size_t j = 0; j < operands.size(); j++)
91 others.push_back(operands[j]);
95 std::vector<exprt> new_conditions = conditions;
96 new_conditions.push_back(c);
103 else if(src.
id() == ID_not)
111 std::vector<exprt> new_conditions1 = conditions;
112 new_conditions1.push_back(src);
116 std::vector<exprt> new_conditions2 = conditions;
117 new_conditions2.push_back(e);
133 std::set<exprt> result;
135 for(
const auto &d : decisions)
144 const std::set<exprt> &replacement_exprs,
145 const std::vector<exprt> &operands,
148 std::set<exprt> result;
149 for(
auto &y : replacement_exprs)
151 std::vector<exprt> others;
152 for(std::size_t j = 0; j < operands.size(); j++)
154 others.push_back(operands[j]);
171 std::set<exprt> result;
174 for(
auto &src : controlling)
176 std::set<exprt>
s1,
s2;
188 bool changed =
false;
201 std::vector<exprt> operands;
204 for(std::size_t i = 0; i < operands.size(); i++)
212 if(operands[i].
id() == ID_not)
214 exprt no = operands[i].op0();
218 std::set<exprt> ctrl_no;
226 std::set<exprt> ctrl;
227 ctrl.insert(operands[i]);
233 s2.insert(co.begin(), co.end());
251 result.insert(
s1.begin(),
s1.end());
263 std::set<signed> signs;
287 std::vector<exprt> ops;
294 else if(y.
id() == ID_not)
302 signs.insert(re.begin(), re.end());
308 signs.insert(re.begin(), re.end());
321 std::set<exprt> conditions;
325 conditions.insert(new_conditions.begin(), new_conditions.end());
329 std::set<exprt> new_exprs;
333 for(
auto &c : conditions)
357 for(
auto &y : new_exprs)
360 for(
auto &c : conditions)
364 int s1 = signs1.size(),
s2 = signs2.size();
373 if(
s1 == 0 &&
s2 == 0)
376 if(*(signs1.begin()) != *(signs2.begin()))
407 std::vector<exprt> operands;
410 if(src.
id() == ID_and)
412 for(
auto &x : operands)
418 else if(src.
id() == ID_or)
420 std::size_t fcount = 0;
422 for(
auto &x : operands)
426 if(fcount < operands.size())
432 else if(src.
id() == ID_not)
442 if(atomic_exprs.find(src)->second == +1)
450 std::map<exprt, signed>
453 std::map<exprt, signed> atomic_exprs;
454 for(
auto &c : conditions)
460 atomic_exprs.insert(std::pair<exprt, signed>(c, 0));
464 if(signs.size() != 1)
467 atomic_exprs.insert(std::pair<exprt, signed>(c, *signs.begin()));
480 const std::set<exprt> &conditions,
481 const exprt &decision)
489 std::map<exprt, signed> atomic_exprs_e1 =
491 std::map<exprt, signed> atomic_exprs_e2 =
495 signed cs1 = atomic_exprs_e1.find(c)->second;
496 signed cs2 = atomic_exprs_e2.find(c)->second;
498 if(cs1 == 0 || cs2 == 0)
519 auto e1_it = atomic_exprs_e1.begin();
520 auto e2_it = atomic_exprs_e2.begin();
521 while(e1_it != atomic_exprs_e1.end())
523 if(e1_it->second != e2_it->second)
541 const std::set<exprt> &expr_set,
542 const std::set<exprt> &conditions,
543 const exprt &decision)
545 for(
auto y1 : expr_set)
547 for(
auto y2 : expr_set)
565 std::set<exprt> &controlling,
566 const exprt &decision)
569 std::set<exprt> conditions;
570 for(
auto &x : controlling)
573 conditions.insert(new_conditions.begin(), new_conditions.end());
578 std::set<exprt> new_controlling;
579 bool ctrl_update =
false;
596 for(
auto &x : controlling)
599 new_controlling.clear();
600 for(
auto &y : controlling)
602 new_controlling.insert(y);
604 bool removing_x =
true;
607 for(
auto &c : conditions)
609 bool cOK =
has_mcdc_pair(c, new_controlling, conditions, decision);
633 controlling = new_controlling;
653 if(!i_it->source_location.is_built_in())
658 std::set<exprt> both;
664 inserter(both, both.end()));
668 for(
const auto &p : both)
670 bool is_decision = decisions.find(p) != decisions.end();
671 bool is_condition = conditions.find(p) != conditions.end();
674 ?
"decision/condition" 675 : is_decision ?
"decision" :
"condition";
677 std::string p_string =
from_expr(
ns, i_it->function, p);
679 std::string comment_t = description +
" `" + p_string +
"' true";
680 const irep_idt function = i_it->function;
684 i_it->source_location = source_location;
688 i_it->source_location.set_function(
function);
689 i_it->function =
function;
691 std::string comment_f = description +
" `" + p_string +
"' false";
694 i_it->make_assertion(p);
695 i_it->source_location = source_location;
699 i_it->source_location.set_function(
function);
700 i_it->function =
function;
703 std::set<exprt> controlling;
709 INVARIANT(!decisions.empty(),
"There must be at least one decision");
712 for(
const auto &p : controlling)
714 std::string p_string =
from_expr(
ns, i_it->function, p);
716 std::string description =
717 "MC/DC independence condition `" + p_string +
"'";
719 const irep_idt function = i_it->function;
723 i_it->source_location = source_location;
727 i_it->source_location.set_function(
function);
728 i_it->function =
function;
731 for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++)
std::set< exprt > collect_decisions(const exprt &src)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void collect_operands(const exprt &src, std::vector< exprt > &dest)
void set_comment(const irep_idt &comment)
void remove_repetition(std::set< exprt > &exprs)
After the ''collect_mcdc_controlling_nested'', there can be the recurrence of the same expr in the re...
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void instrument(goto_programt &, goto_programt::targett &, const cover_blocks_baset &) const override
Override this method to implement an instrumenter.
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''.
Coverage Instrumentation.
bool is_condition(const exprt &src)
#define INVARIANT(CONDITION, REASON)
exprt conjunction(const exprt::operandst &op)
const irep_idt & id() const
std::set< exprt > collect_conditions(const exprt &src)
void minimize_mcdc_controlling(std::set< exprt > &controlling, const exprt &decision)
This method minimizes the controlling conditions for mcdc coverage.
instructionst::iterator targett
std::set< signed > sign_of_expr(const exprt &e, const exprt &E)
The sign of expr ''e'' within the super-expr ''E''.
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.
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.
const irep_idt coverage_criterion
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''...
Coverage Instrumentation Utilities.
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.
std::set< exprt > collect_mcdc_controlling(const std::set< exprt > &decisions)
A generic container class for the GOTO intermediate representation of one function.
Base class for all expressions.
const irep_idt property_class
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
goto_programt & goto_program
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''...
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...
bool is_non_cover_assertion(goto_programt::const_targett t) const