Model verification with optional message fields

[rssen]

Model verification fails if a message defines optional fields that are referenced in a subsequent expression.

The following example yields:

test.rflx:28:67: model: error: undefined variable "Pad_Length"
test.rflx:28:67: model: info: on path Payload_Length -> Frame_Type -> Flag_Padded -> Data -> Padding

Pad_Length is optional, that means it only is part of the message if Frame_Type = DATA and Flag_Padded = True.
The Path Payload_Length -> Frame_Type -> Flag_Padded -> Data -> Padding cannot be a valid Path as Flag_Padded = True implies the occurrence of Pad_Length and Padded. A Path where Pad_Length is absent but Padding is present cannot exist.

package Test is

   type Frame_Type is (
      DATA => 0,
      HEADERS => 1
   ) with Size => 8;

   type Payload_Length is mod 2**8;
   type Pad_Length is mod 2**8;

   type Message is
      message
         Payload_Length : Payload_Length;
         Frame_Type : Frame_Type;
         Flag_Padded : Boolean
            then Pad_Length
               if Frame_Type = DATA and Flag_Padded = True
            then Data
               with Size => Payload_Length * 8
               if (Frame_Type  = HEADERS or Frame_Type = DATA) and Flag_Padded = False;
         Pad_Length : Pad_Length
            then Data with Size => (Payload_Length - Pad_Length) * 8;
         Data : Opaque
            then Padding with Size => Pad_Length * 8
               if Flag_Padded = True
            then null;
         Padding : Opaque;
   end message;

end Test;

[treiher]

There seems to be an error in your specification. Flag_Padded should be unconditionally present on every path. Otherwise it is not possible to check Flag_Padded = True at the outgoing edge of Data.

I guess the following specification shows the actual problem (please correct me if I'm wrong):

package Test is

   type T is mod 2**8;

   type M is
      message
         Flag : T
            then Opt1
               if Flag = 1
            then Data
               if Flag /= 1;
         Opt1 : T;
         Data : Opaque
            with Size => 8
            then Opt2
               if Flag = 1
            then null
               if Flag /= 1;
         Opt2 : Opaque
            with Size => Opt1 * 8;
      end message;

test.rflx:20:26: model: error: undefined variable "Opt1"
test.rflx:20:26: model: info: on path Flag -> Data -> Opt2

The type checking of expressions is done on every possible path without considering any condition, even if the path cannot occur in practice (e.g., Opt1 and Opt2 have the same condition and cannot exist separately). The issue can be solved by filtering out all impossible paths before type checking.