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/spectec/Spectec/Sli/Unboot/index.html

Module Sli.Unboot

val unboot_param_mtchtbl : Lang.Sl.param Runtime.Value.Get.mtchtbl Stdlib.ref
val unboot_holdcase_mtchtbl : Lang.Sl.holdcase Runtime.Value.Get.mtchtbl Stdlib.ref
val unboot_guard_mtchtbl : Lang.Sl.guard Runtime.Value.Get.mtchtbl Stdlib.ref
val unboot_instr_mtchtbl : Lang.Sl.instr Runtime.Value.Get.mtchtbl Stdlib.ref
val unboot_def_mtchtbl : Lang.Sl.def Runtime.Value.Get.mtchtbl Stdlib.ref
val unboot_iterinstr : Runtime.Value.t -> Lang.Sl.iterinstr
val unboot_iterinstrs : Runtime.Value.t -> Lang.Sl.iterinstr list
val unboot_param : Runtime.Value.t -> Lang.Sl.param
val unboot_exp_param : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.param
val unboot_def_param : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.param
val unboot_params : Runtime.Value.t -> Lang.Sl.param list
val unboot_instr : Runtime.Value.t -> Lang.Sl.instr
val unboot_if_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_holdcase : Runtime.Value.t -> Lang.Sl.holdcase
val unboot_both_holdcase : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.holdcase
val unboot_hold_holdcase : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.holdcase
val unboot_nothold_holdcase : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.holdcase
val unboot_hold_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_guard : Runtime.Value.t -> Lang.Sl.guard
val unboot_bool_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_cmp_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_sub_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_match_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_mem_guard : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.guard
val unboot_case : Runtime.Value.t -> Lang.Sl.case
val unboot_cases : Runtime.Value.t -> Lang.Sl.case list
val unboot_case_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_group_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_let_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_rule_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_result_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_return_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_debug_instr : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.instr
val unboot_instrs : Runtime.Value.t -> Lang.Sl.block
val unboot_block : Runtime.Value.t -> Lang.Sl.block
val unboot_block_opt : Runtime.Value.t -> Lang.Sl.block option
val unboot_tablerow : Runtime.Value.t -> Lang.Sl.tablerow
val unboot_tablerows : Runtime.Value.t -> Lang.Sl.tablerow list
val unboot_def : Runtime.Value.t -> Lang.Sl.def
val unboot_extern_typ_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_typ_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_extern_rel_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_rel_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_extern_func_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_builtin_func_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_table_func_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_func_def : Util.Source.region -> Runtime.Value.t list -> Lang.Sl.def
val unboot_script : Runtime.Value.t -> Lang.Sl.spec