Receiving GigE Vision Packets with Ada Types — Pitfalls of Representation Clauses and a SPARK-Proved Parser

GigE Vision cameras send the images they capture as UDP packets using GVSP (GigE Vision Streaming Protocol)¹. The receiver reads the header at the start of each packet to learn which image the packet belongs to and where it falls in the sequence, and then assembles the image. If the header is read incorrectly, a short or broken packet makes the receiver read past the end of the receive buffer.

An Ada record representation clause specifies where each field sits in the byte sequence². You can write the header layout diagram directly as a type. Overlaying that type on a received byte sequence, however, has pitfalls. This article compares a header type written with a representation clause against functions that read the byte sequence one field at a time, and uses SPARK to prove that the reading functions never read out of range, whatever packet arrives.

To state the conclusion first: for byte sequences arriving from the network, it is safer to check the length and then read one field at a time. A representation-clause type is better suited to documenting the layout, or to use after the length and values have been checked.

On November 10, 2026, I built and ran the code locally with GNAT 13.3.0 on Ubuntu 24.04. The proofs were done on a GitHub Actions Ubuntu 24.04 runner with GNATprove (FSF 16.1.0) installed through Alire. Building and running with Alire’s GNAT 16.1.0 on the same runner produced the same output as locally. No real camera was connected; the packets tested are byte sequences assembled by hand. The GigE Vision specification is distributed by A3 (Association for Advancing Automation)³, but I did not consult it for this article. The field layout was written by cross-checking the publicly available GVSP dissector in Wireshark⁴ against the definitions in Aravis, an open-source camera library⁵. Items found in neither are not covered.

GVSP packets and the header layout

A camera sends one image as three kinds of packets: leader, payload and trailer. The leader carries the image width, height and pixel format, the payloads carry the pixel data, and the trailer signals the end of the image. Besides these three, both Wireshark and Aravis define formats that combine leader, payload and trailer into one, and formats such as H.264⁴⁵.

flowchart TB
        accTitle: Order of the GVSP packets that carry one image
        accDescr: Shows that a camera sends one image as a leader, several payloads and a trailer in that order, and that the receiver assembles the image using the block ID and packet ID.
        A["Camera"] --> B["Leader (width, height, pixel format)"]
        B --> C["Several payloads (pixel data)"]
        C --> D["Trailer (end of image)"]
        D --> E["Receiver assembles by ID"]

Figure 1: One image is sent as a leader, payloads and a trailer in that order, and the receiver assembles it by block ID and packet ID.

Every packet starts with a header, and the header starts with a 2-byte status code. Below, byte offsets are counted from 0 at the start of the packet. The header comes in two forms. The most significant bit of the byte at offset 4 is the extended-ID flag: 0 means an 8-byte standard-ID header, and 1 means a 20-byte extended-ID header. In both forms the remaining 7 bits of the byte at offset 4 give the packet format: 1 is leader, 2 is trailer and 3 is payload. All values are big-endian (most significant byte first)⁴⁵.

flowchart TB
        accTitle: Standard-ID header (8 bytes)
        accDescr: Shows that a standard-ID header consists of a 2-byte status code, a 2-byte block ID, one byte holding the extended-ID flag and the format, and a 3-byte packet ID, in that order.
        A["Offsets 0–1: status code"] --> B["Offsets 2–3: block ID (16 bits)"]
        B --> C["Offset 4: extended-ID flag (1 bit)"]
        C --> C2["Offset 4: format (7 bits)"]
        C2 --> D["Offsets 5–7: packet ID (24 bits)"]

Figure 2: A standard-ID header is 8 bytes, with a 16-bit block ID and a 24-bit packet ID.

In an extended-ID header, the block ID grows to 64 bits and the packet ID to 32 bits. Offsets 2–3, which hold the block ID in a standard-ID header, carry flags instead; Wireshark defines bits there such as one indicating a resent packet. Offsets 5–7 are not used for the packet ID, which moves to the 4 bytes starting at offset 16⁴⁵.

flowchart TB
        accTitle: Extended-ID header (20 bytes)
        accDescr: Shows that an extended-ID header consists of the status code, flags, the extended-ID flag and format, 3 unused bytes, a 64-bit block ID and a 32-bit packet ID, in that order.
        A["Offsets 0–1: status code"] --> B["Offsets 2–3: flags"]
        B --> C["Offset 4: extended-ID flag and format"]
        C --> D["Offsets 5–7: not used for the packet ID"]
        D --> E["Offsets 8–15: block ID (64 bits)"]
        E --> F["Offsets 16–19: packet ID (32 bits)"]

