Project

General

Profile

« Previous | Next » 

Revision 8cacf677

Added by Pierre-Loïc Garoche almost 7 years ago

[lustrec/mcdc/ improved the MCDC output

View differences:

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