Project

General

Profile

Revision 0d79d0f3 src/tools/seal_verifier.ml

View differences:

src/tools/seal_verifier.ml
1
open Seal_slice
2
open Seal_extract
1 3
open Seal_utils
2 4

  
3 5
let active = ref false
......
7 9
let seal_run basename prog machines =
8 10
  let node_name =
9 11
    match !Options.main_node with
10
    | "" -> assert false
12
    | "" -> (
13
      Format.eprintf "SEAL verifier requires a main node.@.";
14
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
15
        (Utils.fprintf_list ~sep:"@ "
16
           (fun fmt m ->
17
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
18
           )
19
        )
20
        machines; 
21
      exit 1
22
    )
11 23
    | s -> s
12 24
  in
13 25
  let m = Machine_code_common.get_machine machines node_name in
......
19 31
  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)
20 32
  let sliced_nd = slice_node mems msch nd in
21 33
  (* Format.eprintf "Sliced Node %a@." Printers.pp_node sliced_nd; *)
34
  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");
22 35
  let sw_init, sw_sys = node_as_switched_sys mems sliced_nd in
23 36
  let pp_res =
24 37
    (Utils.fprintf_list ~sep:"@ "
25 38
       (fun fmt (gel, up) ->
26
         Format.fprintf fmt "@[<v 2>%a:@ %a@]"
39
         Format.fprintf fmt "@[<v 2>[%a]:@ %a@]"
27 40
           (Utils.fprintf_list ~sep:"; "
28 41
              (fun fmt (e,b) ->
29 42
                if b then Printers.pp_expr fmt e
30 43
                else Format.fprintf fmt "not(%a)"
31 44
                       Printers.pp_expr e)) gel
32
           (Utils.fprintf_list ~sep:"; "
45
           (Utils.fprintf_list ~sep:";@ "
33 46
              (fun fmt (id, e) ->
34
                Format.fprintf fmt "%s = %a"
47
                Format.fprintf fmt "%s = @[<hov 0>%a@]"
35 48
                  id
36 49
                  Printers.pp_expr e)) up
37 50
    ))
38 51
  in
52
  report ~level:1 (
53
      fun fmt -> Format.fprintf fmt
54
                   "%i memories, %i init, %i step switch cases@."
55
                   (List.length mems)
56
                   (List.length sw_init)
57
                   (List.length sw_sys)
58
               
59
    );
39 60
  report ~level:1 (fun fmt ->
40 61
      Format.fprintf fmt "@[<v 0>@[<v 3>Init:@ %a@]@ "
41 62
        pp_res sw_init;

Also available in: Unified diff