Revision 2104c80a
Added by PierreLoï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