* Assertion_Policy implementation regarding Aspect Features
@ 2013-02-09 1:52 Anh Vo
2013-02-09 10:24 ` Simon Wright
0 siblings, 1 reply; 5+ messages in thread
From: Anh Vo @ 2013-02-09 1:52 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Assertion_Policy implementation regarding Aspect Features
2013-02-09 1:52 Assertion_Policy implementation regarding Aspect Features Anh Vo
@ 2013-02-09 10:24 ` Simon Wright
2013-02-09 14:48 ` Anh Vo
2013-02-09 18:04 ` Georg Bauhaus
0 siblings, 2 replies; 5+ messages in thread
From: Simon Wright @ 2013-02-09 10:24 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Assertion_Policy implementation regarding Aspect Features
2013-02-09 10:24 ` Simon Wright
@ 2013-02-09 14:48 ` Anh Vo
2013-02-09 18:04 ` Georg Bauhaus
1 sibling, 0 replies; 5+ messages in thread
From: Anh Vo @ 2013-02-09 14:48 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Assertion_Policy implementation regarding Aspect Features
2013-02-09 10:24 ` Simon Wright
2013-02-09 14:48 ` Anh Vo
@ 2013-02-09 18:04 ` Georg Bauhaus
2013-02-21 23:21 ` Anh Vo
1 sibling, 1 reply; 5+ messages in thread
From: Georg Bauhaus @ 2013-02-09 18:04 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: Assertion_Policy implementation regarding Aspect Features
2013-02-09 18:04 ` Georg Bauhaus
@ 2013-02-21 23:21 ` Anh Vo
0 siblings, 0 replies; 5+ messages in thread
From: Anh Vo @ 2013-02-21 23:21 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2013-02-21 23:21 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2013-02-09 1:52 Assertion_Policy implementation regarding Aspect Features Anh Vo
2013-02-09 10:24 ` Simon Wright
2013-02-09 14:48 ` Anh Vo
2013-02-09 18:04 ` Georg Bauhaus
2013-02-21 23:21 ` Anh Vo
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox