26 const std::vector<exprt> &conditions,
27 std::set<exprt> &result)
32 std::vector<exprt> operands;
35 if(operands.size() == 1)
37 exprt e = *operands.begin();
40 else if(!operands.empty())
42 for(std::size_t i = 0; i < operands.size(); i++)
44 const exprt op = operands[i];
51 if(!conditions.empty())
57 for(std::size_t j = 0; j < operands.size(); j++)
63 others2.push_back((operands[j]));
71 std::vector<exprt> o = operands;
85 others.reserve(operands.size() - 1);
87 for(std::size_t j = 0; j < operands.size(); j++)
93 others.push_back(operands[j]);
133 std::set<exprt> result;
145 const std::vector<exprt> &operands,
148 std::set<exprt> result;
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;
176 std::set<exprt>
s1,
s2;
187 bool changed =
false;
200 std::vector<exprt> operands;
203 for(std::size_t i = 0; i < operands.size(); i++)
209 if(operands[i].
id() ==
ID_not)
223 std::set<exprt>
ctrl;
224 ctrl.insert(operands[i]);
230 s2.insert(
co.begin(),
co.end());
248 result.insert(
s1.begin(),
s1.end());
260 std::set<signed>
signs;
282 std::vector<exprt>
ops;
284 for(
const auto &
x :
ops)
315 std::set<exprt> conditions;
327 for(
auto &
c : conditions)
352 for(
auto &
c : conditions)
365 if(
s1 == 0 &&
s2 == 0)
397 std::vector<exprt> operands;
402 for(
auto &
x : operands)
412 for(
auto &
x : operands)
416 if(
fcount < operands.size())
438std::map<exprt, signed>
442 for(
auto &
c : conditions)
452 if(
signs.size() != 1)
468 const std::set<exprt> &conditions,
527 const std::set<exprt> &expr_set,
528 const std::set<exprt> &conditions,
531 for(
auto y1 : expr_set)
533 for(
auto y2 : expr_set)
555 std::set<exprt> conditions;
591 for(
auto &
c : conditions)
630 i_it->turn_into_skip();
637 if(!
i_it->source_location().is_built_in())
642 std::set<exprt>
both;
652 for(
const auto &p :
both)
655 bool is_condition = conditions.find(p) != conditions.end();
658 ?
"decision/condition"
696 std::string description =
697 "MC/DC independence condition '" +
p_string +
"'";
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const irep_idt property_class
const irep_idt coverage_criterion
bool is_non_cover_assertion(goto_programt::const_targett t) const
std::function< goto_programt::instructiont(const exprt &, const source_locationt &)> assertion_factoryt
The type of function used to make goto_program assertions.
void instrument(const irep_idt &function_id, goto_programt &, goto_programt::targett &, const cover_blocks_baset &, const assertion_factoryt &) const override
Override this method to implement an instrumenter.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A generic container class for the GOTO intermediate representation of one function.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
const irep_idt & id() const
Coverage Instrumentation.
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''.
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''.
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::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.
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.
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.
void minimize_mcdc_controlling(std::set< exprt > &controlling, const exprt &decision)
This method minimizes the controlling conditions for mcdc coverage.
std::set< exprt > collect_mcdc_controlling(const std::set< exprt > &decisions)
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< signed > sign_of_expr(const exprt &e, const exprt &E)
The sign of expr ''e'' within the super-expr ''E''.
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...
void collect_operands(const exprt &src, std::vector< exprt > &dest)
std::set< exprt > collect_decisions(const goto_programt::const_targett t)
bool is_condition(const exprt &src)
std::set< exprt > collect_conditions(const exprt &src)
Coverage Instrumentation Utilities.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.