Revision 8cacf677
Added by Pierre-Loïc Garoche almost 7 years ago
src/pathConditions.ml | ||
---|---|---|
78 | 78 |
let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in |
79 | 79 |
let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in |
80 | 80 |
let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in |
81 |
((expr,vi_as_expr),[expr1;expr2]) |
|
81 |
((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom |
|
82 |
true while expr2 |
|
83 |
corresponds to atom |
|
84 |
false *) |
|
82 | 85 |
|
83 | 86 |
(* Format.printf "%a@." Printers.pp_expr expr1; *) |
84 | 87 |
(* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *) |
... | ... | |
209 | 212 |
let mcdc_node_eq eq = |
210 | 213 |
let vl = |
211 | 214 |
match eq.eq_lhs, Types.is_bool_type eq.eq_rhs.expr_type, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with |
212 |
| [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs
|
|
215 |
| [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs |
|
213 | 216 |
| _::_, false, Types.Ttuple tl, Expr_tuple rhs -> |
214 | 217 |
(* We iterate trough pairs, but accumulate variables aside. The resulting |
215 | 218 |
expression shall remain a tuple defintion *) |
... | ... | |
235 | 238 |
| Node nd -> |
236 | 239 |
let new_coverage_exprs = |
237 | 240 |
List.fold_right ( |
238 |
fun s accu_v -> |
|
241 |
fun s accu_v ->
|
|
239 | 242 |
let vl' = mcdc_node_stmt s in |
240 | 243 |
vl'@accu_v |
241 |
) nd.node_stmts []
|
|
244 |
) nd.node_stmts []
|
|
242 | 245 |
in |
243 |
(* We add coverage vars as boolean internal flows. TODO *)
|
|
244 |
let fresh_cov_defs = List.flatten (List.map snd new_coverage_exprs) in
|
|
246 |
(* We add coverage vars as boolean internal flows. *) |
|
247 |
let fresh_cov_defs = List.flatten (List.map (fun ((_, atom), expr_l) -> List.map (fun (atom_valid, case) -> atom, atom_valid, case) expr_l) new_coverage_exprs) in
|
|
245 | 248 |
let nb_total = List.length fresh_cov_defs in |
246 |
let fresh_cov_vars = List.mapi (fun i cov_expr ->
|
|
247 |
let loc = cov_expr.expr_loc in
|
|
248 |
Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
|
|
249 |
let cov_id = Format.flush_str_formatter () in
|
|
250 |
let cov_var = mkvar_decl loc
|
|
251 |
(cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in |
|
252 |
let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
|
|
253 |
cov_var, cov_def, cov_expr
|
|
254 |
) fresh_cov_defs
|
|
249 |
let fresh_cov_vars = List.mapi (fun i (atom, atom_valid, cov_expr) ->
|
|
250 |
let loc = cov_expr.expr_loc in
|
|
251 |
Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
|
|
252 |
let cov_id = Format.flush_str_formatter () in
|
|
253 |
let cov_var = mkvar_decl loc
|
|
254 |
(cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in
|
|
255 |
let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
|
|
256 |
cov_var, cov_def, atom, atom_valid
|
|
257 |
) fresh_cov_defs
|
|
255 | 258 |
in |
256 | 259 |
let fresh_vars, fresh_eqs = |
257 | 260 |
List.fold_right |
258 |
(fun (v,eq,_) (accuv, accueq)-> v::accuv, eq::accueq ) |
|
261 |
(fun (v,eq,_,_) (accuv, accueq)-> v::accuv, eq::accueq )
|
|
259 | 262 |
fresh_cov_vars |
260 | 263 |
([], []) |
261 | 264 |
in |
... | ... | |
263 | 266 |
kind2, and regular ones to keep track of the nature |
264 | 267 |
of the annotations. *) |
265 | 268 |
List.map |
266 |
(fun v -> let ee = expr_to_eexpr (expr_of_vdecl v) in |
|
267 |
{annots = [["PROPERTY"], ee; |
|
268 |
["coverage";"mcdc"], ee |
|
269 |
]; |
|
270 |
annot_loc = v.var_loc}) |
|
271 |
fresh_vars |
|
269 |
(fun (v, _, atom, atom_valid) -> |
|
270 |
let e = expr_of_vdecl v in |
|
271 |
let ee = expr_to_eexpr e in |
|
272 |
let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [e]) in |
|
273 |
{annots = [["PROPERTY"], neg_ee; (* Using negated property to force |
|
274 |
model-checker to produce a |
|
275 |
suitable covering trace *) |
|
276 |
let _ = Printers.pp_expr Format.str_formatter atom in |
|
277 |
let atom_as_string = Format.flush_str_formatter () in |
|
278 |
let valid = if atom_valid then "true" else "false" in |
|
279 |
["coverage";"mcdc";atom_as_string;valid], ee |
|
280 |
]; |
|
281 |
annot_loc = v.var_loc}) |
|
282 |
fresh_cov_vars |
|
272 | 283 |
in |
273 | 284 |
Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id; |
274 | 285 |
(* And add them as annotations --%PROPERTY: var TODO *) |
275 | 286 |
{td with top_decl_desc = Node {nd with |
276 |
node_locals = nd.node_locals@fresh_vars;
|
|
277 |
node_stmts = nd.node_stmts@fresh_eqs;
|
|
278 |
node_annot = nd.node_annot@fresh_annots
|
|
279 |
}}
|
|
287 |
node_locals = nd.node_locals@fresh_vars;
|
|
288 |
node_stmts = nd.node_stmts@fresh_eqs;
|
|
289 |
node_annot = nd.node_annot@fresh_annots
|
|
290 |
}}
|
|
280 | 291 |
| _ -> td |
281 | 292 |
|
282 | 293 |
|
Also available in: Unified diff
[lustrec/mcdc/ improved the MCDC output