verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
74 stars 20 forks source link

well-formed rules of fixed-length integers are loose #366

Open pataei opened 1 year ago

pataei commented 1 year ago

Petr4 doesn't check the length of a fixed-length integer, either signed or unsigned. However, the P4 spec specifies that for signed integers the length must be more than 1 and for unsigned integers the length must be equal or more than zero.

pataei commented 1 year ago

In P4light this is enforced statically.