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