Project

General

Profile

Revision ea1c2906 src/normalization.ml

View differences:

src/normalization.ml
372 372
  let new_locals = List.filter is_local vars in
373 373
  (* Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals; *)
374 374

  
375
  (* Compute traceability info: 
376
     - gather newly bound variables
377
     - compute the associated expression without aliases     
378
  *)
379
  let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
380
  let norm_traceability = {
381
    annots = List.map (fun v ->
382
      let eq =
383
	try
384
	  List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs 
385
	with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
386
      let expr = substitute_expr diff_vars defs eq.eq_rhs in
387
      let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
388
      (["traceability"], pair)
389
    ) diff_vars;
390
    annot_loc = Location.dummy_loc
391
  }
392

  
375
  let new_annots =
376
    if !Options.traces then
377
      begin
378
	(* Compute traceability info: 
379
	   - gather newly bound variables
380
	   - compute the associated expression without aliases     
381
	*)
382
	let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
383
	let norm_traceability = {
384
	  annots = List.map (fun v ->
385
	    let eq =
386
	      try
387
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs 
388
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
389
	    let expr = substitute_expr diff_vars defs eq.eq_rhs in
390
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
391
	    (["traceability"], pair)
392
	  ) diff_vars;
393
	  annot_loc = Location.dummy_loc
394
	} 
395
	in
396
	norm_traceability::node.node_annot
397
      end
398
    else
399
      node.node_annot
393 400
  in
401

  
394 402
  let node =
395 403
  { node with 
396 404
    node_locals = new_locals; 
397 405
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
398 406
    node_asserts = asserts;
399
    node_annot = norm_traceability::node.node_annot;
407
    node_annot = new_annots;
400 408
  }
401 409
  in ((*Printers.pp_node Format.err_formatter node;*) 
402 410
    node

Also available in: Unified diff