Project

General

Profile

Revision a703ed0c src/tools/seal_verifier.ml

View differences:

src/tools/seal_verifier.ml
1
open Seal_utils
2

  
1 3
let active = ref false
2 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
  
3 25
module Verifier =
4 26
  (struct
5 27
    include VerifierType.Default
6 28
    let name = "seal"
7 29
    let options = []
8
    let activate () = active := true
30
    let activate () =
31
      active := true;
32
      Options.global_inline := true
33
      
9 34
    let is_active () = !active
10
    let run basename prog machines = ()
35
    let run = seal_run
36
      
11 37
                    
12 38
  end: VerifierType.S)
13 39
    

Also available in: Unified diff