Run-Time Checks, Assertions, 'Valid & Suppression

Know every language-defined check (range, index, overflow, division, discriminant, tag, access, length, accessibility, elaboration), which exception each raises, use pragma Assert and Assertion_Policy, detect invalid data with 'Valid, and understand pragma Suppress / -gnatp trade-offs.

Ada's safety comes from checks: the compiler proves what it can at compile time, and inserts run-time checks for the rest. When a check fails, an exception is raised instead of corrupting memory. This lesson catalogues the checks, adds programmer-defined assertions, and explains how and when checks may be removed.

Language-Defined Checks

Constraint_Error is raised by: Range_Check (value outside a subtype), Index_Check (array index), Overflow_Check (arithmetic overflow), Division_Check (divide by zero), Length_Check (array assignment lengths), Discriminant_Check (wrong variant), Tag_Check (bad tagged conversion) and Access_Check (null dereference). Program_Error is raised by Accessibility_Check, Elaboration_Check, missing return from a function, and some bounded errors. Storage_Error signals memory or stack exhaustion. Tasking_Error concerns failed task communication. GNAT removes checks it can prove unnecessary and warns when a check will certainly fail.

Names are those used by pragma Suppress/Unsuppress.

• Most checks → Constraint_Error; accessibility/elaboration → Program_Error. • Storage_Error: memory/stack; Tasking_Error: task communication. • The compiler removes provably unnecessary checks.

Check name            Exception          Example
Range_Check           Constraint_Error   P : Percent := 101;
Index_Check           Constraint_Error   A (A'Last + 1)
Overflow_Check        Constraint_Error   Integer'Last + 1
Division_Check        Constraint_Error   X / 0
Length_Check          Constraint_Error   S (1 .. 3) := "abcd";
Discriminant_Check    Constraint_Error   Circle.Width
Tag_Check             Constraint_Error   Square (A_Circle)
Access_Check          Constraint_Error   Null_Ptr.all
Accessibility_Check   Program_Error      dangling 'Access (dynamic)
Elaboration_Check     Program_Error      call before body elaborated

Assertions and 'Valid

'pragma Assert (Condition, "message");' raises Ada.Assertions.Assertion_Error when the condition is False and assertions are enabled (GNAT: -gnata, or pragma Assertion_Policy (Check)). Without a message, GNAT uses the source location as the message. X'Valid checks whether a scalar object holds a valid value of its subtype — essential after Unchecked_Conversion, reading binary files, or receiving data from hardware or foreign code, where the language's checks were bypassed.

• pragma Assert (Cond[, Msg]) → Assertion_Error when enabled. • Enable with -gnata or pragma Assertion_Policy (Check). • X'Valid validates scalars from unchecked sources.

Suppressing Checks

'pragma Suppress (Range_Check);' gives the compiler permission to omit a check in a region; the GNAT switch -gnatp suppresses all checks. If a suppressed check would have failed, the program is erroneous — anything can happen. Suppress only in measured hot spots after proving (ideally with SPARK) that the checks cannot fail. Note that GNAT enables overflow checks by default in modern versions, and -gnato controls their mode.

• pragma Suppress (Check_Name) / -gnatp — permission to omit checks. • A failed suppressed check = erroneous execution. • Prove first (SPARK), measure, then suppress locally.

Code Examples

Each procedure triggers one check; Check reports the exception name. Unchecked_Conversion of 200 into Small (range 1.. 10) produces an invalid value that 'Valid detects. The assertion without a message reports its source location. GNAT also warns at compile time about the constant division by zero and the assertion that will fail. Output: Index check A (4) -> CONSTRAINT_ERROR Division check I / 0 -> CONSTRAINT_ERROR Overflow check Integer'Last + 1 -> CONSTRAINT_ERROR Range check Small (14) -> CONSTRAINT_ERROR pragma Assert -> ADA.ASSERTIONS.ASSERTION_ERROR raise Program_Error -> PROGRAM_ERROR Suppressed scope: no exception S'Valid after Unchecked_Conversion of 200: FALSE S'Valid after Unchecked_Conversion of 7: TRUE Assertion message: l42_checks.adb:55 -- shipping with -gnatp everywhere 'for speed' -- keep checks on; suppress locally only where profiling and proof justify it

Checks usually cost a few percent and catch real bugs in production.

S := To_Small (Raw_Byte); Table (S) := ...; -- trusting unchecked data

S := To_Small (Raw_Byte); if not S'Valid then raise Data_Error; end if;

Unchecked conversions bypass constraints; validate before use.

pragma Assert (Initialize_Device); -- side effect in assertion

Ok := Initialize_Device; pragma Assert (Ok);

Assertions may be disabled; never put required work inside them.

Which exception does a failed index check raise? A. Index_Error B. Constraint_Error C. Program_Error D. Storage_Error

Which switch enables assertions and contracts in GNAT? A. -gnatp B. -gnata C. -O2 D. -gnatwa

What does X'Valid tell you? A. X is initialized B. X holds a valid value of its subtype C. X is not null D. X is aliased

What happens if a check suppressed by pragma Suppress would fail? A. Constraint_Error B. The program is erroneous (undefined behavior) C. Compile error D. A warning Trace the checks example.

Real output: Index check A (4) -> CONSTRAINT_ERROR Division check I / 0 -> CONSTRAINT_ERROR Overflow check Integer'Last + 1 -> CONSTRAINT_ERROR Range check Small (14) -> CONSTRAINT_ERROR pragma Assert -> ADA.ASSERTIONS.ASSERTION_ERROR raise Program_Error -> PROGRAM_ERROR Suppressed scope: no exception S'Valid after Unchecked_Conversion of 200: FALSE S'Valid after Unchecked_Conversion of 7: TRUE Assertion message: l42_checks.adb:55

with Ada.Text_IO;    use Ada.Text_IO;
with Ada.Exceptions; use Ada.Exceptions;
with Ada.Assertions;
with Ada.Unchecked_Conversion;

procedure L42_Checks is
   type Small is range 1 .. 10 with Size => 8;
   type Byte is mod 256;
   function To_Small is new Ada.Unchecked_Conversion (Byte, Small);   --  bypasses checks

   type Arr is array (1 .. 3) of Integer;
   A : Arr := [others => 0];
   I : Integer := 3;
   Zero : constant Integer := 0;
   Big : Integer := Integer'Last;
   S : Small;

   procedure Check (Name : String; Action : access procedure) is
   begin
      Action.all;
      Put_Line (Name & ": no exception");
   exception
      when E : others =>
         Put_Line (Name & " -> " & Exception_Name (E));
   end Check;

   procedure Index_Check is begin I := I + 1; A (I) := 1; end Index_Check;
   procedure Division_Check is begin I := I / Zero; end Division_Check;
   procedure Overflow_Check is begin Big := Big + 1; end Overflow_Check;
   procedure Range_Check is begin S := Small (I + 10); end Range_Check;
   procedure Assertion is begin pragma Assert (Zero > 0, "Zero must be positive"); end Assertion;
   procedure Explicit is begin raise Program_Error; end Explicit;

   proc
…