Revision 8cacf677
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 
modelchecker 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