Revision 54d032f5 src/normalization.ml
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