Calling Ada Inspection Logic from a C# Inspection App — Passing Image Buffers Without Copying and Guarding the Boundary

Sometimes you want to keep the screens, settings and camera control of an inspection system in C# and WPF, and write only the pass/fail logic in Ada. The decision logic may be small, but it is the part where mistakes are not acceptable, so the idea is to protect just that part with Ada’s types and SPARK proofs and leave everything else in familiar .NET. The hard part is the boundary between C# and Ada. You do not want to copy a multi-megabyte image on every call, and if the dimensions C# passes disagree with the actual length of the buffer, the Ada side ends up reading memory outside it.

The answer comes down to four points. Pass the image as a pointer to its first byte, the buffer length, and the width, height and stride (the number of bytes per row); on the Ada side, check that the dimensions fit within that length, then view the same memory as a two-dimensional array. Return the result as a struct, and compare its size on both the C# and Ada sides before using it. Ada functions called directly from C# never let exceptions escape; they turn them into error codes. Keep the decision logic itself within SPARK and use GNATprove to prove that it has no out-of-bounds reads and no overflow.

General topics such as building the DLL, initialization and passing strings were covered in “Connecting Ada with C and C#”. This article continues from there and focuses on designing the boundary that carries image buffers and inspection results.

Every example was actually built and run. On Linux (Ubuntu 24.04, GNAT 13.3.0) I built a shared library and called it from a C test driver; on a GitHub Actions Windows runner I built the DLL and called it from a .NET 10 console app. The proofs were done with GNATprove on a GitHub Actions Linux runner. The WPF example was only built; its window was never run. Calling the library from a .NET app on Linux is out of scope because its signal handling conflicts with .NET, and on .NET on Linux I ran only the tests that confirm why it is excluded. The reasons are given in the last section.

Which part of the inspection app to write in Ada

Think of the inspection app as split into the screens, image capture from the camera, the decision, and saving results. In this article only the decision moves to Ada. The screens, capture and saving stay in WPF and C#, and a thin C# layer passes the image buffer to the Ada DLL.

The Ada DLL is also split in two. The functions that C# calls directly (called boundary functions below) receive a pointer and dimensions, check them, and pass the memory to the decision function as an Ada array. Because the decision function receives only Ada arrays, it can be proved with SPARK. The part that treats a pointer as an array stays outside SPARK; to compensate, it is kept short and verified by human review.

flowchart TB
        accTitle: Structure of the inspection app
        accDescr: The WPF screens and capture call the boundary function in the Ada DLL through a thin C# layer; the boundary function checks the pointer and dimensions, calls the decision function proved with SPARK, and returns the result and an error code.
        A["WPF screens and capture (C#)"] --> B["Thin C# layer (pins and calls)"]
        B --> C["Boundary function (Ada)"]
        C --> D["Decision function (SPARK)"]
        D --> C
        C -->|"Result and error code"| B
        E["Check pointer and dimensions"] -.-> C
        F["Prove no out-of-bounds reads"] -.-> D

