Revision 8cacf677
Added by Pierre-Loïc Garoche about 5 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