Project

General

Profile

Revision c95a441d

View differences:

src/pathConditions.ml
271 271
       List.map
272 272
	 (fun (v, _, atom, atom_valid) ->
273 273
	  let e = expr_of_vdecl v in
274
	  let ee = expr_to_eexpr e in
275 274
	  let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [e]) in
276 275
	  {annots =  [["PROPERTY"], neg_ee; (* Using negated property to force
277 276
                                               model-checker to produce a
278 277
                                               suitable covering trace *)
279
		      let _ = Printers.pp_expr Format.str_formatter atom in
280
		      let atom_as_string = Format.flush_str_formatter () in
281
		      let valid = if atom_valid then "true" else "false" in
282
		      ["coverage";"mcdc";atom_as_string;valid], ee
278
                      let loc = Location.dummy_loc in
279
		      let valid_e = let open Corelang in mkexpr loc (Expr_const (const_of_bool atom_valid)) in
280
		      ["coverage";"mcdc";v.var_id], expr_to_eexpr (Corelang.expr_of_expr_list loc [e; atom; valid_e])
283 281
		     ];
284 282
	   annot_loc = v.var_loc})
285 283
	 fresh_cov_vars

Also available in: Unified diff