Assertion_Policy implementation regarding Aspect Features

[Anh Vo <anhvofrcaus@gmail.com>]

I revisited "about the new Ada 2012 pre/post conditions" thread posted by Nasser M. Abbasi, https://groups.google.com/forum/?fromgroups#!search/aspect$20example$20in$20Ada$202012/comp.lang.ada/t4w2M1NVFwI/qOXDIyT6JJ0J.

This inspires me to learn this feature a little bit deeper. I would like to know if GNAT comply with ARM by showing the following scenarios.


------------ Scenario 1 --------------
with Ada.Text_Io;
with Ada.Exceptions; use Ada;

procedure Predicates_Test is
   use Text_Io;

   type Even is new Integer range 0 .. Integer'Last
      with Dynamic_Predicate => Even mod 2 = 0,
           Default_Value => 0;

   My_Number : Even; -- set to 0 by default

begin
   Put_Line ("Predicates_Test starts");
   Put_Line ("Initial My_Number => " & My_Number'Img);
   My_Number := 3;  -- intentionally violate predicate rules
   Put_Line ("Final My_Number => " & My_Number'Img);
   Put_Line ("Predicates_Test ends");
exception
   when Err : others =>
      Put_Line ("Houston we have a problem: " & 
                                       Exceptions.Exception_Information(Err));
end Predicates_Test;

 For scenario 1 the code is compiled with gnatmake -gnat12 -gnata. When running this program, the output is as follows: 

Predicates_Test starts
My_Number =>  0
Houston we have a problem: Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: predicate failed at predicates_test.adb:16

Observation: GNAT implemented the Aspect feature even pragma Assertion_Policy (Check) is not present.


------------ Scenario 2 --------------
pragma Assertion_Policy (Check);
with Ada.Text_Io;
with Ada.Exceptions; use Ada;

procedure Predicates_Test is
   use Text_Io;

   type Even is new Integer range 0 .. Integer'Last
      with Dynamic_Predicate => Even mod 2 = 0,
           Default_Value => 0;

   My_Number : Even; -- set to 0 by default

begin
   Put_Line ("Predicates_Test starts");
   Put_Line ("Initial My_Number => " & My_Number'Img);
   My_Number := 3;  -- intentionally violate predicate rules
   Put_Line ("Final My_Number => " & My_Number'Img);
   Put_Line ("Predicates_Test ends");
exception
   when Err : others =>
      Put_Line ("Houston we have a problem: " & 
                                       Exceptions.Exception_Information(Err));
end Predicates_Test;


For scenario 2, it is compliled with gnatmake -gnat12. Then running this program yielding output as

Predicates_Test starts
Initial My_Number =>  0
Final My_Number =>  3
Predicates_Test ends

Observation: GNAT did not implement the Aspect feature even though pragma Assertion_Policy (Check) is present.


------------ Scenario 3 --------------
pragma Assertion_Policy (Check);
with Ada.Text_Io;
with Ada.Exceptions; use Ada;

procedure Predicates_Test is
   use Text_Io;

   type Even is new Integer range 0 .. Integer'Last
      with Dynamic_Predicate => Even mod 2 = 0,
           Default_Value => 0;

   My_Number : Even; -- set to 0 by default

begin
   Put_Line ("Predicates_Test starts");
   Put_Line ("Initial My_Number => " & My_Number'Img);
   My_Number := 3;  -- intentionally violate predicate rules
   Put_Line ("Final My_Number => " & My_Number'Img);
   Put_Line ("Predicates_Test ends");
exception
   when Err : others =>
      Put_Line ("Houston we have a problem: " & 
                                       Exceptions.Exception_Information(Err));
end Predicates_Test;


For scenario 3, it is compliled with gnatmake -gnat12 -gnata. Then running this program yielding output as below.

Predicates_Test starts
Initial My_Number =>  0
Houston we have a problem: Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: predicate failed at predicates_test.adb:17


Observation: GNAT implements Aspect feature through compiler option.


Thanks in advance for your insight.


Anh Vo