package p4spectec
P4-SpecTec: A mechanization toolchain for the P4 Programming Language
Install
dune-project
Dependency
Authors
Maintainers
Sources
v0.1.2.tar.gz
md5=1a3bc0a385fe1ecf403c019f49aa6de6
sha512=5d20b5821f33e2a3a5419b208606f27c01511994c2b3b1e1cdf4c077056dfd0aa81682af0720e1060ee2bfb0341918fcc4c53159820205a2bc32b725e5c1a714
doc/p4spectec.backend_sim/Backend_sim/V1model/Func/Make/argument-1-Spec/Rel/index.html
Module Spec.Rel
type call_rel =
string ->
Backend_sim.Spec_impl.Rel.Value.t list ->
Backend_sim.Spec_impl.Rel.Value.t listval register : call_rel -> unitval lvalue_read_var :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
Backend_sim.Spec_impl.Rel.Value.tval lvalue_read_var_global :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
Backend_sim.Spec_impl.Rel.Value.tval lvalue_read_dot :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
string ->
Backend_sim.Spec_impl.Rel.Value.tval lvalue_read_dot_global :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
string ->
Backend_sim.Spec_impl.Rel.Value.tval lvalue_write_var :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.tval lvalue_write_dot :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
string ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.tval lvalue_write_var_local :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.tval lvalue_write_dot_global :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
string ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.tval lvalue_write_dot_local :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
string ->
string ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.tval v1model_init_packet_in :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.tval v1model_init_packet_out :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.tval v1model_init_globals :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.IO.port ->
Backend_sim.Spec_impl.Rel.Value.tval v1model_setup_preserved_meta_fields :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.tval ebpf_init_globals :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.tval psa_ingress_init_packet_in :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.tval psa_ingress_init_packet_out :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.tval psa_ingress_init_metadata :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.IO.port ->
string ->
Backend_sim.Spec_impl.Rel.Value.tval psa_ingress_init_globals :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.IO.port ->
Backend_sim.Spec_impl.Rel.Value.tval psa_egress_init_packet_in :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.tval psa_egress_init_packet_out :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.tval psa_egress_init_metadata :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.IO.port ->
string ->
int ->
int ->
Backend_sim.Spec_impl.Rel.Value.tval psa_egress_init_globals :
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.Value.t ->
Backend_sim.Spec_impl.Rel.IO.port ->
Backend_sim.Spec_impl.Rel.Value.t