Figure 3: An extended-ID header is 20 bytes, and its block ID and packet ID sit at different offsets from the standard ID.

In an image leader, 36 bytes of information follow the header. Cross-checking the Wireshark and Aravis definitions gives the layout below. This article does not read the first 2 bytes (Wireshark decodes only the first byte, as Field Info, while Aravis defines the 2 bytes as 16-bit flags). A Payload Type of 0x0001 means an image, and the 0x4000 bit means additional information (chunk) follows the image⁴⁵.

In the diagram a solid line marks a relation that always holds and a dashed line marks a conditional one (the conditions are given per relation on the detail page). The full list of relations (7 in total, with evidence and certainty) and the definitions of the main concepts are collected on the knowledge map detail page (in Japanese). Data: JSON-LD / Turtle

Writing the header as a type with a representation clause

Turning the standard-ID header into an Ada type with a representation clause looks like this. The number after at is the byte offset from the start of the record, and the range after range is the range of bits counted from that byte.

with Interfaces; use Interfaces;
with System;

package Gvsp_Layout is

   type Format_Code is
     (Leader, Trailer, Payload, All_In, H264, Multi_Zone, Multi_Part, Gen_DC);
   for Format_Code use
     (Leader => 1, Trailer => 2, Payload => 3, All_In => 4,
      H264 => 5, Multi_Zone => 6, Multi_Part => 7, Gen_DC => 8);
   for Format_Code'Size use 7;

   type Packet_Id_24 is mod 2 ** 24;

   --  Standard-ID header (8 bytes)
   type Standard_Header is record
      Status      : Unsigned_16;
      Block_Id    : Unsigned_16;
      Extended_Id : Boolean;
      Format      : Format_Code;
      Packet_Id   : Packet_Id_24;
   end record
     with Bit_Order            => System.High_Order_First,
          Scalar_Storage_Order => System.High_Order_First,
          Size                 => 64;

   for Standard_Header use record
      Status      at 0 range 0 .. 15;
      Block_Id    at 2 range 0 .. 15;
      Extended_Id at 4 range 0 .. 0;
      Format      at 4 range 1 .. 7;
      Packet_Id   at 5 range 0 .. 23;
   end record;

end Gvsp_Layout;

The header diagram and the type declaration correspond one to one, so this style is easy to read when checking the layout. The format is an enumeration, and for Format_Code use assigns 1–8 to its values.

The two aspects on the type play different roles.

• Bit_Order is a standard Ada attribute that decides how bit numbers in the representation clause are counted. With High_Order_First, bit 0 is the most significant bit⁶. This matches the numbering used in network header diagrams, so the extended-ID flag can be written as at 4 range 0 .. 0.
• Scalar_Storage_Order is an attribute specific to GNAT; standard Ada does not have it. It decides the byte order in which integers inside the record are stored in memory⁷. The GNAT manual requires that, when it is specified on a record, it have the same value as Bit_Order.

flowchart TB
        accTitle: Roles of Bit_Order and Scalar_Storage_Order
        accDescr: Shows that Bit_Order decides how bit numbers in the representation clause are counted, Scalar_Storage_Order decides the byte order of multi-byte integers, and only both together read a big-endian header correctly.
        A["Record type with a representation clause"] --> B["Bit_Order (standard attribute)"]
        A --> C["Scalar_Storage_Order (GNAT-specific)"]
        B --> D["Bit numbering changes"]
        C --> E["Integer byte order changes"]
        D --> F["Both together read correctly"]
        E --> F

Figure 4: Bit_Order decides how bit numbers are counted, and Scalar_Storage_Order decides the byte order of integers.

To confirm that Bit_Order alone is not enough, I read the same 4 bytes, 00 00 00 2A, with two types. One type has only Bit_Order; the other also has Scalar_Storage_Order. Both place the block ID at offsets 2–3. The result on x86-64 is:

Without Scalar_Storage_Order: Block_Id = 10752
With Scalar_Storage_Order: Block_Id = 42

