Revision 2104c80a
Added by Pierre-Loïc Garoche almost 4 years ago
| src/pathConditions.ml | ||
|---|---|---|
| 64 | 64 |
) (IdSet.elements all) |
| 65 | 65 |
|
| 66 | 66 |
|
| 67 |
(* In a previous version, the printer was introducing fake description, ie
|
|
| 68 |
tautologies, over inout variables to make sure they were not suppresed by
|
|
| 69 |
some other algorithms *) |
|
| 67 |
(* In a previous version, the printer was introducing fake |
|
| 68 |
description, ie tautologies, over inout variables to make sure they
|
|
| 69 |
were not suppresed by some other algorithms *)
|
|
| 70 | 70 |
|
| 71 |
(* Takes the variable on which these coverage criteria will apply, as well as
|
|
| 72 |
the expression and its negated version. Returns the expr and the variable
|
|
| 73 |
expression, as well as the two new boolean expressions descibing the two
|
|
| 74 |
associated modes. *) |
|
| 75 |
let mcdc_var vi_as_expr expr expr_neg_vi = |
|
| 71 |
(* Takes the variable on which these coverage criteria will apply, as |
|
| 72 |
well as the expression and its negated version. Returns the expr
|
|
| 73 |
and the variable expression, as well as the two new boolean
|
|
| 74 |
expressions descibing the two associated modes. *)
|
|
| 75 |
let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =
|
|
| 76 | 76 |
let loc = expr.expr_loc in |
| 77 |
let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in |
|
| 78 | 77 |
let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in |
| 79 |
let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in |
|
| 80 |
let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in |
|
| 78 |
let expr1, expr2 = |
|
| 79 |
if nb_elems > 1 then |
|
| 80 |
let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in |
|
| 81 |
let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in |
|
| 82 |
let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in |
|
| 83 |
expr1, expr2 |
|
| 84 |
else |
|
| 85 |
vi_as_expr, not_vi_as_expr |
|
| 86 |
in |
|
| 81 | 87 |
((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom |
| 82 | 88 |
true while expr2 |
| 83 | 89 |
corresponds to atom |
| ... | ... | |
| 102 | 108 |
| Expr_tuple l -> |
| 103 | 109 |
let vl, neg = neg_list l in |
| 104 | 110 |
vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
|
| 105 |
|
|
| 111 |
|
|
| 106 | 112 |
| Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) -> ( |
| 107 | 113 |
let list = [i; t; e] in |
| 108 | 114 |
let vl, neg = neg_list list in |
| 109 | 115 |
vl, combine (fun l -> |
| 110 |
match l with |
|
| 111 |
| [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
|
|
| 112 |
| _ -> assert false |
|
| 113 |
) neg list |
|
| 116 |
match l with
|
|
| 117 |
| [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
|
|
| 118 |
| _ -> assert false
|
|
| 119 |
) neg list
|
|
| 114 | 120 |
) |
| 115 | 121 |
| Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *) |
| 116 | 122 |
let vl = gen_mcdc_cond_guard i in |
| 117 | 123 |
let list = [i; t; e] in |
| 118 | 124 |
let vl', neg = neg_list list in |
| 119 | 125 |
vl@vl', combine (fun l -> |
| 120 |
match l with |
|
| 121 |
| [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
|
|
| 122 |
| _ -> assert false |
|
| 123 |
) neg list |
|
| 126 |
match l with
|
|
| 127 |
| [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
|
|
| 128 |
| _ -> assert false
|
|
| 129 |
) neg list
|
|
| 124 | 130 |
) |
| 125 | 131 |
| Expr_arrow (e1, e2) -> |
| 126 | 132 |
let vl1, e1' = compute_neg_expr cpt_pre e1 in |
| 127 | 133 |
let vl2, e2' = compute_neg_expr cpt_pre e2 in |
| 128 | 134 |
vl1@vl2, combine (fun l -> match l with |
| 129 |
| [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
|
|
| 130 |
| _ -> assert false |
|
| 131 |
) [e1'; e2'] [e1; e2] |
|
| 135 |
| [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
|
|
| 136 |
| _ -> assert false
|
|
| 137 |
) [e1'; e2'] [e1; e2]
|
|
| 132 | 138 |
|
| 133 | 139 |
| Expr_pre e -> |
| 134 | 140 |
let vl, e' = compute_neg_expr (cpt_pre+1) e in |
| 135 | 141 |
vl, List.map |
| 136 |
(fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
|
|
| 142 |
(fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
|
|
| 137 | 143 |
|
| 138 | 144 |
| Expr_appl (op_name, args, r) when List.mem op_name rel_op -> |
| 139 | 145 |
[], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] |
| ... | ... | |
| 141 | 147 |
| Expr_appl (op_name, args, r) -> |
| 142 | 148 |
let vl, args' = compute_neg_expr cpt_pre args in |
| 143 | 149 |
vl, List.map |
| 144 |
(fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
|
|
| 145 |
args' |
|
| 150 |
(fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
|
|
| 151 |
args'
|
|
| 146 | 152 |
|
| 147 | 153 |
| Expr_ident _ when (Types.is_bool_type expr.expr_type) -> |
| 148 | 154 |
[], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]] |
| 149 | 155 |
| _ -> [] (* empty vars *) , [] |
| 150 | 156 |
and gen_mcdc_cond_var v expr = |
| 151 | 157 |
report ~level:1 (fun fmt -> |
| 152 |
Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@." |
|
| 153 |
v |
|
| 154 |
Printers.pp_expr expr); |
|
| 158 |
Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@."
|
|
| 159 |
v
|
|
| 160 |
Printers.pp_expr expr);
|
|
| 155 | 161 |
let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in |
| 156 |
if List.length leafs_n_neg_expr >= 1 then ( |
|
| 162 |
let len = List.length leafs_n_neg_expr in |
|
| 163 |
if len >= 1 then ( |
|
| 157 | 164 |
List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) -> |
| 158 |
(mcdc_var (mk_pre nb_pre vi) expr expr_neg_vi)::accu
|
|
| 159 |
) vl leafs_n_neg_expr |
|
| 165 |
(mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi)::accu
|
|
| 166 |
) vl leafs_n_neg_expr
|
|
| 160 | 167 |
) |
| 161 | 168 |
else |
| 162 |
(* TODO: deal with the case length xxx = 1 with a simpler condition *) |
|
| 163 | 169 |
vl |
| 164 | 170 |
|
| 165 | 171 |
and gen_mcdc_cond_guard expr = |
| 166 | 172 |
report ~level:1 (fun fmt -> |
| 167 |
Format.fprintf fmt".. Generating MC/DC cond for guard %a@." |
|
| 168 |
Printers.pp_expr expr); |
|
| 173 |
Format.fprintf fmt".. Generating MC/DC cond for guard %a@."
|
|
| 174 |
Printers.pp_expr expr);
|
|
| 169 | 175 |
let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in |
| 170 |
if List.length leafs_n_neg_expr >= 1 then ( |
|
| 176 |
let len = List.length leafs_n_neg_expr in |
|
| 177 |
if len >= 1 then ( |
|
| 171 | 178 |
List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) -> |
| 172 |
(mcdc_var (mk_pre nb_pre vi) expr expr_neg_vi)::accu
|
|
| 173 |
) vl leafs_n_neg_expr) |
|
| 179 |
(mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi)::accu
|
|
| 180 |
) vl leafs_n_neg_expr)
|
|
| 174 | 181 |
else |
| 175 |
(* TODO: deal with the case length xxx = 1 with a simpler condition *) |
|
| 176 | 182 |
vl |
| 177 | 183 |
|
| 178 | 184 |
|
Also available in: Unified diff
Addressed a TODO in MCDC Pathconditions: simpler condition for single expression