Project

General

Profile

Revision 15003796 src/normalization.ml

View differences:

src/normalization.ml
374 374
	   - gather newly bound variables
375 375
	   - compute the associated expression without aliases
376 376
	*)
377
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
377
	let diff_vars = List.fold_left (fun accu v -> if not (List.mem v node.node_locals) then v.var_id :: accu else accu ) [] new_locals in
378 378
	let norm_traceability = {
379
	  annots = List.map (fun v ->
379
	  annots = List.map (fun vid ->
380 380
	    let eq =
381 381
	      try
382
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs) 
383
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
384
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
385
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
382
		List.find (fun eq -> eq.eq_lhs = [vid]) (defs@assert_defs) 
383
	      with Not_found -> (Format.eprintf "var not found %s@." vid; assert false) in
384
	    let expr = substitute_expr ~open_pre:true diff_vars (defs@assert_defs) eq.eq_rhs in
385
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident vid expr.expr_loc; expr])) in
386 386
	    (["traceability"], pair)
387 387
	  ) diff_vars;
388 388
	  annot_loc = Location.dummy_loc

Also available in: Unified diff