Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / seal_verifier.ml @ a703ed0c

History | View | Annotate | Download (1.06 KB)

1
open Seal_utils
2

    
3
let active = ref false
4

    
5
(* Select the appropriate node, should have been inlined already and
6
   extract update/output functions. *)
7
let seal_run basename prog machines =
8
  let node_name =
9
    match !Options.main_node with
10
    | "" -> assert false
11
    | s -> s
12
  in
13
  let m = Machine_code_common.get_machine machines node_name in
14
  let nd = m.mname in
15
  Format.eprintf "Node %a@." Printers.pp_node nd; 
16
  let mems = m.mmemory in
17
  Format.eprintf "Mems: %a@." (Utils.fprintf_list ~sep:"; " Printers.pp_var) mems;
18
  let msch = Utils.desome m.msch in
19
  let deps = msch.Scheduling_type.dep_graph in
20
  Format.eprintf "graph: %a@." Causality.pp_dep_graph deps;
21
  let sliced_nd = slice_node mems deps nd in
22
  Format.eprintf "Node %a@." Printers.pp_node sliced_nd; 
23
  ()
24
  
25
module Verifier =
26
  (struct
27
    include VerifierType.Default
28
    let name = "seal"
29
    let options = []
30
    let activate () =
31
      active := true;
32
      Options.global_inline := true
33
      
34
    let is_active () = !active
35
    let run = seal_run
36
      
37
                    
38
  end: VerifierType.S)
39