Project

General

Profile

« Previous | Next » 

Revision 15c3e4e7

Added by LĂ©lio Brun 11 months ago

generic ACSL spec generation

View differences:

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