diff --git a/regression/cbmc-cover/mcdc1/main.c b/regression/cbmc-cover/mcdc1/main.c index 5f8f3869543..002fc28c9a6 100644 --- a/regression/cbmc-cover/mcdc1/main.c +++ b/regression/cbmc-cover/mcdc1/main.c @@ -17,4 +17,6 @@ int main() else { } + + return 1; } diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc index ea1f3ed221a..060d9040829 100644 --- a/regression/cbmc-cover/mcdc1/test.desc +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -3,7 +3,13 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$ +^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$ +^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$ ^\*\* .* of .* covered (100.0%)$ -^\*\* Used 6 iterations$ +^\*\* Used 10 iterations$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc2/main.c b/regression/cbmc-cover/mcdc2/main.c new file mode 100644 index 00000000000..147fe9eb47c --- /dev/null +++ b/regression/cbmc-cover/mcdc2/main.c @@ -0,0 +1,18 @@ +int main() +{ + + __CPROVER_bool A, B, C; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + + if(A||B||C) + { + } + else + { + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc2/test.desc b/regression/cbmc-cover/mcdc2/test.desc new file mode 100644 index 00000000000..6c69a4144b5 --- /dev/null +++ b/regression/cbmc-cover/mcdc2/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 6 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc3/main.c b/regression/cbmc-cover/mcdc3/main.c new file mode 100644 index 00000000000..312cf1a35b6 --- /dev/null +++ b/regression/cbmc-cover/mcdc3/main.c @@ -0,0 +1,8 @@ +int main() +{ + unsigned x, y; + if (!(x>3) && y<5) + ; + + return 1; +} diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc new file mode 100644 index 00000000000..bfbf4d6d094 --- /dev/null +++ b/regression/cbmc-cover/mcdc3/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$ +^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 4 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc4/main.c b/regression/cbmc-cover/mcdc4/main.c new file mode 100644 index 00000000000..08ea1146922 --- /dev/null +++ b/regression/cbmc-cover/mcdc4/main.c @@ -0,0 +1,19 @@ +int main() +{ + + __CPROVER_bool A, B, C, D; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + __CPROVER_input("D", D); + + if((A && B) || (C && D)) + { + } + else + { + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc new file mode 100644 index 00000000000..9d55f2ebf19 --- /dev/null +++ b/regression/cbmc-cover/mcdc4/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$ +^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 9 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc5/main.c b/regression/cbmc-cover/mcdc5/main.c new file mode 100644 index 00000000000..65a7761db1b --- /dev/null +++ b/regression/cbmc-cover/mcdc5/main.c @@ -0,0 +1,18 @@ +int main() +{ + __CPROVER_bool A, B, C, D; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + __CPROVER_input("D", D); + + if((A || B) && (C || D)) + { + } + else + { + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc5/test.desc b/regression/cbmc-cover/mcdc5/test.desc new file mode 100644 index 00000000000..c65bbc9cd1d --- /dev/null +++ b/regression/cbmc-cover/mcdc5/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ +^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 9 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc6/main.c b/regression/cbmc-cover/mcdc6/main.c new file mode 100644 index 00000000000..cebf2b427a0 --- /dev/null +++ b/regression/cbmc-cover/mcdc6/main.c @@ -0,0 +1,8 @@ +int main() +{ + unsigned x; + if(x<3) + ; + + return 1; +} diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc new file mode 100644 index 00000000000..d920e78a57e --- /dev/null +++ b/regression/cbmc-cover/mcdc6/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$ +^\[main.coverage.2\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 2 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc7/main.c b/regression/cbmc-cover/mcdc7/main.c new file mode 100644 index 00000000000..939c0644000 --- /dev/null +++ b/regression/cbmc-cover/mcdc7/main.c @@ -0,0 +1,8 @@ +int main() +{ + signed x, y; + + y = x*123<0 ? 0 : (x*123>100 ? 100 : x*123 ); + + return 1; +} diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc new file mode 100644 index 00000000000..f43810e9e45 --- /dev/null +++ b/regression/cbmc-cover/mcdc7/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 5 function main decision/condition `x \* 123 > 100.* false: SATISFIED$ +^\[main.coverage.2\] file main.c line 5 function main decision/condition `x \* 123 > 100.* true: SATISFIED$ +^\[main.coverage.3\] file main.c line 5 function main decision/condition `x \* 123 < 0.* false: SATISFIED$ +^\[main.coverage.4\] file main.c line 5 function main decision/condition `x \* 123 < 0.* true: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 2 iterations$ +-- +^warning: ignoring diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 648f8441e85..66411824d9f 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -224,7 +224,8 @@ Function: collect_mcdc_controlling_rec Outputs: - Purpose: + Purpose: To recursively collect controlling exprs for + for mcdc coverage. \*******************************************************************/ @@ -233,6 +234,7 @@ void collect_mcdc_controlling_rec( const std::vector &conditions, std::set &result) { + // src is conjunction (ID_and) or disjunction (ID_or) if(src.id()==ID_and || src.id()==ID_or) { @@ -252,6 +254,29 @@ void collect_mcdc_controlling_rec( if(is_condition(op)) { + if(src.id()==ID_or) + { + std::vector others1, others2; + if(not conditions.empty()) + { + others1.push_back(conjunction(conditions)); + others2.push_back(conjunction(conditions)); + } + + for(unsigned j=0; j o=operands; // 'o[i]' needs to be true and false @@ -289,7 +314,28 @@ void collect_mcdc_controlling_rec( else if(src.id()==ID_not) { exprt e=to_not_expr(src).op(); - collect_mcdc_controlling_rec(e, conditions, result); + if(not is_condition(e)) + collect_mcdc_controlling_rec(e, conditions, result); + else + { + // to store a copy of ''src'' + std::vector new_conditions1=conditions; + new_conditions1.push_back(src); + result.insert(conjunction(new_conditions1)); + + // to store a copy of its negation, i.e., ''e'' + std::vector new_conditions2=conditions; + new_conditions2.push_back(e); + result.insert(conjunction(new_conditions2)); + } + } + else + { + /** + * 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. + **/ } } @@ -315,9 +361,598 @@ std::set collect_mcdc_controlling( return result; } + +/*******************************************************************\ + +Function: replacement_conjunction + + Inputs: + + Outputs: + + Purpose: To replace the i-th expr of ''operands'' with each + expr inside ''replacement_exprs''. + +\*******************************************************************/ + +std::set replacement_conjunction( + const std::set &replacement_exprs, + const std::vector &operands, + const int i) +{ + std::set result; + for(auto &y : replacement_exprs) + { + std::vector others; + for(unsigned j=0; j collect_mcdc_controlling_nested( + const std::set &decisions) +{ + // To obtain the 1st-level controlling conditions + std::set controlling = collect_mcdc_controlling(decisions); + + std::set result; + // For each controlling condition, to check if it contains + // non-atomic exprs + for(auto &src : controlling) + { + std::set s1, s2; + /** + * The final controlling conditions resulted from ''src'' + * will be stored in ''s1''; ''s2'' is usd to hold the + * temporary expansion. + **/ + s1.insert(src); + + // dual-loop structure to eliminate complex + // non-atomic-conditional terms + while(true) + { + bool changed=false; + // the 2nd loop + for(auto &x : s1) + { + // if ''x'' is atomic conditional term, there + // is no expansion + if(is_condition(x)) + { + s2.insert(x); + continue; + } + // otherwise, we apply the ''nested'' method to + // each of its operands + std::vector operands; + collect_operands(x, operands); + for(int i=0; i res; + /** + * 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''. + **/ + if(operands[i].id()==ID_not) + { + exprt no=operands[i].op0(); + if(not is_condition(no)) + { + changed=true; + std::set ctrl_no; + ctrl_no.insert(no); + res=collect_mcdc_controlling(ctrl_no); + } + } + else if(not is_condition(operands[i])) + { + changed=true; + std::set ctrl; + ctrl.insert(operands[i]); + res=collect_mcdc_controlling(ctrl); + } + + // To replace a non-atomic expr with its expansion + std::set co= + replacement_conjunction(res, operands, i); + s2.insert(co.begin(), co.end()); + if(res.size() > 0) break; + } + // if there is no change x.r.t current operands of ''x'', + // i.e., they are all atomic, we reserve ''x'' + if(not changed) s2.insert(x); + } + // update ''s1'' and check if change happens + s1=s2; + if(not changed) {break;} + s2.clear(); + } + + // The expansions of each ''src'' should be added into + // the ''result'' + result.insert(s1.begin(), s1.end()); + } + + return result; +} + +/*******************************************************************\ + +Function: sign_of_expr + + Inputs: E should be the pre-processed output by + ''collect_mcdc_controlling_nested'' + + Outputs: +1 : not negated + -1 : negated + + Purpose: The sign of expr ''e'' within the super-expr ''E'' + +\*******************************************************************/ + +std::set sign_of_expr(const exprt &e, const exprt &E) +{ + std::set signs; + + // At fist, we pre-screen the case such that ''E'' + // is an atomic condition + if(is_condition(E)) + { + if(e==E) + signs.insert(+1); + return signs; + } + + // or, ''E'' is the negation of ''e''? + if(E.id()==ID_not) + { + if(e==E.op0()) + { + signs.insert(-1); + return signs; + } + } + + /** + * In the general case, we analyze each operand of ''E''. + **/ + std::vector ops; + collect_operands(E, ops); + for(auto &x : ops) + { + exprt y(x); + if(y == e) signs.insert(+1); + else if(y.id()==ID_not) + { + y.make_not(); + if(y==e) signs.insert(-1); + if(not is_condition(y)) + { + std::set re=sign_of_expr(e, y); + signs.insert(re.begin(), re.end()); + } + } + else if(not is_condition(y)) + { + std::set re=sign_of_expr(e, y); + signs.insert(re.begin(), re.end()); + } + } + + return signs; +} + +/*******************************************************************\ + +Function: remove_repetition + + Inputs: + + Outputs: + + Purpose: 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. + +\*******************************************************************/ + +void remove_repetition(std::set &exprs) +{ + // to obtain the set of atomic conditions + std::set conditions; + for(auto &x: exprs) + { + std::set new_conditions = collect_conditions(x); + conditions.insert(new_conditions.begin(), new_conditions.end()); + } + // exprt that contains multiple (inconsistent) signs should + // be removed + std::set new_exprs; + for(auto &x : exprs) + { + bool kept=true; + for(auto &c : conditions) + { + std::set signs=sign_of_expr(c, x); + if(signs.size()>1) + { + kept=false; + break; + } + } + if(kept) new_exprs.insert(x); + } + exprs=new_exprs; + new_exprs.clear(); + + for(auto &x: exprs) + { + bool red=false; + /** + * 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''. + **/ + for(auto &y: new_exprs) + { + bool iden = true; + for(auto &c : conditions) + { + std::set signs1=sign_of_expr(c, x); + std::set signs2=sign_of_expr(c, y); + int s1=signs1.size(), s2=signs2.size(); + // it is easy to check non-equivalence; + if(s1!=s2) + { + iden=false; + break; + } + else + { + if(s1==0 && s2==0) continue; + // it is easy to check non-equivalence + if(*(signs1.begin())!=*(signs2.begin())) + { + iden=false; + break; + } + } + } + /** + * If ''x'' is found identical w.r.t some + * expr in ''new_conditions, we label it + * and break. + **/ + if(iden) + { + red=true; + break; + } + } + // an expr is added into ''new_exprs'' + // if it is not found repetitive + if(not red) new_exprs.insert(x); + } + + // update the original ''exprs'' + exprs = new_exprs; +} + +/*******************************************************************\ + +Function: eval_expr + + Inputs: + + Outputs: + + Purpose: To evaluate the value of expr ''src'', according to + the atomic expr values + +\*******************************************************************/ +bool eval_expr( + const std::map &atomic_exprs, + const exprt &src) +{ + std::vector operands; + collect_operands(src, operands); + // src is AND + if(src.id()==ID_and) + { + for(auto &x : operands) + if(not eval_expr(atomic_exprs, x)) + return false; + return true; + } + // src is OR + else if(src.id()==ID_or) + { + unsigned fcount=0; + for(auto &x : operands) + if(not eval_expr(atomic_exprs, x)) + fcount++; + if(fcountsecond==+1) + return true; + else //if(atomic_exprs.find(src)->second==-1) + return false; + } +} + +/*******************************************************************\ + +Function: values_of_atomic_exprs + + Inputs: + + Outputs: + + Purpose: To obtain values of atomic exprs within the super expr + +\*******************************************************************/ + +std::map values_of_atomic_exprs( + const exprt &e, + const std::set &conditions) +{ + std::map atomic_exprs; + for(auto &c : conditions) + { + std::set signs=sign_of_expr(c, e); + if(signs.size()==0) + { + // ''c'' is not contained in ''e'' + atomic_exprs.insert(std::pair(c, 0)); + continue; + } + // we do not consider inconsistent expr ''e'' + if(signs.size()!=1) continue; + + atomic_exprs.insert( + std::pair(c, *signs.begin())); + } + return atomic_exprs; +} + +/*******************************************************************\ + +Function: is_mcdc_pair + + Inputs: + + Outputs: + + Purpose: 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. + +\*******************************************************************/ + +bool is_mcdc_pair( + const exprt &e1, + const exprt &e2, + const exprt &c, + const std::set &conditions, + const exprt &decision) +{ + // An controlling expr cannot be mcdc pair of itself + if(e1==e2) return false; + + // To obtain values of each atomic condition within ''e1'' + // and ''e2'' + std::map atomic_exprs_e1= + values_of_atomic_exprs(e1, conditions); + std::map atomic_exprs_e2= + values_of_atomic_exprs(e2, conditions); + + // the sign of ''c'' inside ''e1'' and ''e2'' + signed cs1=atomic_exprs_e1.find(c)->second; + signed cs2=atomic_exprs_e2.find(c)->second; + // a mcdc pair should both contain ''c'', i.e., sign=+1 or -1 + if(cs1==0||cs2==0) + return false; + + // A mcdc pair regarding an atomic expr ''c'' + // should have different values of ''c'' + if(cs1==cs2) + return false; + + // A mcdc pair should result in different ''decision'' + if(eval_expr(atomic_exprs_e1, decision)== + eval_expr(atomic_exprs_e2, decision)) + return false; + + /** + * 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. + **/ + int diff_count=0; + auto e1_it=atomic_exprs_e1.begin(); + auto e2_it=atomic_exprs_e2.begin(); + while(e1_it!=atomic_exprs_e1.end()) + { + if(e1_it->second!=e2_it->second) + diff_count++; + if(diff_count>1) break; + e1_it++; + e2_it++; + } + + if(diff_count==1) return true; + else return false; +} + +/*******************************************************************\ + +Function: has_mcdc_pair + + Inputs: + + Outputs: + + Purpose: To check if we can find the mcdc pair of the + input ''expr_set'' regarding the atomic expr ''c'' + +\*******************************************************************/ + +bool has_mcdc_pair( + const exprt &c, + const std::set &expr_set, + const std::set &conditions, + const exprt &decision) +{ + for(auto y1 : expr_set) + { + for(auto y2 : expr_set) + { + if(is_mcdc_pair(y1, y2, c, conditions, decision)) + { + return true; + } + } + } + return false; +} + +/*******************************************************************\ + +Function: minimize_mcdc_controlling + + Inputs: The input ''controlling'' should have been processed by + ''collect_mcdc_controlling_nested'' + and + ''remove_repetition'' + + Outputs: + + Purpose: 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. + +\*******************************************************************/ + +void minimize_mcdc_controlling( + std::set &controlling, + const exprt &decision) +{ + // to obtain the set of atomic conditions + std::set conditions; + for(auto &x: controlling) + { + std::set new_conditions = collect_conditions(x); + conditions.insert(new_conditions.begin(), new_conditions.end()); + } + + while(true) + { + std::set new_controlling; + bool ctrl_update=false; + /** + * 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 breaked. + * + * Note: implementaion here for the above procedure is + * not (meant to be) optimal. + **/ + for(auto &x : controlling) + { + // To create a new ''controlling'' set without ''x'' + new_controlling.clear(); + for(auto &y : controlling) + if(y!=x) new_controlling.insert(y); + + bool removing_x=true; + // For each atomic expr condition ''c'', to check if its is + // covered by at least a mcdc pair. + for(auto &c : conditions) + { + bool cOK= + has_mcdc_pair(c, new_controlling, conditions, decision); + /** + * If there is no mcdc pair for an atomic condition ''c'', + * then ''x'' should not be removed from the original + * ''controlling'' set + **/ + if(not cOK) + { + removing_x=false; + break; + } + } + + // If ''removing_x'' is valid, it is safe to remove ''x'' + // from the original ''controlling'' + if(removing_x) + { + ctrl_update=true; + break; + } + } + // Update ''controlling'' or break the while loop + if(ctrl_update) + { + controlling=new_controlling; + } + else break; + } +} + +/*******************************************************************\ + Function: collect_decisions_rec Inputs: @@ -648,21 +1283,28 @@ void instrument_cover_goals( std::string comment_t=description+" `"+p_string+"' true"; goto_program.insert_before_swap(i_it); - i_it->make_assertion(p); + //i_it->make_assertion(p); + i_it->make_assertion(not_exprt(p)); i_it->source_location=source_location; i_it->source_location.set_comment(comment_t); i_it->source_location.set_property_class("coverage"); std::string comment_f=description+" `"+p_string+"' false"; goto_program.insert_before_swap(i_it); - i_it->make_assertion(not_exprt(p)); + //i_it->make_assertion(not_exprt(p)); + i_it->make_assertion(p); i_it->source_location=source_location; i_it->source_location.set_comment(comment_f); i_it->source_location.set_property_class("coverage"); } std::set controlling; - controlling=collect_mcdc_controlling(decisions); + //controlling=collect_mcdc_controlling(decisions); + controlling=collect_mcdc_controlling_nested(decisions); + remove_repetition(controlling); + // for now, we restrict to the case of a single ''decision''; + // however, this is not true, e.g., ''? :'' operator. + minimize_mcdc_controlling(controlling, *decisions.begin()); for(const auto & p : controlling) { @@ -672,7 +1314,8 @@ void instrument_cover_goals( "MC/DC independence condition `"+p_string+"'"; goto_program.insert_before_swap(i_it); - i_it->make_assertion(p); + i_it->make_assertion(not_exprt(p)); + //i_it->make_assertion(p); i_it->source_location=source_location; i_it->source_location.set_comment(description); i_it->source_location.set_property_class("coverage");