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);
131 std::set<exprt> result;
133 for(
const auto &d : decisions)
142 const std::set<exprt> &replacement_exprs,
143 const std::vector<exprt> &operands,
146 std::set<exprt> result;
147 for(
auto &y : replacement_exprs)
149 std::vector<exprt> others;
150 for(std::size_t j = 0; j < operands.size(); j++)
152 others.push_back(operands[j]);
169 std::set<exprt> result;
172 for(
auto &src : controlling)
174 std::set<exprt>
s1,
s2;
185 bool changed =
false;
198 std::vector<exprt> operands;
201 for(std::size_t i = 0; i < operands.size(); i++)
207 if(operands[i].
id() == ID_not)
209 exprt no = operands[i].op0();
213 std::set<exprt> ctrl_no;
221 std::set<exprt> ctrl;
222 ctrl.insert(operands[i]);
228 s2.insert(co.begin(), co.end());
246 result.insert(
s1.begin(),
s1.end());
258 std::set<signed> signs;
280 std::vector<exprt> ops;
287 else if(y.
id() == ID_not)
295 signs.insert(re.begin(), re.end());
301 signs.insert(re.begin(), re.end());
314 std::set<exprt> conditions;
318 conditions.insert(new_conditions.begin(), new_conditions.end());
322 std::set<exprt> new_exprs;
326 for(
auto &c : conditions)
348 for(
auto &y : new_exprs)
351 for(
auto &c : conditions)
355 int s1 = signs1.size(),
s2 = signs2.size();
364 if(
s1 == 0 &&
s2 == 0)
367 if(*(signs1.begin()) != *(signs2.begin()))
396 std::vector<exprt> operands;
399 if(src.
id() == ID_and)
401 for(
auto &x : operands)
407 else if(src.
id() == ID_or)
409 std::size_t fcount = 0;
411 for(
auto &x : operands)
415 if(fcount < operands.size())
421 else if(src.
id() == ID_not)
431 if(atomic_exprs.find(src)->second == +1)
439 std::map<exprt, signed>
442 std::map<exprt, signed> atomic_exprs;
443 for(
auto &c : conditions)
449 atomic_exprs.insert(std::pair<exprt, signed>(c, 0));
453 if(signs.size() != 1)
456 atomic_exprs.insert(std::pair<exprt, signed>(c, *signs.begin()));
469 const std::set<exprt> &conditions,
470 const exprt &decision)
478 std::map<exprt, signed> atomic_exprs_e1 =
480 std::map<exprt, signed> atomic_exprs_e2 =
484 signed cs1 = atomic_exprs_e1.find(c)->second;
485 signed cs2 = atomic_exprs_e2.find(c)->second;
487 if(cs1 == 0 || cs2 == 0)
506 auto e1_it = atomic_exprs_e1.begin();
507 auto e2_it = atomic_exprs_e2.begin();
508 while(e1_it != atomic_exprs_e1.end())
510 if(e1_it->second != e2_it->second)
528 const std::set<exprt> &expr_set,
529 const std::set<exprt> &conditions,
530 const exprt &decision)
532 for(
auto y1 : expr_set)
534 for(
auto y2 : expr_set)
552 std::set<exprt> &controlling,
553 const exprt &decision)
556 std::set<exprt> conditions;
557 for(
auto &x : controlling)
560 conditions.insert(new_conditions.begin(), new_conditions.end());
565 std::set<exprt> new_controlling;
566 bool ctrl_update =
false;
581 for(
auto &x : controlling)
584 new_controlling.clear();
585 for(
auto &y : controlling)
587 new_controlling.insert(y);
589 bool removing_x =
true;
592 for(
auto &c : conditions)
594 bool cOK =
has_mcdc_pair(c, new_controlling, conditions, decision);
616 controlling = new_controlling;
636 if(!i_it->source_location.is_built_in())
641 std::set<exprt> both;
647 inserter(both, both.end()));
651 for(
const auto &p : both)
653 bool is_decision = decisions.find(p) != decisions.end();
654 bool is_condition = conditions.find(p) != conditions.end();
657 ?
"decision/condition" 658 : is_decision ?
"decision" :
"condition";
660 std::string p_string =
from_expr(
ns, i_it->function, p);
662 std::string comment_t = description +
" `" + p_string +
"' true";
663 const irep_idt function = i_it->function;
666 i_it->source_location = source_location;
670 i_it->source_location.set_function(
function);
671 i_it->function =
function;
673 std::string comment_f = description +
" `" + p_string +
"' false";
675 i_it->make_assertion(p);
676 i_it->source_location = source_location;
680 i_it->source_location.set_function(
function);
681 i_it->function =
function;
684 std::set<exprt> controlling;
689 if(!decisions.empty())
694 for(
const auto &p : controlling)
696 std::string p_string =
from_expr(
ns, i_it->function, p);
698 std::string description =
699 "MC/DC independence condition `" + p_string +
"'";
701 const irep_idt function = i_it->function;
704 i_it->source_location = source_location;
708 i_it->source_location.set_function(
function);
709 i_it->function =
function;
712 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)
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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