Figure 1: Only the decision goes into the Ada DLL, and the DLL is split into the boundary function and a decision function proved with SPARK.

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 (18 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

Defining the exported functions as C declarations

C# and Ada cannot talk to each other directly, so the C ABI (the rules for how functions are called and how structs are laid out) sits between them. The first step is therefore to write the exported functions as C declarations and match the types on both sides to them.

typedef struct { int threshold; int max_defect_pixels; } inspect_params;
typedef struct {
    int64_t defect_pixels;
    int min_x, min_y, max_x, max_y;
    int verdict;
} inspect_result;

int inspect_dark_defects(const uint8_t *pixels, size_t length,
                         int width, int height, int stride,
                         const inspect_params *params, inspect_result *result);
int inspect_result_size(void);
int inspect_elaborated(void);

The example inspection works on 8-bit grayscale images and counts pixels darker than a threshold as defects. If the number of defect pixels exceeds a limit, the part fails, and the bounding box around the defects is returned as well. The inspection itself is deliberately simple, because what this article is about is not the inspection but how to pass the image and the result across the boundary.

The parameters were chosen on the following principles.

• Pass the buffer length (in bytes) in addition to the pointer to the first byte of the image. With the dimensions alone, the Ada side cannot check whether they fit in the buffer.
• Pass the number of bytes per row (the stride) separately from the width.
• The caller allocates and frees the memory. Ada reads it only during the call and does not keep the pointer.
• The return value is an error code, and the inspection result is written into a struct prepared by the caller.

There are six error codes.

flowchart TB
        accTitle: Who owns the image buffer
        accDescr: The caller prepares the image buffer and the result struct, Ada reads the buffer and writes the result only during the call, and after it returns the caller reuses or frees the buffer.
        A["Caller prepares buffer and result"] --> B["Call inspect_dark_defects"]
        B --> C["Ada reads only during the call"]
        C --> D["Ada returns result and error code"]
        D --> E["Caller reuses or frees"]

Figure 2: The caller is responsible for allocating and freeing the buffer, and Ada reads it only during the call.

Image buffer dimensions and stride

In an image buffer, the number of bytes per row is not necessarily the same as the width. Microsoft’s documentation also explains that an image in memory may have padding bytes after each row, in which case the stride is larger than the width¹. Two images with the same dimensions can have different strides depending on the buffer. The pixel in row y, column x is at byte y × stride + x from the start.

flowchart TB
        accTitle: Stride and padding
        accDescr: A row is stride bytes long; the first width bytes are pixels and the rest is padding, and the decision function reads only the pixel part of each row.
        A["One row (stride bytes)"] --> B["Pixels (width bytes)"]
        A --> C["Padding (stride − width)"]
        B --> D["Read by the decision function"]
        C -.->|"Not read"| D

Figure 3: Each row consists of pixels and padding, and the decision function reads only the pixels.

Before reading memory, the boundary function checks three things.

1. The pointers are not NULL.
2. The width and height are 1 or more, and the stride is at least the width.
3. Stride × height is no greater than the buffer length.

It also checks the ranges of parameters such as the threshold and returns error code 4 if they are out of range. That is explained in a later section.

The third condition requires that the last row also has stride bytes. If a buffer omits the padding only on its last row, the length needed is (height − 1) × stride + width. This example views the memory as an array shaped (height, stride), so it requires stride × height bytes. To also accept buffers without padding on the last row, change the shape of the array or read row by row.

The multiplication is done in 64-bit unsigned integers. The width, height and stride are C ints, so they are at most 2³¹ − 1. The product of two of them fits in 64 bits, so the multiplication itself cannot overflow.

Images with a negative stride are not accepted. According to Microsoft’s documentation, a bottom-up image, whose last row comes first in memory, has a negative stride¹. This example handles only top-down images, whose first row comes first in memory, and returns error code 2 at the second condition if the stride is negative.

flowchart TB
        accTitle: Order in which the boundary function checks dimensions
        accDescr: If a pointer is NULL it returns error code 1, if the width, height and stride are invalid it returns 2, if the product of stride and height exceeds the buffer length it returns 3, and only when all checks pass does it read the buffer as an array.
        A{"Is a pointer NULL?"} -->|"NULL"| B["Return 1"]
        A -->|"Not NULL"| C{"Are width, height and stride valid?"}
        C -->|"Invalid"| D["Return 2"]
        C -->|"Valid"| E{"stride × height ≤ length?"}
        E -->|"Exceeds"| F["Return 3"]
        E -->|"Fits"| G["Read as an array"]

Figure 4: The boundary function checks the three dimension conditions in order and reads memory only when all of them hold.

Viewing the received buffer as an Ada array

This is the specification (.ads) of the boundary functions. The records corresponding to the C structs get Convention => C, and the functions get Export and External_Name.

with Interfaces;
with Interfaces.C; use Interfaces.C;
with System;

package Inspect_API is

   --  struct inspect_params { int threshold; int max_defect_pixels; };
   type Inspect_Params is record
      Threshold         : int;  --  Pixels darker than this count as defects (0-255)
      Max_Defect_Pixels : int;  --  Fail if the number of defect pixels exceeds this (0 or more)
   end record
     with Convention => C;

   --  struct inspect_result { int64_t defect_pixels;
   --    int min_x, min_y, max_x, max_y; int verdict; };
   type Inspect_Result is record
      Defect_Pixels : Interfaces.Integer_64;
      Min_X, Min_Y  : int;  --  Bounding box of the defects; -1 if there are none
      Max_X, Max_Y  : int;
      Verdict       : int;  --  0 = pass, 1 = fail
   end record
     with Convention => C;

   type Params_Access is access constant Inspect_Params
     with Convention => C;
   type Result_Access is access all Inspect_Result
     with Convention => C;

   Status_OK               : constant int := 0;
   Status_Null_Pointer     : constant int := 1;
   Status_Bad_Geometry     : constant int := 2;
   Status_Buffer_Too_Small : constant int := 3;
   Status_Bad_Parameter    : constant int := 4;
   Status_Internal_Error   : constant int := 99;

   --  int inspect_dark_defects (const uint8_t *pixels, size_t length,
   --                            int width, int height, int stride,
   --                            const inspect_params *params,
   --                            inspect_result *result);
   function Inspect_Dark_Defects
     (Pixels : System.Address;
      Length : size_t;
      Width  : int;
      Height : int;
      Stride : int;
      Params : Params_Access;
      Result : Result_Access) return int
     with Export, Convention => C, External_Name => "inspect_dark_defects";

   --  int inspect_result_size (void);  Compared with the size of the caller's struct
   function Result_Size return int
     with Export, Convention => C, External_Name => "inspect_result_size";

   --  int inspect_elaborated (void);  1 once initialization has completed
   function Elaborated return int
     with Export, Convention => C, External_Name => "inspect_elaborated";

end Inspect_API;

The parameters and the result are received as access types. Annex B of the Ada Reference Manual specifies that both record-type parameters and in parameters of an access type are passed to a C function as t*². Writing Params : Inspect_Params or Result : out Inspect_Result would also look like a pointer from the C side, but then Ada has no way to check whether it is NULL. With an access type it can be compared with null, so if the C side passes NULL the function can return error code 1.

flowchart TB
        accTitle: How parameters are received and how NULL is checked
        accDescr: If a C pointer to const inspect_params is received in Ada as an in parameter of the record type, NULL cannot be checked; if it is received as an access type, it can be compared with null and error code 1 can be returned.
        A["C const inspect_params*"] --> B{"How Ada receives it"}
        B -->|"in parameter of record type"| C["NULL cannot be checked"]
        B -->|"Access type"| D["Can be compared with null"]
        D --> E["Return error code 1"]

Figure 5: Receiving parameters as access types lets Ada check for a NULL passed from the C side.

The body (.adb) is as follows.

with Inspect_Core;
with System; use type System.Address;

package body Inspect_API is

   use type Interfaces.Unsigned_64;
   use type Interfaces.Integer_64;

   Elaboration_Done : int := 0;  --  Set to 1 when the package body is elaborated

   function Inspect_Dark_Defects
     (Pixels : System.Address;
      Length : size_t;
      Width  : int;
      Height : int;
      Stride : int;
      Params : Params_Access;
      Result : Result_Access) return int
   is
   begin
      if Result = null then
         return Status_Null_Pointer;
      end if;

      --  Whatever path returns, leave the result the caller reads in a defined state
      Result.all :=
        (Defect_Pixels => 0, Min_X | Min_Y | Max_X | Max_Y => -1, Verdict => 1);

      if Pixels = System.Null_Address or else Params = null then
         return Status_Null_Pointer;
      end if;

      if Width <= 0 or else Height <= 0 or else Stride < Width then
         return Status_Bad_Geometry;
      end if;

      --  Require the last row to have stride bytes as well
      if Interfaces.Unsigned_64 (Stride) * Interfaces.Unsigned_64 (Height)
         > Interfaces.Unsigned_64 (Length)
      then
         return Status_Buffer_Too_Small;
      end if;

      --  Check parameter ranges with if instead of relying on exceptions
      if Params.Threshold not in 0 .. 255
        or else Params.Max_Defect_Pixels < 0
      then
         return Status_Bad_Parameter;
      end if;

      declare
         --  The ranges were checked above, so these conversions raise no exception
         Threshold   : constant Inspect_Core.Byte :=
           Inspect_Core.Byte (Params.Threshold);
         Max_Defects : constant Natural := Natural (Params.Max_Defect_Pixels);

         --  View the caller's buffer as a (row, column) array without copying
         Img : Inspect_Core.Image
                 (0 .. Natural (Height) - 1, 0 .. Natural (Stride) - 1)
           with Import, Address => Pixels;

         S : Inspect_Core.Summary;
      begin
         Inspect_Core.Count_Dark (Img, Positive (Width), Threshold, S);

         Result.all :=
           (Defect_Pixels => S.Defect_Pixels,
            Min_X         => int (S.Min_X),
            Min_Y         => int (S.Min_Y),
            Max_X         => int (S.Max_X),
            Max_Y         => int (S.Max_Y),
            Verdict       =>
              (if S.Defect_Pixels <= Interfaces.Integer_64 (Max_Defects)
               then 0 else 1));
         return Status_OK;
      end;
   exception
      when others =>
         --  An unexpected failure; the caller treats it as a reason to stop inspecting
         return Status_Internal_Error;
   end Inspect_Dark_Defects;

   function Result_Size return int is
     (int (Inspect_Result'Max_Size_In_Storage_Elements));

   function Elaborated return int is (Elaboration_Done);

begin
   Elaboration_Done := 1;
end Inspect_API;

The key to avoiding a copy is the declaration of Img. Address => Pixels places the array at the same address as the caller’s buffer. A variable with Import is not initialized³, so merely declaring it does not overwrite the caller’s pixels. The index ranges are fixed only after the dimensions have been checked, so Img never extends beyond the buffer.

Passing Img to the decision function does not copy it either. The Reference Manual leaves it to the implementation whether a parameter of this array type is passed by copy or by reference⁴. With GNAT 13.3.0 on my machine, I confirmed that the caller’s buffer and the array received by the procedure have the same address.

It is also worth checking how a two-dimensional array is laid out in memory. The Reference Manual advises implementations to store multidimensional arrays in row-major order by default (Implementation Advice). Only types with Convention => Fortran are column-major⁵. GNAT uses row-major order, so Img (Y, X) refers to the pixel at byte Y × stride + X from the start. This is also confirmed by the test shown later, in which the defect positions in a padded image come out correctly.

flowchart TB
        accTitle: Viewing the same memory as an Ada array
        accDescr: The boundary function receives the address of the first byte of a pinned C# byte array, checks the dimensions and then overlays the two-dimensional Ada array Img on it, so the pixels are not copied and the rows and columns of Img correspond to the pixel in row y and column x.
        A["C# byte array"] -->|"Address of pinned first byte"| B["Boundary function"]
        B -->|"Check dimensions, then overlay"| C["Ada array Img (row, column)"]
        C --> D["Img (y, x) is byte y × stride + x"]
        A -.->|"Same memory, no copy"| C

Figure 6: The boundary function checks the dimensions and then views the same memory as the C# array as a two-dimensional Ada array.

Threshold and Max_Defects are made by converting C ints to range-constrained Ada types. Inspect_Core.Byte is a type from 0 to 255, so passing 300 as the threshold would raise Constraint_Error in the conversion. The function therefore checks the range with if before converting and returns error code 4 if it is out of range. You could instead let Ada’s range checks fire and turn the exception into an error code, but this example does not do that. The reason is given in the section “Stopping exceptions in the boundary function and turning them into error codes”.

Proving the decision logic with SPARK

The decision function lives in a separate package, Inspect_Core. This package has SPARK_Mode and is proved with GNATprove.

with Interfaces; use type Interfaces.Integer_64;

package Inspect_Core with SPARK_Mode is

   type Byte is mod 2 ** 8;

   --  Cap the index at Natural'Last - 1 so that 'Length fits in Integer
   subtype Index is Natural range 0 .. Natural'Last - 1;

   --  The first index is the row (y), the second the column (x); the second length is the stride
   type Image is array (Index range <>, Index range <>) of Byte;

   type Summary is record
      Defect_Pixels : Interfaces.Integer_64;
      Min_X, Min_Y  : Integer;   --  Bounding box of the defects; -1 if there are none
      Max_X, Max_Y  : Integer;
   end record;

   --  Look only at the first Width pixels of each row and count those darker than Threshold
   procedure Count_Dark
     (Img       : Image;
      Width     : Positive;
      Threshold : Byte;
      S         : out Summary)
   with
     Pre  => Img'Length (1) >= 1 and then Width <= Img'Length (2),
     Post => S.Defect_Pixels >= 0;

end Inspect_Core;

package body Inspect_Core with SPARK_Mode is

   procedure Count_Dark
     (Img       : Image;
      Width     : Positive;
      Threshold : Byte;
      S         : out Summary)
   is
      X_First : constant Natural := Img'First (2);
      X_Last  : constant Natural := Img'First (2) + (Width - 1);
      Total   : Interfaces.Integer_64 := 0;
      Row     : Natural;
   begin
      S := (Defect_Pixels => 0, Min_X | Min_Y | Max_X | Max_Y => -1);

      for Y in Img'Range (1) loop
         Row := 0;
         for X in X_First .. X_Last loop
            if Img (Y, X) < Threshold then
               Row := Row + 1;
               declare
                  DX : constant Natural := X - X_First;
                  DY : constant Natural := Y - Img'First (1);
               begin
                  if S.Min_X < 0 then
                     S.Min_X := DX;
                     S.Min_Y := DY;
                     S.Max_X := DX;
                     S.Max_Y := DY;
                  else
                     S.Min_X := Integer'Min (S.Min_X, DX);
                     S.Max_X := Integer'Max (S.Max_X, DX);
                     S.Max_Y := Integer'Max (S.Max_Y, DY);
                  end if;
               end;
            end if;
            pragma Loop_Invariant (Row <= X - X_First + 1);
         end loop;

         Total := Total + Interfaces.Integer_64 (Row);
         pragma Loop_Invariant
           (Total >= 0
            and then Total <=
              (Interfaces.Integer_64 (Y) - Interfaces.Integer_64 (Img'First (1)) + 1)
              * Interfaces.Integer_64 (Natural'Last));
      end loop;

      S.Defect_Pixels := Total;
   end Count_Dark;

end Inspect_Core;

The precondition (Pre) only requires at least one row and a Width no greater than the number of columns (the stride). When both hold, X_First .. X_Last always stays within the column index range, and Img (Y, X) never reads out of bounds. The boundary function calls it only after checking that the height is at least 1 and the stride is at least the width, so the precondition is met.

The index type is capped at Natural'Last - 1 to keep 'Length within Integer. If the index stayed Natural, the length of an array indexed 0 .. Natural'Last would exceed Integer'Last by one. When I first wrote it that way, GNATprove could not prove the range check on Img'Length (2) in the precondition.

The counting variables are structured so that the absence of overflow is easy to prove. The per-row count Row is a Natural, and a loop invariant states that it is at most the number of pixels seen so far. The count for the whole image, Total, is a 64-bit integer, and its invariant states that it is at most the number of finished rows × Natural'Last. Since this only multiplies the row count by a constant, the proof needs no nonlinear reasoning about products of variables.

flowchart TB
        accTitle: How the variables counting defect pixels are split
        accDescr: Within a row, Row is kept at most the number of pixels seen; each time a row is finished Row is added to the 64-bit Total, and Total is kept at most the product of the number of finished rows and Natural'Last, so it can be proved that neither overflows.
        A["Set Row to 0 at the start of a row"] --> B["Add 1 to Row for a dark pixel"]
        B --> C["Row ≤ pixels seen"]
        C --> D["Add to Total at the end of the row"]
        D --> E["Total ≤ rows × Natural'Last"]
        E -->|"Next row"| A

Figure 7: Keep the per-row count and the overall count separate, and give each a loop invariant that bounds it.

On a GitHub Actions Linux runner I ran GNATprove (FSF 16.1.0), installed through Alire, with --level=2. All 20 checks in scope were proved, and none were left unproved. They break down into 2 variable initializations, 13 run-time checks such as index, overflow and range checks, 4 for the initialization and preservation of the two loop invariants, and 1 postcondition.

gnatprove -P inspect.gpr --level=2 --report=all --checks-as-errors=on -j0

--checks-as-errors=on is the switch that treats unproved checks as errors⁶. Used in CI, it makes the job fail when a proof breaks.

What the proof guarantees is that, as long as the precondition holds, the decision function neither reads out of bounds nor overflows. The boundary function is outside SPARK, so whether it overlays Img with the right size and calls the decision function only after meeting the precondition is not proved. That part is kept short and checked by tests and review. Nor can the Ada side check that the length C# passes matches the real length of the buffer. That length is passed by the C# layer described in a later section, taken from the length of a Span.

flowchart TB
        accTitle: What is proved and what people check
        accDescr: That C# passes the correct length and that the boundary function checks the dimensions and overlays the array are checked by tests and review; under the precondition that results from them, GNATprove proves that the decision function has no out-of-bounds reads and no overflow.
        A["C# passes the correct length"] --> B["Boundary function checks and overlays"]
        B --> C["Precondition holds"]
        C --> D["Decision function (proved by GNATprove)"]
        D --> E["No out-of-bounds reads or overflow"]
        F["Checked by tests and review"] -.-> A
        F -.-> B

Figure 8: GNATprove proves the decision function, and its assumptions are the responsibility of the boundary function and the C# layer.

How to proceed with SPARK proofs, and whether to suppress run-time checks once the code is proved, are covered in “Proving Image Processing Free of Out-of-Bounds Access with SPARK”.

Stopping exceptions in the boundary function and turning them into error codes

Ada exceptions must not be allowed to reach C#. In the Linux experiments in the article “Connecting Ada with C and C#”, an unhandled Ada exception terminated the process⁷. The .NET documentation also says that exceptions from unmanaged code can be handled only on Windows, and that on other platforms they can cause unpredictable behavior or crashes⁸.

The boundary function therefore ends with a when others handler that turns any exception into error code 99. Out-of-range parameters are checked with the if statements from the previous section and return error code 4, so no exception occurs for either a correct call or a call with wrong values.

Exceptions are not used to report ordinary errors because, when the function is called from several threads at once, the threads may contend for a runtime variable. This library has no Ada tasks, so the GNAT runtime keeps the information about the exception being handled and the position of the secondary stack (an area used, for example, when a function returns a value whose size is not known in advance) together in a single variable, NT_TSD⁹. When the function is called with Task.Run, as in the WPF example, several threads may enter the boundary function at the same time. If an exception is raised or the secondary stack is used then, they contend for this variable. Checking with if keeps the exception from being raised at all.

For the secondary stack, adding pragma Restrictions (No_Secondary_Stack); to the library makes the compiler reject any code that uses it. With GNAT 13.3.0 on my machine, this article’s library still built unchanged with the restriction, and the results of the C test driver did not change. When I added a function that concatenates strings as a test, it was rejected with violation of restriction "No_Secondary_Stack". The restriction goes in the file read through Global_Configuration_Pragmas in the Builder package of the project file¹⁰. I have not, however, tested calls from several threads at once. If you do not need simultaneous calls, you can also serialize the calls on the C# side (wrap them in a lock).

flowchart TB
        accTitle: The shared variable when called from several threads
        accDescr: In a library without tasks, the exception information and the secondary stack position are in a single variable, NT_TSD, and threads contend for it if they raise exceptions or use the secondary stack at the same time, so exceptions are avoided with if checks and the secondary stack is avoided with No_Secondary_Stack.
        A["Several threads enter the boundary function"] --> B["Exception info and secondary stack position"]
        B --> C["Share a single variable, NT_TSD"]
        C --> D["Contention when used at once"]
        E["Check with if and raise no exception"] -.-> D
        F["Avoid it with No_Secondary_Stack"] -.-> D

Figure 9: A library without tasks shares the exception and secondary-stack information in one variable, so the code is written to use neither.

99 means “an unexpected failure”. The proof of the decision function assumes that the pointer and length C# passes are correct. If the caller passes a length longer than the real one, Ada reads memory outside the image. If it hits an address that cannot be read, then on Linux the GNAT runtime turns the SIGSEGV signal into an exception, as described in a later section, and 99 is returned. In a test where a C program on Linux passed the unreadable address 0x1000 with a length matching the dimensions, 99 was returned. In tests that passed the same values from .NET on GitHub Actions Linux and Windows runners, 99 was returned as well. If the address happens to be readable, nothing is detected and a wrong verdict is returned as is.

So when 99 is returned, discard the result for that image, stop inspecting, write a log entry and restart the app.

flowchart TB
        accTitle: Handling errors and exceptions in the boundary function
        accDescr: If a parameter is out of range it is checked with if and error code 4 is returned, every unexpected exception is turned into 99, and when 99 is returned the caller stops inspecting.
        A["Boundary function"] --> B{"Are parameters in range?"}
        B -->|"Out of range"| C["Return 4 (checked with if)"]
        B -->|"In range"| D["Decide and return 0"]
        D -.->|"Unexpected exception"| E["Return 99"]
        E --> F["Caller stops inspecting"]

Figure 10: Parameter errors become 4 through if checks, and only unexpected exceptions become 99.

Here are the results of calling the shared library from the C test driver on Linux. The calls that passed 300 as the threshold and −1 as the limit returned error code 4 from the if checks. Whichever way the function returns, the result struct has already been set to defined values (0 defects, bounding box −1) at the start of the boundary function.

elaborated=1 result size: C=32 Ada=32
ng (max 50)        status=0 defects=100 bbox=(100,50)-(109,59) verdict=1
ok (max 200)       status=0 defects=100 bbox=(100,50)-(109,59) verdict=0
padded stride      status=0 defects=100 bbox=(100,50)-(109,59) verdict=0
buffer too small   status=3 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
width > stride     status=2 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
threshold 300      status=4 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
max -1             status=4 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
null pixels        status=1 defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
ALL PASSED

The test image is 640 × 480 with a background of brightness 200 and a 10 × 10 square of brightness 20 at (100, 50). The threshold is 64. padded stride is an image with a stride of 644 whose last 4 bytes of padding in each row are 0 (dark). If the decision function read the padding too, the defects would grow by 4 × 480 pixels, but the result was 100 pixels, and the bounding box matched the position of the square.

flowchart TB
        accTitle: Test with a padded image
        accDescr: The last 4 bytes of each row of an image with a stride of 644 are made dark; if the decision function read the padding the defects would be 2020 pixels, and if it does not they are only the 100 pixels of the square.
        A["Make the last 4 bytes of each row dark"] --> B["Count with the decision function"]
        B --> C{"Number of defect pixels"}
        C -->|"100"| D["Padding not read"]
        C -->|"2020"| E["Padding read too"]

Figure 11: With the padding made dark, 100 defect pixels means the decision function does not read the padding.

Calling from C#

On the C# side, the struct definitions, the LibraryImport declarations and the wrapper that pins the buffer with fixed and makes the call are all in one file.

using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;

namespace Inspection;

[StructLayout(LayoutKind.Sequential)]
public struct InspectParams
{
    public int Threshold;        // Pixels darker than this count as defects (0-255)
    public int MaxDefectPixels;  // Fail if the number of defect pixels exceeds this
}

[StructLayout(LayoutKind.Sequential)]
public struct InspectResult
{
    public long DefectPixels;
    public int MinX, MinY, MaxX, MaxY;  // Bounding box of the defects; -1 if there are none
    public int Verdict;                 // 0 = pass, 1 = fail
}

public enum InspectStatus
{
    Ok = 0,
    NullPointer = 1,
    BadGeometry = 2,
    BufferTooSmall = 3,
    BadParameter = 4,
    InternalError = 99,
}

public static unsafe partial class AdaInspector
{
    // Looks for libinspect.dll on Windows and libinspect.so on Linux
    private const string Lib = "libinspect";

    [LibraryImport(Lib, EntryPoint = "inspect_dark_defects")]
    [UnmanagedCallConv(CallConvs = new[] { typeof(CallConvCdecl) })]
    private static partial int InspectDarkDefects(
        byte* pixels, nuint length, int width, int height, int stride,
        InspectParams* parameters, InspectResult* result);

    [LibraryImport(Lib, EntryPoint = "inspect_result_size")]
    [UnmanagedCallConv(CallConvs = new[] { typeof(CallConvCdecl) })]
    public static partial int NativeResultSize();

    [LibraryImport(Lib, EntryPoint = "inspect_elaborated")]
    [UnmanagedCallConv(CallConvs = new[] { typeof(CallConvCdecl) })]
    public static partial int Elaborated();

    public static InspectStatus Inspect(
        ReadOnlySpan<byte> pixels, int width, int height, int stride,
        InspectParams parameters, out InspectResult result)
    {
        InspectResult r;
        int status;

        // The GC does not move the array only inside fixed; Ada reads it only during this call
        fixed (byte* p = pixels)
        {
            status = InspectDarkDefects(
                p, (nuint)pixels.Length, width, height, stride, &parameters, &r);
        }

        result = r;
        return (InspectStatus)status;
    }
}

Both structs consist only of int and long fields and specify LayoutKind.Sequential. Microsoft’s documentation calls such structs blittable types (types whose bit layout is the same in managed and native code) and recommends using them because they can be passed without conversion¹¹. bool is not blittable, so the verdict is also an int, Verdict. C’s int64_t corresponds to C#’s long.

The image is received as a ReadOnlySpan<byte>, pinned with fixed, and then the pointer to its first byte is passed. While the fixed statement runs, the garbage collector does not move the array, and the declared pointer can be used only inside fixed¹². Ada reads only during the call and does not keep the pointer, so this scope is enough. With Span, part of an array or a range made from another buffer can be passed through the same function.

flowchart TB
        accTitle: A pointer valid only inside fixed
        accDescr: Entering fixed pins the array, the Ada function is called inside it, and after Ada finishes reading and returns, leaving fixed lets the GC move the array again.
        A["Enter fixed (pin)"] --> B["Call the Ada function"]
        B --> C["Ada reads only during the call"]
        C --> D["Ada returns"]
        D --> E["Leave fixed (GC can move it)"]
        E -.->|"Not used from here on"| F["Pointer"]

Figure 12: The pointer is valid only inside fixed, so Ada reads only during the call.

Applying fixed to an empty Span yields a NULL pointer, because ReadOnlySpan<T>.GetPinnableReference returns a null reference when the span is empty¹³. The boundary function returns error code 1 for it. The parameters and the result are passed as the addresses of local variables using &. A struct local to a method is not moved by the GC, so its address can be passed as is, as long as the callee does not use the pointer after the method ends¹¹.

The library name is "libinspect". On Windows, .NET looks for libinspect and libinspect.dll, and on Linux for names such as libinspect.so¹⁴. gprbuild produces libinspect.dll on Windows and libinspect.so on Linux, so the same name resolves to both files. The calling convention is specified as CallConvCdecl. On x64 there is only one calling convention, so it makes no difference, but the P/Invoke default on x86 is Stdcall, so specifying it avoids a mismatch on x86¹⁵.

flowchart TB
        accTitle: Files looked up for the name libinspect
        accDescr: Writing libinspect in LibraryImport makes .NET look for libinspect.dll on Windows and libinspect.so on Linux, and both match the file names gprbuild produces.
        A["LibraryImport (libinspect)"] --> B{"Operating system"}
        B -->|"Windows"| C["Look for libinspect.dll"]
        B -->|"Linux"| D["Look for libinspect.so"]
        C --> E["Matches gprbuild output"]
        D --> E

Figure 13: The name libinspect resolves to the file gprbuild produces on both Windows and Linux.

Comparing the struct size on both sides

If the layouts of the C# struct and the Ada record disagree, values are read and written wrongly without any error. Microsoft’s documentation also names differences in type size as a cause of values silently going wrong, and recommends comparing the managed and native sizes¹¹. So the Ada side provides inspect_result_size, and inspection starts only after comparing it with sizeof in C#.

// Compare the struct size on both sides, and do not start inspecting if they differ
int managedSize;
unsafe { managedSize = sizeof(InspectResult); }
int nativeSize = AdaInspector.NativeResultSize();

The Ada side returns Inspect_Result'Max_Size_In_Storage_Elements. Strictly speaking, this attribute is the upper bound on the size needed when an allocator creates the object. With GNAT 13.3.0 on my machine, it was 32, the same as Inspect_Result'Object_Size / System.Storage_Unit, which is the number of bytes of the object. To make the intent clear, use the latter. On Linux, both C’s sizeof and Ada gave 32 bytes. The 64-bit integer comes first, and the 20 bytes of the five ints that follow get 4 bytes of padding to make a multiple of 8. Even if the sizes match, the field order is not necessarily the same, so the C declaration is the reference for the field order and both sides are written from it.

flowchart TB
        accTitle: Aligning the result struct across three languages
        accDescr: The Ada record and the C# struct are written from the C declaration of inspect_result as the reference, their sizes are compared with Ada's inspect_result_size and C#'s sizeof, and inspection starts only when they are the same.
        A["C declaration (reference)"] --> B["Ada record (Convention C)"]
        A --> C["C# struct (Sequential)"]
        B --> D["inspect_result_size"]
        C --> E["sizeof"]
        D --> F{"Same size?"}
        E --> F
        F -->|"Same"| G["Start inspecting"]
        F -->|"Different"| H["Do not start inspecting"]

Figure 14: Write both sides from the C declaration as the reference, and start inspecting only when the sizes match.

These are the results of calling the DLL from a .NET 10 console app on a GitHub Actions Windows runner. It uses the same image and values as the C test driver, except that the last line uses an empty Span.

elaborated=1 result size: C#=32 Ada=32
ng (max 50)        status=Ok defects=100 bbox=(100,50)-(109,59) verdict=1
ok (max 200)       status=Ok defects=100 bbox=(100,50)-(109,59) verdict=0
padded stride      status=Ok defects=100 bbox=(100,50)-(109,59) verdict=0
buffer too small   status=BufferTooSmall defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
width > stride     status=BadGeometry defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
threshold 300      status=BadParameter defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
max -1             status=BadParameter defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
empty span         status=NullPointer defects=0 bbox=(-1,-1)-(-1,-1) verdict=1
ALL PASSED

For buffer too small, a Span one byte shorter was sliced from a 644 × 480 byte array and passed. The dimensions are the same, but the length C# passes is too short, so Ada returns error code 3 without reading the array.

Using it from a WPF window

From a WPF window, the app captures an image when a button is pressed, displays it and then inspects it. In place of a camera, there is a function that creates the same image as the tests.

    private async void InspectButton_Click(object sender, RoutedEventArgs e)
    {
        const int width = 640, height = 480, stride = 640;
        byte[] frame = CaptureFrame(width, height, stride);  // Stands in for an image received from the camera

        FrameImage.Source = BitmapSource.Create(
            width, height, 96, 96, PixelFormats.Gray8, null, frame, stride);

        var parameters = new InspectParams { Threshold = 64, MaxDefectPixels = 50 };
        InspectButton.IsEnabled = false;
        bool fatal = false;
        try
        {
            // Inspect off the UI thread. Do not modify frame until it finishes
            var (status, result) = await Task.Run(() =>
            {
                var s = AdaInspector.Inspect(frame, width, height, stride, parameters, out var r);
                return (s, r);
            });

            // 99 is an unexpected failure. An invalid memory access is possible, so never call the DLL again
            fatal = status == InspectStatus.InternalError;
            ResultText.Text = status == InspectStatus.Ok
                ? $"{(result.Verdict == 0 ? "Pass" : "Fail")}  Defects: {result.DefectPixels} pixels"
                : fatal
                    ? "Inspection stopped. Save the log and restart the app"
                    : $"Could not inspect ({status})";
        }
        finally
        {
            InspectButton.IsEnabled = !fatal;
        }
    }

When the status is 99 (InternalError), the button stays disabled and the DLL is never called again. As described in the section “Stopping exceptions in the boundary function and turning them into error codes”, 99 can also come back when an unreadable address was passed, so the app stops inspecting, keeps a log and is restarted.

The inspection is moved off the UI thread with Task.Run. With large images the decision can take time, and this keeps the window from freezing in the meantime. WPF UI elements can be touched only from the thread that created them¹⁶, so the result is written to ResultText after the await, once execution is back on the UI thread. The relationship between async and the UI thread in WPF is summarized in “WPF/WinForms async and the UI Thread on One Sheet”.

Ada reads frame without copying it. If the next image is written into the same array before the inspection finishes, Ada inspects a half-written image. To capture and inspect in parallel, prepare several capture buffers and never write into a buffer that is being inspected. How to cycle buffers so that capture drops nothing is covered in “Frame Acquisition Without Drops Using Ada Tasks”.

flowchart TB
        accTitle: The WPF UI thread and the inspection thread
        accDescr: The UI thread captures and displays the image, hands the inspection to another thread with Task.Run, the inspection thread calls the Ada function and returns the result, the UI thread after the await displays the result, and the image array is not modified in the meantime.
        A["UI thread captures and displays"] --> B["Hand off inspection with Task.Run"]
        B --> C["Inspection thread calls Ada"]
        C --> D["UI thread displays after await"]
        E["Do not modify the array until inspection ends"] -.-> C

Figure 15: Inspection runs on another thread, and the result is displayed after returning to the UI thread.

This example omits the struct size comparison and the initialization check described in the previous section. A real app checks them once at startup before it starts inspecting.

I confirmed that this WPF example builds with dotnet build on the Windows runner. The revised code, which no longer re-enables the button after a 99, was built on my Linux machine with .NET SDK 10.0.114 and EnableWindowsTargeting specified. Neither produced warnings or errors. I did not display the window or operate it.

Initialization and DLL deployment

The library is built from a gprbuild project file as a stand-alone library that initializes itself automatically¹⁰.

library project Inspect is
   for Source_Dirs use ("src");
   for Object_Dir use "obj";
   for Library_Name use "inspect";
   for Library_Dir use "lib";
   for Library_Kind use "dynamic";
   for Library_Interface use ("Inspect_API");
   for Library_Auto_Init use "true";
end Inspect;

What Library_Auto_Init means, and the restriction that tasks cannot be declared at library level on Windows¹⁷, were covered in the initialization section of “Connecting Ada with C and C#”⁷. Inspect_API and Inspect_Core in this example have no tasks, so the restriction does not apply.

Whether initialization has completed can be checked with inspect_elaborated. The variable is set to 1 after the begin at the end of the package body, so it returns 1 if initialization has run. Both the C test driver on Linux and the C# app on the Windows runner got 1 without calling any initialization procedure.

Signal handlers are replaced on Linux

On Linux, the library’s automatic initialization replaces the process’s signal handlers. The GNAT runtime maps signals such as SIGSEGV to Ada exceptions¹⁸ and installs its handlers during initialization. When a C program installed handlers for SIGSEGV, SIGBUS, SIGFPE, SIGILL and SIGABRT and then loaded the library with dlopen, all five had been replaced by GNAT’s.

This becomes a problem when the process that loads the library uses signals itself. In a .NET 10 console app on Linux, after the library was loaded and initialized, a null dereference in managed code could not be caught as a NullReferenceException. The process printed the following message and terminated with exit code 1. The output shows that GNAT’s handler received the SIGSEGV caused by the null dereference and turned it into an Ada Storage_Error.

raised STORAGE_ERROR : stack overflow or erroneous memory access

flowchart TB
        accTitle: Signal handlers when the library is loaded on Linux
        accDescr: Handlers for SIGSEGV and other signals installed by the host process are replaced by GNAT's handlers during the library's automatic initialization, and GNAT receives subsequent signals.
        A["Host installs handlers"] --> B["Load the library with dlopen"]
        B --> C["Automatic initialization"]
        C --> D["Replaced by GNAT's handlers"]
        D --> E["GNAT receives SIGSEGV"]
        E -.->|"With .NET"| F["Null dereference cannot be caught"]

Figure 16: On Linux, loading the library replaces the host’s signal handlers with GNAT’s.

GNAT has pragma Interrupt_State, which keeps the runtime from installing handlers¹⁸. With GNAT 13.3.0 on my machine, specifying State => System for the five signals left the host’s handlers in place. However, this made the library link the tasking runtime (libgnarl), and many signals, including SIGTERM and the real-time signals, became blocked in the thread that loaded it. Since this is no solution for loading the library into a host that uses signals itself, this article leaves calling it from .NET on Linux out of scope.

flowchart TB
        accTitle: The result of adding pragma Interrupt_State
        accDescr: Specifying System as the State in pragma Interrupt_State keeps the host's signal handlers, but the tasking runtime is linked and many signals are blocked, so it is no solution for a host that uses signals.
        A["Interrupt_State (State => System)"] --> B["Host's handlers remain"]
        A --> C["Tasking runtime is linked"]
        C --> D["Many signals are blocked"]
        D --> E["No solution for hosts that use signals"]

Figure 17: pragma Interrupt_State prevents the handlers from being replaced, but it pulls in the tasking runtime and blocks other signals.

According to the GNAT documentation, this pragma cannot be used on Windows¹⁸. On the Windows runner, a null dereference after the library was loaded could be caught as a NullReferenceException.

DLLs to place in the app folder on Windows

Running objdump -p on the libinspect.dll that Alire’s GNAT (16.1.0) built on the Windows runner showed dependencies on Windows’ KERNEL32.dll and msvcrt.dll, plus the GNAT runtime’s libgnat-16.dll and libgcc_s_seh-1.dll. The latter two are in the bin folder of the GNAT toolchain, so place them in the app folder together with libinspect.dll.

When the console app was run in a folder without the GNAT runtime DLLs, the process terminated with the following unhandled exception. Even though libinspect.dll itself is in the folder, the message says that libinspect or one of its dependencies cannot be loaded.

Unhandled exception. System.DllNotFoundException: Unable to load DLL 'libinspect' or one of its dependencies: The specified module could not be found. (0x8007007E)

The exception was thrown at the first call, NativeResultSize, and the process exit code was −532462766 (0xE0434352). If this exception appears while libinspect.dll is present, suspect the DLLs it depends on.

flowchart TB
        accTitle: Files to place in the app folder
        accDescr: libinspect.dll and the GNAT runtime DLLs are placed in the same folder as the WPF app's executable, and a missing runtime DLL results in DllNotFoundException.
        A["App folder"] --> B["WPF app (exe and dll)"]
        A --> C["libinspect.dll"]
        A --> D["GNAT runtime DLLs"]
        C --> D
        D -.->|"If missing"| E["DllNotFoundException"]

Figure 18: Place the Ada DLL and the GNAT runtime DLLs together in the app folder.

If a DLL with the same module name is already loaded into the process, Windows uses it, regardless of the folder it was loaded from¹⁹. If the same process contains other DLLs built with GNAT or MinGW and a different version of libgcc_s_seh-1.dll or a similar DLL was loaded first, that one is used. The encapsulated option, which pulls the GNAT runtime into the DLL itself, and the results of testing it are mentioned in “Connecting Ada with C and C#”. The folders Windows searches for DLLs and their order are summarized in “How Windows DLL Name Resolution Works - Search Order and SxS”.

Test environment and what was not verified

The code in this article was run on November 10, 2026, in the following environments.

• Ubuntu 24.04, GNAT 13.3.0 and the Ubuntu gprbuild package (2024.1). I built the shared library and called it from the C test driver to obtain the results above. The replacement of signal handlers on loading, the return value when an unreadable address is passed, and the linking and signal blocking with pragma Interrupt_State were also checked here with C programs. The build with pragma Restrictions (No_Secondary_Stack), the address of the array parameter and the attribute values were also checked here. The WPF example, changed so that the button is not re-enabled after 99, was built here with .NET SDK 10.0.114 and EnableWindowsTargeting specified.
• A GitHub Actions Linux runner (ubuntu-24.04) and Alire’s GNAT (gnat_native 16.1.0). I proved Inspect_Core with GNATprove (FSF 16.1.0) and called the shared library from the C test driver and a .NET 10 console app. The null dereference test was also done here.
• A GitHub Actions Windows runner (windows-latest, image windows-2025-vs2026), Alire’s GNAT (gnat_native 16.1.0) and .NET SDK 10.0.403. I built the DLL, called it from the console app, tried running without the runtime DLLs and passing an unreadable address, ran the null dereference test, and built the WPF example.

I did not verify behavior in the WPF window, 32-bit Windows, buffers passed by a real camera SDK, the speed of the decision, or behavior when called from several threads at once. Calling the library from .NET on Linux is out of scope for the reasons given above. The correctness of the boundary function (the part outside SPARK) was checked by the tests above and by review, not by proof. The full project used for verification is not published, and 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 are:

• Proving Image Processing Free of Out-of-Bounds Access with SPARK — Binarization, Smoothing, Labeling and a Speed Comparison with C
• Receiving GigE Vision Packets with Ada Types — Pitfalls of Representation Clauses and a SPARK-Proved Parser
• Frame Acquisition Without Drops Using Ada Tasks — A Protected-Object Ring Buffer and Priorities
• Separating Pixels and Millimeters with Types — Preventing Unit Mix-ups in Dimensional Inspection with Ada

Related existing articles:

• Connecting Ada with C and C# — Building a DLL and Calling It
• Proving AI-Written Code with SPARK ── Humans Write the Contracts, GNATprove Checks Them
• Dropped Frames with GigE Vision and USB3 Vision Cameras — Locating the Cause and the Windows Settings to Review
• Safely Calling Win32 APIs from C# — A Practical P/Invoke Guide (DllImport / LibraryImport / CsWin32)

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.

How can I pass an image from C# to an Ada DLL without copying it?

In C#, pin the array or Span with fixed and pass the pointer to its first byte, the buffer length, and the width, height and stride (bytes per row). On the Ada side, check that the dimensions fit within the buffer length, then view the same memory as a two-dimensional array with Address and Import. Ada reads it only during the call and does not keep the pointer.

How do I keep Ada exceptions from reaching C#?

Put an exception handler at the end of each function that C# calls directly, and turn every exception into error code 99. Check parameter ranges with if statements instead of relying on exceptions, and return 4 when they are out of range. Code 99 can also come back when memory could not be read because of a wrong pointer or length, so treat it as a signal to stop inspecting.

How do I check that a C# struct and an Ada record have the same layout?

Give both sides Convention => C and StructLayout(LayoutKind.Sequential) so that they follow the same layout as the C struct. Then provide a function on the Ada side that returns the size of the struct, and compare it with sizeof in C# before starting any inspection. In this article's example, both were 32 bytes.

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.