package p4spectec

You can search for identifiers within the package.

in-package search v0.2.0

P4-SpecTec: A mechanization toolchain for the P4 Programming Language

Install

dune-project

Dependency

md5=1a3bc0a385fe1ecf403c019f49aa6de6

sha512=5d20b5821f33e2a3a5419b208606f27c01511994c2b3b1e1cdf4c077056dfd0aa81682af0720e1060ee2bfb0341918fcc4c53159820205a2bc32b725e5c1a714

module Value = Runtime.Value

module Dep = Runtime.Testgen_neg.Dep

Sourceval handlers : (module Handler.HANDLER) list Stdlib.ref

Sourceval register : (module Handler.HANDLER) list -> unit

Sourceval is_active : unit -> bool

Sourceval init_spec : Handler.spec -> unit

Sourceval finish : unit -> unit

Sourceval backup : unit -> unit

Sourceval restore : unit -> unit

Sourceval on_program : Inst.Handler.Value.t -> unit

Sourceval on_value : Inst.Handler.Value.t -> unit

val on_value_dependency : 
  Inst.Handler.Value.t ->
  Inst.Handler.Value.t ->
  Inst.Handler.Dep.Edges.label ->
  unit

Sourceval on_rel_enter : Domain.Lib.RId.t -> Inst.Handler.Value.t list -> unit

Sourceval on_rel_exit : Domain.Lib.RId.t -> unit

Sourceval on_func_enter : Domain.Lib.FId.t -> Inst.Handler.Value.t list -> unit

Sourceval on_func_exit : Domain.Lib.FId.t -> unit

Sourceval on_prem : Lang.Il.prem -> unit

Sourceval on_instr : Lang.Sl.instr -> unit

val on_instr_dangling : 
  bool ->
  Domain.Lib.IId.t ->
  Inst.Handler.Value.t ->
  unit