Assertion_Policy implementation regarding Aspect Features

Assertion_Policy implementation regarding Aspect Features

[Anh Vo]

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

Re: Assertion_Policy implementation regarding Aspect Features

[Simon Wright]

Anh Vo <anhvofrcaus@gmail.com> writes:

> 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.

The fact that you need to enable assertions with -gnata seems to be a
GNAT feature, so we'll maybe need to add -gnata to the other flags
needed to make GNAT a standard-conforming compiler (-fstack-check,
-gnato).

I don't see in the ARM anything that says what the default
Assertion_Policy should be.

On the other hand, the fact that your predicate isn't disabled by pragma
Assertion_Policy (Ignore) may be a failure to comply with the second
sentence of ARM 11.4.2(10)[1]:

   The policy_identifier Check requires that assertion expressions of
   the given aspect be checked that they evaluate to True at the points
   specified for the given aspect; the policy_identifier Ignore requires
   that the assertion expression not be evaluated at these points, and
   the run-time checks not be performed.

because of a misinterpretation of the last sentence:

   Note that for subtype predicate aspects (see 3.2.4), even when the
   applicable Assertion_Policy is Ignore, the predicate will still be
   evaluated as part of membership tests and Valid attribute_references,
   and if static, will still have an effect on loop iteration over the
   subtype, and the selection of case_statement_alternatives and
   variants.

[1] http://www.ada-auth.org/standards/12rm/html/RM-11-4-2.html#p10



   

Re: Assertion_Policy implementation regarding Aspect Features

[Anh Vo]

On Saturday, February 9, 2013 2:24:41 AM UTC-8, Simon Wright wrote:
> Anh Vo <anhvofrcaus@gmail.com> writes:
> 
> 
> > 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.
> 
> On the other hand, the fact that your predicate isn't disabled by pragma
> 
> Assertion_Policy (Ignore) may be a failure to comply with the second
> 
> sentence of ARM 11.4.2(10)[1]:
> 

Thank you for your analysis. It does not make sense to comply with pragma Assertion_Policy thru compiler option. 

Re: Assertion_Policy implementation regarding Aspect Features

[Georg Bauhaus]

On 09.02.13 11:24, Simon Wright wrote:
> The fact that you need to enable assertions with -gnata seems to be a
> GNAT feature, so we'll maybe need to add -gnata to the other flags
> needed to make GNAT a standard-conforming compiler (-fstack-check,
> -gnato).

Should this additional flag be reported as missing from
http://gcc.gnu.org/onlinedocs/gnat_rm/Strict-Conformance-to-the-Ada-Reference-Manual.html

Re: Assertion_Policy implementation regarding Aspect Features

[Anh Vo]

On Saturday, February 9, 2013 10:04:10 AM UTC-8, Georg Bauhaus wrote:
>> On 09.02.13 11:24, Simon Wright wrote: 
>> The fact that you need to enable assertions with -gnata seems to be a 
>> GNAT feature, so we'll maybe need to add -gnata to the other flags 
>> needed to make GNAT a standard-conforming compiler (-fstack-check, > -gnato). 

>Should this additional flag be reported as missing from >http://gcc.gnu.org/onlinedocs/gnat_rm/Strict-Conformance-to-the-Ada-Reference->Manual.html

Robert Dewar confirms that Assertion_Policy is not fully implemented yet.  A full implementation is being worked on as we speak. I am sure that this full implementation will be in gnat-gpl-2013.