Revision ea1c2906 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