Revision 66359a5e src/pathConditions.ml
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 
(* compilecommand:"make C .." *) 
289  303 
(* End: *) 
Also available in: Unified diff