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