Project

General

Profile

Revision 54d032f5 src/normalization.ml

View differences:

src/normalization.ml
65 65
  if List.exists (fun v -> v.var_id = s) vars then aux () else
66 66
  {
67 67
    var_id = s;
68
    var_orig = false;
68 69
    var_dec_type = dummy_type_dec;
69 70
    var_dec_clock = dummy_clock_dec;
70 71
    var_dec_const = false;
......
371 372
     - compute the associated expression without aliases     
372 373
  *)
373 374
  let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
375
  let split_defs = Splitting.tuple_split_eq_list defs in
374 376
  let norm_traceability = {
375
    annots =
376
      List.map 
377
	(fun v -> 
378
	  let expr = substitute_expr diff_vars defs (
379
	    let eq = try
380
		       List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs 
381
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
382
	    eq.eq_rhs) in 
383
	  let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
384
	  ["horn_backend";"trace"], pair 
385
	)
386
    diff_vars ;
377
    annots = List.map (fun v ->
378
      let eq =
379
	try
380
	  List.find (fun eq -> eq.eq_lhs = [v.var_id]) split_defs 
381
	with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
382
      let expr = substitute_expr diff_vars split_defs eq.eq_rhs in
383
      let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
384
      (["horn_backend";"trace"], pair)
385
    ) diff_vars;
387 386
    annot_loc = Location.dummy_loc
388 387
  }
389 388

  

Also available in: Unified diff