Project

General

Profile

Revision 66359a5e src/pathConditions.ml

View differences:

src/pathConditions.ml
100 100
     let vl, neg = neg_list l in
101 101
     vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
102 102
       
103
  | Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> (
103
  | Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) -> (
104 104
    let list = [i; t; e] in
105 105
    let vl, neg = neg_list list in
106 106
    vl, combine (fun l ->
......
141 141
       (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
142 142
       args'
143 143

  
144
  | Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool ->
144
  | Expr_ident _ when (Types.is_bool_type expr.expr_type) ->
145 145
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
146 146
  | _ -> [] (* empty vars *) , [] 
147 147
and gen_mcdc_cond_var v expr =
......
199 199
  | _ -> []
200 200

  
201 201
let mcdc_var_def v expr = 
202
  match (Types.repr expr.expr_type).Types.tdesc with
203
  | Types.Tbool ->
202
  if Types.is_bool_type expr.expr_type then
204 203
     let vl = gen_mcdc_cond_var v expr in
205 204
     vl
206
  | _ -> let vl = mcdc_expr 0 expr in
207
	 vl
208

  
205
  else
206
    let vl = mcdc_expr 0 expr in
207
    vl
208
      
209 209
let mcdc_node_eq eq =
210 210
  let vl =
211
    match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
212
    | [lhs], Types.Tbool, _ ->  gen_mcdc_cond_var lhs eq.eq_rhs 
213
    | _::_, Types.Ttuple tl, Expr_tuple rhs ->
211
    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 
213
    | _::_, false, Types.Ttuple tl, Expr_tuple rhs ->
214 214
       (* We iterate trough pairs, but accumulate variables aside. The resulting
215 215
	  expression shall remain a tuple defintion *)
216 216
       let vl = List.fold_right2 (fun lhs rhs accu ->
......
248 248
       Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
249 249
       let cov_id = Format.flush_str_formatter () in
250 250
       let cov_var = mkvar_decl loc
251
	 (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None) in
251
	 (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in
252 252
       let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
253
       cov_var, cov_def
253
       cov_var, cov_def, cov_expr
254 254
     ) fresh_cov_defs
255 255
     in
256
     let fresh_vars, fresh_eqs = List.split fresh_cov_vars in
257
     let fresh_annots =
256
     let fresh_vars, fresh_eqs =
257
       List.fold_right
258
	 (fun (v,eq,_) (accuv, accueq)-> v::accuv, eq::accueq )
259
	 fresh_cov_vars
260
	 ([], [])
261
     in
262
     let fresh_annots = (* We produce two sets of annotations: PROPERTY ones for
263
			   kind2, and regular ones to keep track of the nature
264
			   of the annotations. *)
258 265
       List.map
259
	 (fun v -> {annots =  [["PROPERTY"], expr_to_eexpr (expr_of_vdecl v)]; annot_loc = td.top_decl_loc})
260
	 fresh_vars in
261
     Format.printf "We have %i coverage criteria for node %s@." nb_total nd.node_id;
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
272
     in
273
     Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id;
262 274
     (* And add them as annotations --%PROPERTY: var TODO *)
263 275
     {td with top_decl_desc = Node {nd with
264 276
       node_locals = nd.node_locals@fresh_vars;
......
284 296
      | _ -> assert false);
285 297
  List.map mcdc_top_decl prog
286 298

  
299

  
300
    
287 301
(* Local Variables: *)
288 302
(* compile-command:"make -C .." *)
289 303
(* End: *)

Also available in: Unified diff