verified-network-toolchain / petr4

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

Enums cannot have default values (initializer) #367

Closed pataei closed 1 year ago

pataei commented 1 year ago

In enum well-formedness rule: Petr4 doesn't allow for an enum to have default values (initializer) for constants, however, P4 spec does. Here's an example.

pataei commented 1 year ago

Wrong! Here's the code:

    | SerializableEnum of
        { tags: 'a;
          annotations: Annotation.t list;
          typ: Type.t [@key "type"];
          name: P4String.t;
          members: (P4String.t * Expression.t) list }