Revision 15c3e4e7
Added by LĂ©lio Brun almost 4 years ago
src/causality.ml | ||
---|---|---|
544 | 544 |
maybe removing shorter branches *) |
545 | 545 |
type disjoint_map = (ident, CISet.t) Hashtbl.t |
546 | 546 |
|
547 |
let pp_ciset fmt t = |
|
548 |
begin |
|
549 |
Format.fprintf fmt "{@ "; |
|
550 |
CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t; |
|
551 |
Format.fprintf fmt "}@." |
|
552 |
end |
|
547 |
let pp_ciset fmt t = let open Format in |
|
548 |
pp_print_braced' ~pp_sep:pp_print_space Printers.pp_var_name fmt |
|
549 |
(CISet.elements t) |
|
553 | 550 |
|
554 | 551 |
let clock_disjoint_map vdecls = |
555 | 552 |
let map = Hashtbl.create 23 in |
... | ... | |
602 | 599 |
end |
603 | 600 |
|
604 | 601 |
let pp_disjoint_map fmt map = |
605 |
begin |
|
606 |
Format.fprintf fmt "{ /* disjoint map */@."; |
|
607 |
Hashtbl.iter (fun k v -> Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map; |
|
608 |
Format.fprintf fmt "}@." |
|
609 |
end |
|
602 |
Format.(fprintf fmt "@[<v 2>{ /* disjoint map */%t@] }" |
|
603 |
(fun fmt -> |
|
604 |
Hashtbl.iter (fun k v -> |
|
605 |
fprintf fmt "@,%s # %a" |
|
606 |
k (pp_print_braced' Printers.pp_var_name) |
|
607 |
(CISet.elements v)) map)) |
|
610 | 608 |
end |
611 | 609 |
|
612 | 610 |
|
613 | 611 |
let pp_dep_graph fmt g = |
614 |
begin |
|
615 |
Format.fprintf fmt "{ /* graph */@."; |
|
616 |
IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "%s -> %s@." s t) g; |
|
617 |
Format.fprintf fmt "}@." |
|
618 |
end |
|
612 |
Format.fprintf fmt "@[<v 2>{ /* graph */%t@] }" |
|
613 |
(fun fmt -> |
|
614 |
IdentDepGraph.iter_edges (fun s t -> Format.fprintf fmt "@,%s -> %s" s t) g) |
|
619 | 615 |
|
620 | 616 |
let pp_error fmt err = |
621 | 617 |
match err with |
Also available in: Unified diff
generic ACSL spec generation