10752 is 0x2A00 in hexadecimal. Because x86-64 is little-endian, the type with only Bit_Order read the byte that comes first in memory as the low-order byte, and 42 became 10752.

Next, an 8-byte sequence is converted to Standard_Header with Ada.Unchecked_Conversion and read. The source type of the conversion is an 8-element subtype of Gvsp.Byte_Array, the same type used by the parser described later.

   subtype Header_Bytes is Byte_Array (0 .. 7);

   function To_Header is
     new Ada.Unchecked_Conversion (Header_Bytes, Standard_Header);

   procedure Show (Label : String; Packet : Byte_Array) is
   begin
      declare
         H : constant Standard_Header :=
           To_Header (Packet (Packet'First .. Packet'First + 7));
      begin
         Put (Label & ": Block_Id =" & H.Block_Id'Image
              & " Packet_Id =" & H.Packet_Id'Image);
         if H.Format'Valid then
            Put_Line (" Format = " & H.Format'Image);
         else
            Put_Line (" Format is an invalid value");
         end if;
      end;
   exception
      when Constraint_Error =>
         Put_Line (Label & ": Constraint_Error");
   end Show;

I passed three packets: a correct header with format 3 (payload), a broken header whose format byte is 0x09, and a packet only 5 bytes long.

Good  : Block_Id = 42 Packet_Id = 258 Format = PAYLOAD
Broken: Block_Id = 42 Packet_Id = 258 Format is an invalid value
Short : Constraint_Error

The correct header was read as block ID 42 and packet ID 258 (0x000102). The other two hit the pitfalls described next.

Pitfalls of overlaying a type on a byte sequence

Reading the header with a representation-clause type has four pitfalls.

flowchart TB
        accTitle: Pitfalls of reading by overlaying a type
        accDescr: Shows that overlaying a representation-clause type on a received byte sequence causes problems in four places: overlaying by address, short packets, invalid format values, and the length difference caused by the extended ID.
        A["Overlay on received bytes"] --> B["Overlay by address"]
        A --> C["Short packet"]
        A --> D["Bad format value"]
        A --> E["Extended ID"]
        B --> F["GNAT does not support storage-order types"]
        C --> G["Too few bytes"]
        D --> H["Invalid enum value"]
        E --> I["One type cannot express it"]

Figure 5: Reading by overlaying a type causes problems in four places: address, length, values and header form.

GNAT does not guarantee the behavior of overlaying by address

You can also place a record at the address of the receive buffer (with Address => Buffer'Address), much like a pointer to a C struct. For an object with a specified address, however, the programmer must guarantee that the address is appropriate for the type. If it is not, execution is erroneous (a state whose result the language does not define)⁸. The same applies when the address does not satisfy the type’s Alignment. In addition, the GNAT manual says that overlays that change the scalar storage order are not supported and that such code draws a warning. What it does support is conversion with Ada.Unchecked_Conversion⁷. That is why the examples in this article use conversion.

In fact, compiling a declaration that overlays a Standard_Header with Scalar_Storage_Order on the address of a Byte_Array with GNAT 13.3.0 produced this warning:

overlay_warning.adb:7:59: warning: overlay changes scalar storage order [enabled by default]

A short packet does not fill the size of the type

The conversion needs exactly 8 bytes. Trying to slice 8 bytes out of a 5-byte packet makes Ada raise Constraint_Error from the array range check. The Short line above is the result. Unlike overlaying a pointer to a C struct, Ada does not silently read out of range.

However, in a build with checks suppressed, such as with -gnatp, this check disappears too. Reading out of range with checks suppressed makes execution erroneous⁹. And even with the check in place, an exception in the receive loop stops reception unless it is caught.

An unexpected Format value leaves the enumeration invalid

Converting a header whose format byte is 0x09 puts a value into Format that is none of 1–8. Ada calls a representation that does not represent any value of the type an invalid representation. When the result of an Unchecked_Conversion to a non-scalar type such as a record does not represent a value of the type, the effect is implementation-defined and the result can be abnormal¹⁰. Using an abnormal object makes execution erroneous. The data validity rules define what happens when the result of a conversion to a scalar type is invalid¹¹. The 'Valid attribute exists to check whether data produced by a conversion or similar means is a valid value¹². In the example above, H.Format'Valid was false and the program printed “invalid value”.

The behavior of this example is still well defined because GNAT defines Unchecked_Conversion between types of the same size as a bit-for-bit copy¹³. Each component of the record is a copy of the bits in the byte sequence, and only the Format component becomes invalid. That is why you can read Block_Id and the others and then check Format with 'Valid. This is implementation-defined behavior, and other compilers may not behave the same way.

flowchart TB
        accTitle: Checking a converted value with Valid before use
        accDescr: Shows that the format of a header produced by Unchecked_Conversion is checked with the Valid attribute before use, and the packet is discarded if the result is false.
        A["Build the header with Unchecked_Conversion"] --> B{"Is Format'Valid true?"}
        B -->|"True"| C["Handle according to the format"]
        B -->|"False"| D["Discard the packet"]

Figure 6: Check an enumeration value produced by conversion with Valid before using it.

If you forget to call 'Valid, the compiler gives neither an error nor a warning. The more fields there are to check, the easier it is to forget.

The extended ID changes the form of the header itself

When the extended-ID flag is set, the header becomes 20 bytes and the block ID and packet ID move. Which type to read with cannot be decided until the flag in the byte at offset 4 has been read. In the end, you read one byte before overlaying the type anyway.

Checking the length before reading the byte sequence

To avoid the pitfalls, check the packet length and then read the necessary bytes one at a time to assemble the values. The received byte array and the functions that read from it are declared as follows.

   --  Use a value larger than the maximum UDP payload length as the index bound.
   subtype Packet_Index is Natural range 0 .. 65_535;
   type Byte_Array is array (Packet_Index range <>) of Unsigned_8;

The header type that holds the values read, the format, the result and the length constants are declared as follows. The header type has no representation clause and is kept separate from the byte layout.

   type Packet_Format is
     (Leader, Trailer, Payload, All_In, H264, Multi_Zone, Multi_Part, Gen_DC);

   type Parse_Result is (Ok, Too_Short, Unknown_Format, Not_Leader, Not_Image);

   Standard_Header_Length : constant := 8;
   Extended_Header_Length : constant := 20;
   Image_Leader_Length    : constant := 36;

   type Gvsp_Header is record
      Status_Code : Unsigned_16   := 0;
      Flags       : Unsigned_16   := 0;  --  Extended ID only
      Extended_Id : Boolean       := False;
      Format      : Packet_Format := Leader;
      Block_Id    : Unsigned_64   := 0;
      Packet_Id   : Unsigned_32   := 0;
      Data_Offset : Natural       := 0;  --  Start of the data (from the start of the packet)
   end record;

   function Read_U16 (P : Byte_Array; Offset : Natural) return Unsigned_16
   with Pre => P'Length >= 2 and then Offset <= P'Length - 2;

   function Read_U32 (P : Byte_Array; Offset : Natural) return Unsigned_32
   with Pre => P'Length >= 4 and then Offset <= P'Length - 4;

   function Read_U64 (P : Byte_Array; Offset : Natural) return Unsigned_64
   with Pre => P'Length >= 8 and then Offset <= P'Length - 8;

   procedure Parse_Header
     (Packet : Byte_Array;
      Header : out Gvsp_Header;
      Result : out Parse_Result)
   with
     Post =>
       (if Result = Ok then
          Header.Data_Offset in Standard_Header_Length | Extended_Header_Length
          and then Header.Data_Offset <= Packet'Length);

Three design decisions were made.

• The index bound is 65535, which makes it easy to prove that index arithmetic cannot overflow.
• The reading functions take an offset from the start of the packet (Offset) and read from P'First + Offset. This also works for arrays whose first index is not 0, such as a slice cut out of a receive buffer.
• The precondition (Pre) of Read_U16 is “the offset allows 2 bytes to be read”. The caller must first write a length check that establishes this condition.

flowchart TB
        accTitle: Precondition of Read_U16 and the array range
        accDescr: Shows that if the precondition of Read_U16, Offset at most P'Length - 2, holds, then both indices read, P'First + Offset and P'First + Offset + 1, lie within the array range.
        A["Precondition: Offset ≤ P'Length − 2"] --> B["P'First + Offset is in range"]
        A --> C["P'First + Offset + 1 is in range"]
        B --> D["2 bytes read with no out-of-range access"]
        C --> D

Figure 7: When the precondition holds, both indices Read_U16 reads lie within the array range.

The bodies of the reading functions and of the procedure that reads the header are as follows. The procedure always checks the length before calling a reading function.

   function Read_U16 (P : Byte_Array; Offset : Natural) return Unsigned_16 is
     (Shift_Left (Unsigned_16 (P (P'First + Offset)), 8)
      or Unsigned_16 (P (P'First + Offset + 1)));

   function Read_U32 (P : Byte_Array; Offset : Natural) return Unsigned_32 is
     (Shift_Left (Unsigned_32 (P (P'First + Offset)), 24)
      or Shift_Left (Unsigned_32 (P (P'First + Offset + 1)), 16)
      or Shift_Left (Unsigned_32 (P (P'First + Offset + 2)), 8)
      or Unsigned_32 (P (P'First + Offset + 3)));

   function Read_U64 (P : Byte_Array; Offset : Natural) return Unsigned_64 is
     (Shift_Left (Unsigned_64 (Read_U32 (P, Offset)), 32)
      or Unsigned_64 (Read_U32 (P, Offset + 4)));

   procedure Parse_Header
     (Packet : Byte_Array;
      Header : out Gvsp_Header;
      Result : out Parse_Result)
   is
      Format_Byte : Unsigned_8;
      Format_Code : Unsigned_8;
   begin
      Header := (others => <>);

      if Packet'Length < Standard_Header_Length then
         Result := Too_Short;
         return;
      end if;

      Header.Status_Code := Read_U16 (Packet, 0);
      Format_Byte        := Packet (Packet'First + 4);
      Header.Extended_Id := (Format_Byte and 16#80#) /= 0;
      Format_Code        := Format_Byte and 16#7F#;

      if Format_Code not in 1 .. 8 then
         Result := Unknown_Format;
         return;
      end if;
      Header.Format := Packet_Format'Val (Format_Code - 1);

      if Header.Extended_Id then
         if Packet'Length < Extended_Header_Length then
            Result := Too_Short;
            return;
         end if;
         Header.Flags       := Read_U16 (Packet, 2);
         Header.Block_Id    := Read_U64 (Packet, 8);
         Header.Packet_Id   := Read_U32 (Packet, 16);
         Header.Data_Offset := Extended_Header_Length;
      else
         Header.Block_Id    := Unsigned_64 (Read_U16 (Packet, 2));
         Header.Packet_Id   := Read_U32 (Packet, 4) and 16#00FF_FFFF#;
         Header.Data_Offset := Standard_Header_Length;
      end if;

      Result := Ok;
   end Parse_Header;

The format value is converted to the enumeration only after checking that it lies in 1–8, so no invalid enumeration value is ever created. The byte order is assembled with shifts, so it depends neither on Scalar_Storage_Order nor on the CPU’s endianness.

flowchart TB
        accTitle: Order of decisions in Parse_Header
        accDescr: Shows that Parse_Header checks in turn whether the packet is at least 8 bytes, whether the format is 1 to 8, and, for an extended ID, whether it is at least 20 bytes; it returns Too_Short or Unknown_Format if a condition fails, and otherwise reads the header and returns Ok.
        A["Receive a packet"] --> B{"At least 8 bytes?"}
        B -->|"No"| X["Too_Short"]
        B -->|"Yes"| C{"Format is 1–8?"}
        C -->|"No"| Y["Unknown_Format"]
        C -->|"Yes"| D{"Extended ID?"}
        D -->|"Yes"| E{"At least 20 bytes?"}
        E -->|"No"| X
        E -->|"Yes"| F["Read 64-bit IDs and return Ok"]
        D -->|"No"| G["Read 16-bit and 24-bit IDs and return Ok"]

Figure 8: Parse_Header checks the length and format before reading the IDs.

Parse_Image_Leader, which reads an image leader, has the same shape: it checks that the data part is 36 bytes long before reading each field. Like Wireshark and Aravis, it masks the Payload Type with 16#3FFF# before comparing it with image (1). This mask also clears the 0x8000 bit (the start of device-specific values in Wireshark), so 0x8001 also passes as an image. To tell them apart, mask with 16#BFFF#, which clears only the chunk bit⁴⁵.

The two approaches compare as follows.

According to the SPARK User’s Guide, overlays of the form with Address => Y'Address and Unchecked_Conversion are also within the scope of analysis. SPARK, however, requires every value that is read to be valid, and treats 'Valid as always returning true. An object that may hold invalid values must be marked Potentially_Invalid, with its validity written in contracts¹⁴. Of the values the 7-bit Format field can hold, only 8 are valid, so the overlay approach cannot be proved with SPARK as it stands. In this article, the overlay approach was not run through GNATprove.

flowchart TB
        accTitle: What is needed to handle the overlay approach in SPARK
        accDescr: Shows that reading by overlaying a type lets Format hold invalid values, but SPARK requires values read to be valid and treats Valid as always true, so Potentially_Invalid and validity contracts are needed.
        A["Read by overlaying a type"] --> B["Format may hold invalid values"]
        B --> C["SPARK requires values read to be valid"]
        C --> D["Valid is treated as always true"]
        D --> E["Potentially_Invalid and contracts are needed"]

Figure 9: To handle the overlay approach in SPARK, the possibility of invalid values must be stated with Potentially_Invalid and contracts.

Proving with SPARK that nothing is read out of range

The reading functions and the header procedure are written in a package with SPARK_Mode. For code in this scope, GNATprove verifies, for all inputs, the array index checks, absence of integer overflow, the range of 'Val, the precondition at every call, and the postcondition¹⁵. A proof of the absence of run-time errors (AoRTE) corresponds to the Silver level of SPARK¹⁶.

flowchart TB
        accTitle: What GNATprove checks
        accDescr: Shows that for code in SPARK_Mode, GNATprove checks index ranges, integer overflow, conversions to enumerations, call preconditions and postconditions for all inputs, and reports checks it cannot prove.
        A["SPARK_Mode code and contracts"] --> B["GNATprove"]
        B --> C["Indices in range?"]
        B --> D["No overflow?"]
        B --> E["Val in enum range?"]
        B --> F["Pre/postconditions"]
        C --> G["Reports results"]
        D --> G
        E --> G
        F --> G

Figure 10: GNATprove checks run-time checks and contracts for all inputs.

The proof was run with the following command. -u gvsp.adb restricts the analysis to this package, and --checks-as-errors=on makes the run fail if any check cannot be proved¹⁷.

gnatprove -P gvsp.gpr -u gvsp.adb --level=2 --report=all --checks-as-errors=on -j0

The last line of GNATprove’s output was the following: all 66 checks were proved.

Success: all checks proved (66 checks).

The --report=all output lists precondition proved for each call to Read_U16 and the other functions, and index check proved for each index inside the reading functions. The postcondition of Parse_Header was also reported as postcondition proved.

Removing one length check breaks the proof

To confirm that the proof means something, I also prepared code with only the extended-ID length check removed.

      if Header.Extended_Id then
         Header.Flags       := Read_U16 (Packet, 2);
         Header.Block_Id    := Read_U64 (Packet, 8);
         Header.Packet_Id   := Read_U32 (Packet, 16);
         Header.Data_Offset := Extended_Header_Length;

For this code GNATprove reported 3 checks it could not prove, and because of --checks-as-errors=on the run ended as a failure. The first was the call to Read_U64 (Packet, 8).

 medium: precondition might fail, cannot prove Offset <= P'Length - 8
--> gvsp.adb:45:32
   45 |             Header.Block_Id    := Read_U64 (Packet, 8);

The other two were the precondition of Read_U32 (Packet, 16) on the next line (Offset <= P'Length - 4) and the postcondition of Parse_Header, Header.Data_Offset <= Packet'Length. This is because, for an extended-ID packet of 8–15 bytes, none of the three holds, and for 16–19 bytes, the last two do not. Every report carried the note “provers reached time limit before completing the proof”, and no counterexample was given. They report that the proof could not be completed within the time limit.

When the same code was linked into the test program and run locally, it stopped at the 12-byte extended-ID packet. In a build with assertions enabled (-gnata) the exception came from the precondition of Read_U64; in a build with assertions disabled it came from the index check inside the function.

raised ADA.ASSERTIONS.ASSERTION_ERROR : failed precondition from gvsp.ads:47

raised CONSTRAINT_ERROR : gvsp.adb:8 index check failed

flowchart TB
        accTitle: Where a missing length check is found
        accDescr: Shows that code with the extended-ID length check removed is reported by GNATprove before execution as a failing precondition, and is found by tests as an exception when a 12-byte extended-ID packet is passed.
        A["Code with the length check removed"] --> B["GNATprove reports it before execution"]
        A --> C["Tests raise an exception at 12 bytes"]

Figure 11: A missing length check is found before execution by proof, and by tests only when that input is passed.

To find it by testing, you need a packet of exactly that length. GNATprove reports the missing check for all lengths without your having to prepare such inputs.

What the proof guarantees is only that nothing is read out of range and that the properties in the contracts hold. Whether the field offsets match real GVSP is outside the proof. In this article the offsets were cross-checked against the Wireshark and Aravis sources, and the values were checked by the tests below.

Running it on hand-built packets

For the tests, I assembled the following packets by hand and passed them to Parse_Header, also calling Parse_Image_Leader for leaders.

• A 44-byte standard-ID leader (width 640, height 480; the pixel format is 0x01080001, which Aravis defines as Mono8¹⁸)
• The same leader cut to 5 bytes and to 30 bytes
• A 24-byte extended-ID payload (4 bytes of data), and the same cut to 12 bytes
• An 8-byte packet whose format byte is 0x09

standard leader : 44 bytes, header OK, LEADER, block 42, packet 0, data 36, leader OK, 640 x 480
cut to 5 bytes  : 5 bytes, header TOO_SHORT
cut to 30 bytes : 30 bytes, header OK, LEADER, block 42, packet 0, data 22, leader TOO_SHORT
extended payload: 24 bytes, header OK, PAYLOAD, block 4294967296, packet 5, data 4
extended, 12 b  : 12 bytes, header TOO_SHORT
unknown format  : 8 bytes, header UNKNOWN_FORMAT

For the leader cut to 30 bytes, the header could be read, but the leader data part was too short, so the result was TOO_SHORT. For the extended-ID payload, the 64-bit block ID (0x0000_0001_0000_0000) and the 32-bit packet ID were read.

Next, I fed it one million packets of random content with lengths of 0–64 bytes. To make the format byte fall in 1–8 more often, half of them had that value biased toward 0–8. In a build with assertions and run-time checks enabled, not a single exception was raised. The breakdown of results was:

OK: 361063
TOO_SHORT: 159338
UNKNOWN_FORMAT: 460233
NOT_LEADER: 0
NOT_IMAGE: 19366

NOT_LEADER is 0 because the test calls Parse_Image_Leader only for leaders. NOT_IMAGE counts leaders whose header and data part were long enough but whose Payload Type was not an image. A test on random input can only say that no exception occurs for the inputs tried. The guarantee for all inputs comes from the proof in the previous section.

flowchart TB
        accTitle: Division of roles between tests and proof
        accDescr: Shows that tests with hand-built packets check field values, tests with random packets check that no exception occurs for the inputs tried, and GNATprove checks that nothing is read out of range for all inputs.
        A["Hand-built packets"] --> D["Are the field values correct?"]
        B["One million random packets"] --> E["No exception for the inputs tried?"]
        C["GNATprove"] --> F["Nothing read out of range for any input?"]

Figure 12: Correct values are checked by tests, and the absence of out-of-range reads by proof.

Where the parser fits in the receive path

In a real receive path, you slice only the received length out of the buffer filled by the socket and pass it to Parse_Header. Because Packet_Index is a 0-based index, it can be sliced as Buffer (0 .. Received - 1). Even if the received length is 0, it can be passed as an empty array. This, however, is how to write it when the receive buffer is held as a Byte_Array. Receive_Socket in GNAT.Sockets writes into an Ada.Streams.Stream_Element_Array, and that array cannot be type-converted to Byte_Array (GNAT 13.3.0 gives the error “incompatible component types for array conversion”). In that case, add one step, such as copying into a Byte_Array or writing a binding that calls the OS recv directly. After that the flow branches by format. For a leader, Parse_Image_Leader gives the image size so a buffer can be prepared; for a payload, the data is copied to the position given by the packet ID. The trailer signals the end of the image.

flowchart TB
        accTitle: Where the parser sits in the receive path
        accDescr: Shows that the received length is sliced out of the buffer filled by the socket and passed to Parse_Header; a leader goes to Parse_Image_Leader to learn the image size, a payload's data is copied, a trailer completes the image, and failed results discard and count the packet.
        A["Receive on socket"] --> B["Slice received length"]
        B --> C["Parse_Header"]
        C -->|"Leader"| D["Get size (Parse_Image_Leader)"]
        C -->|"Payload"| E["Copy by packet ID"]
        C -->|"Trailer"| F["Complete the image"]
        C -->|"Not Ok"| G["Discard and count"]

Figure 13: Place the parser right after reception, and discard and count packets that fail.

If results other than Ok are counted instead of raised as exceptions, you can later see how many short packets or unexpected formats are arriving.

This article does not build the receive loop, resend requests for missing packets, or image assembly. How missing packets lead to dropped frames, and how to investigate them, is covered in Dropped Frames with GigE Vision and USB3 Vision Cameras, and how to build tasks that separate reception from processing is covered in Frame Acquisition Without Drops Using Ada Tasks. The basics of SPARK contracts and proof are explained in detail in Introduction to Formal Verification with SPARK.

Test environment and what was not verified

• Local build and run: Ubuntu 24.04, GNAT 13.3.0 (Ubuntu package), gprbuild. The CPU is x86-64.
• CI build, run and proof: a GitHub Actions ubuntu-24.04 runner with GNAT 16.1.0 (gnat_native) and GNATprove FSF 16.1.0 installed through Alire 2.1.1. The provers GNATprove used were Alt-Ergo 2.6.1, cvc5 1.3.2 and Z3 4.15.4. The output of the programs run was the same as locally.
• Not tried with a real GigE Vision camera, reception over a network, or on Windows.
• The GigE Vision specification was not consulted. The field layout is what could be confirmed in the Wireshark and Aravis sources. The contents of formats not read in this article, such as chunk, multi-part and GenDC, are not covered.
• The overlay-by-address approach was only compiled to confirm the warning; it was not run and compared.
• The project used for verification is not published; the code in this article is an excerpt from it.

Related Articles

This article is part of the series “Ada and Machine Vision”. The other articles in the series:

• Proving Image Processing Free of Out-of-Bounds Access with SPARK — Binarization, Smoothing, Labeling and a Speed Comparison with C
• Frame Acquisition Without Drops Using Ada Tasks — A Protected-Object Ring Buffer and Priorities
• Calling Ada Inspection Logic from a C# Inspection App — Passing Image Buffers Without Copying and Guarding the Boundary
• Separating Pixels and Millimeters with Types — Preventing Unit Mix-ups in Dimensional Inspection with Ada

Related existing articles:

• Dropped Frames with GigE Vision and USB3 Vision Cameras — Locating the Cause and the Windows Settings to Review
• Proving AI-Written Code with SPARK ── Humans Write the Contracts, GNATprove Checks Them
• Connecting Ada with C and C# — Building a DLL and Calling It

References

Related Articles

Recent articles sharing the same tags. Deepen your understanding with closely related topics.

Related Topics

These are topic pages close to this theme. Starting from the article, you can go on to related services and other articles.

Services Connected to This Topic

This article leads to the following service pages. Start from the entry point closest to your situation.

Frequently Asked Questions

Questions commonly asked at the time of consultation about the topic of this article.

Can I read a GVSP header by overlaying a type written with an Ada representation clause on the byte sequence?

Not for byte sequences that arrive from the network. A short packet does not fill the size of the type, and an unexpected value in the format byte leaves the enumeration with an invalid value. The extended-ID flag also changes the length of the header. Check the length first and read one field at a time; keep the representation-clause type for documenting the layout, or for use after the checks.

If I add Bit_Order => High_Order_First, can I read big-endian values directly?

No. Bit_Order decides how bit numbers in the representation clause are counted; it does not change the byte order of multi-byte integers. In this article's example, on x86-64 a type with only Bit_Order read 42 as 10752. To change the byte order as well, add Scalar_Storage_Order, an attribute specific to GNAT.

What does a SPARK proof guarantee?

That for any byte sequence satisfying the precondition, the code does not read outside the array, integers do not overflow, and conversions to the enumeration stay in range. The properties written in the postcondition also hold. Whether the field offsets match the specification is outside the proof, so they are checked against the sources and by tests.

Author Profile

Profile page for the article author.

Go Komura

Representative of KomuraSoft LLC

Focused on Windows software development, technical consulting, and bug investigation, with particular strength in projects where existing assets remain and in investigating failures whose cause is hard to see.