package p4spectec

  1. Overview
  2. Docs
P4-SpecTec: A mechanization toolchain for the P4 Programming Language

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (2)

Authors

  1. K
    KAIST PLRG

Maintainers

  1. 9
    99jaehyunlee@kaist.ac.kr

Sources

v0.1.2.tar.gz
md5=1a3bc0a385fe1ecf403c019f49aa6de6
sha512=5d20b5821f33e2a3a5419b208606f27c01511994c2b3b1e1cdf4c077056dfd0aa81682af0720e1060ee2bfb0341918fcc4c53159820205a2bc32b725e5c1a714

doc/src/inst/handler.ml.html

Source file handler.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
open Domain.Lib
open Lang
module Value = Runtime.Value
module Dep = Runtime.Testgen_neg.Dep
module Run = Runtime.Dynamic_Runner.Signature
module ICov = Coverage.Instr.Single

type spec = Run.spec

(* Handler signature *)

module type HANDLER = sig
  (* Initialization and finalization *)

  val init_spec : spec -> unit
  val finish : unit -> unit

  (* Backup and restore *)

  val backup : unit -> unit
  val restore : unit -> unit

  (* Common events - values *)

  val on_program : Value.t -> unit
  val on_value : Value.t -> unit
  val on_value_dependency : Value.t -> Value.t -> Dep.Edges.label -> unit

  (* Common events - relations, functions, and iterations *)

  val on_rel_enter : RId.t -> Value.t list -> unit
  val on_rel_exit : RId.t -> unit
  val on_func_enter : FId.t -> Value.t list -> unit
  val on_func_exit : FId.t -> unit

  (* IL events *)

  val on_prem : Il.prem -> unit

  (* SL events *)

  val on_instr : Sl.instr -> unit
  val on_instr_dangling : bool -> IId.t -> Value.t -> unit
end

(* Default handler *)

module Default : HANDLER = struct
  (* Initialization and finalization *)

  let init_spec _ = ()
  let finish () = ()

  (* Backup and restore *)

  let backup () = ()
  let restore () = ()

  (* Common events *)

  let on_program _ = ()
  let on_value _ = ()
  let on_value_dependency _ _ _ = ()
  let on_rel_enter _ _ = ()
  let on_rel_exit _ = ()
  let on_func_enter _ _ = ()
  let on_func_exit _ = ()

  (* IL events *)

  let on_prem _ = ()

  (* SL events *)

  let on_instr _ = ()
  let on_instr_dangling _ _ _ = ()
end