Revision 3ca6d126 src/backends/Horn/horn_backend.ml
| src/backends/Horn/horn_backend.ml | ||
|---|---|---|
| 564 | 564 |
|
| 565 | 565 |
let translate fmt basename prog machines = |
| 566 | 566 |
List.iter (print_machine machines fmt) (List.rev machines); |
| 567 |
|
|
| 568 | 567 |
main_print machines fmt |
| 569 | 568 |
|
| 570 | 569 |
|
| ... | ... | |
| 579 | 578 |
let traces : (ident * expr) list= |
| 580 | 579 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
| 581 | 580 |
let filtered = |
| 582 |
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
|
|
| 581 |
List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
|
|
| 583 | 582 |
in |
| 584 | 583 |
let content = List.map snd filtered in |
| 585 | 584 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
| ... | ... | |
| 620 | 619 |
List.map (fun (p, v) -> |
| 621 | 620 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
| 622 | 621 |
let traces = List.assoc machine machines_traces in |
| 623 |
if List.mem_assoc v.var_id traces then |
|
| 622 |
if List.mem_assoc v.var_id traces then (
|
|
| 624 | 623 |
(* We take the expression associated to variable v in the trace info *) |
| 624 |
(* Format.eprintf "Found variable %a in traces: %a@." pp_var v Printers.pp_expr (List.assoc v.var_id traces); *) |
|
| 625 | 625 |
p, List.assoc v.var_id traces |
| 626 |
else |
|
| 626 |
) |
|
| 627 |
else ( |
|
| 627 | 628 |
(* We keep the variable as is: we create an expression v *) |
| 629 |
(* Format.eprintf "Unable to found variable %a in traces (%a)@." pp_var v (Utils.fprintf_list ~sep:", " Format.pp_print_string) (List.map fst traces); *) |
|
| 628 | 630 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
| 631 |
) |
|
| 629 | 632 |
|
| 630 | 633 |
) (compute_mems m) |
| 631 | 634 |
in |
| 632 | 635 |
let memories_next = (* We remove the topest pre in each expression *) |
| 633 | 636 |
List.map |
| 634 |
(fun (prefix, ee) -> |
|
| 635 |
match ee.expr_desc with |
|
| 636 |
| Expr_pre e -> prefix, e |
|
| 637 |
| _ -> Format.eprintf |
|
| 638 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
|
| 639 |
(Utils.fprintf_list ~sep:"," |
|
| 640 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
|
| 641 |
(List.rev prefix) |
|
| 642 |
Printers.pp_expr ee; |
|
| 643 |
assert false) |
|
| 637 |
(fun (prefix, ee) ->
|
|
| 638 |
match ee.expr_desc with
|
|
| 639 |
| Expr_pre e -> prefix, e
|
|
| 640 |
| _ -> Format.eprintf
|
|
| 641 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
|
|
| 642 |
(Utils.fprintf_list ~sep:","
|
|
| 643 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
|
|
| 644 |
(List.rev prefix)
|
|
| 645 |
Printers.pp_expr ee;
|
|
| 646 |
assert false)
|
|
| 644 | 647 |
memories_old |
| 645 | 648 |
in |
| 646 | 649 |
|
| ... | ... | |
| 680 | 683 |
|
| 681 | 684 |
|
| 682 | 685 |
(* Local Variables: *) |
| 683 |
(* compile-command:"make -C .." *) |
|
| 686 |
(* compile-command:"make -C ../.." *)
|
|
| 684 | 687 |
(* End: *) |
Also available in: Unified diff