Project

General

Profile

Revision 3ca6d126 src/normalization.ml

View differences:

src/normalization.ml
127 127
	(Clocks.clock_list_of_clock expr.expr_clock) in
128 128
    let new_def =
129 129
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
130
    in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
130
    in
131
    (* Format.eprintf "Checkign def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
132
    (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
131 133

  
132 134
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
133 135
   and [opt] is true *)
......
383 385
	with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
384 386
      let expr = substitute_expr diff_vars defs eq.eq_rhs in
385 387
      let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
386
      (["horn_backend";"trace"], pair)
387
    ) [] (*diff_vars*);
388
      (["traceability"], pair)
389
    ) diff_vars;
388 390
    annot_loc = Location.dummy_loc
389 391
  }
390 392

  

Also available in: Unified diff