* Re: Aspect programming
2011-07-28 4:56 ` AdaMagica
@ 2011-07-28 14:25 ` Robert A Duff
2011-07-28 18:13 ` Adam Beneschan
` (2 subsequent siblings)
3 siblings, 0 replies; 11+ messages in thread
From: Robert A Duff @ 2011-07-28 14:25 UTC (permalink / raw)
AdaMagica <christ-usch.grein@t-online.de> writes:
> You're using GNAT, which requires one compilation unit per file.
By default. There are ways to get around that, but the easiest
thing is to follow GNAT's default convention.
> Thus your pragma Assertion_Policy applies only to the unit where it is
> in the context clause.
>
> If you want it to apply to all units, you have to use it as a
> configuration pragma.
Right, or use the -gnata switch.
- Bob
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Aspect programming
2011-07-28 4:56 ` AdaMagica
2011-07-28 14:25 ` Robert A Duff
@ 2011-07-28 18:13 ` Adam Beneschan
2011-07-28 19:38 ` Adam Beneschan
2011-07-29 16:09 ` Anh Vo
2011-07-29 11:03 ` Martin
2011-08-01 18:20 ` Anh Vo
3 siblings, 2 replies; 11+ messages in thread
From: Adam Beneschan @ 2011-07-28 18:13 UTC (permalink / raw)
On 7/27/2011 9:56 PM, AdaMagica wrote:
> You're using GNAT, which requires one compilation unit per file.
> Thus your pragma Assertion_Policy applies only to the unit where it is
> in the context clause.
>
> If you want it to apply to all units, you have to use it as a
> configuration pragma.
I don't think this is entirely accurate. The RM says (10.1.5(8)) that
configuration pragmas appear before the first compilation unit of a
"compilation", and "The pragma applies to all compilation_units
appearing in the compilation, unless there are none, in which case it
applies to all future compilation_units compiled in the same environment."
It's not clear which one applies in the original poster's case. If GNAT
does disallow more than one compilation unit per file, then clearly the
source in the original post must actually be multiple files (or else it
wouldn't have worked), and we weren't really told where the dividing
lines between the files are. For all we know, the first
Assertion_Policy pragma could have been in its own file.
But even if the first Assertion_Policy was in the same file as the
Aspect_Programming_Test procedure, it's still a configuration pragma.
The difference here is that it's a configuration pragma that applies
only to Aspect_Programming_Test and not to any of the other compilation
units (it appears that there's another Assertion_Policy that applies to
the body of Stacks). But it's still a configuration pragma, so I think
you really wanted to say something like "you have to use it as an
environment-wide configuration pragma" or whatever the correct term is.
Even so, I still don't think this is the right answer. Regarding
preconditions, 6.1.1(20) says, "If the assertion policy in effect at the
point of a subprogram or entry declaration is Check, then upon a call of
the subprogram ... precondition checks are performed ...". So where is
the subprogram declaration? Since Stacks is a generic, I think that the
declarations of Int_Stacks.Push and Int_Stacks.Pop occur at the point
the Stacks generic is instantiated, which where the instance Int_Stacks
is declared, which is inside Aspect_Programming_Test; thus, even if the
first Assertion_Policy is a configuration pragma that applies only to
Aspect_Programming_Test, it still should apply here, and the
precondition checks should be performed. However, I haven't researched
all the relevant language rules carefully, and there may be some rules
that affect when assertion policies apply to declarations (or Assert
pragmas) created by instantiation.
-- Adam
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Aspect programming
2011-07-28 18:13 ` Adam Beneschan
@ 2011-07-28 19:38 ` Adam Beneschan
2011-07-29 16:09 ` Anh Vo
1 sibling, 0 replies; 11+ messages in thread
From: Adam Beneschan @ 2011-07-28 19:38 UTC (permalink / raw)
On 7/28/2011 11:13 AM, Adam Beneschan wrote:
>However, I haven't researched
> all the relevant language rules carefully, and there may be some rules
> that affect when assertion policies apply to declarations (or Assert
> pragmas) created by instantiation.
OK, I just ran across 11.4.2(17), which says "The assertion policy that
applies to a generic unit also applies to all its instances". 11.4.2
also talks about a default assertion policy that applies when there's no
explicit Assertion_Policy that applies to a compilation unit; this
policy is implementation-defined, and I don't know how GNAT defines it,
and I don't feel like looking it up, but I assume that GNAT's default is
that assertions aren't checked... is that right?
I assume that "an assertion policy applying to its instances" means that
this policy supersedes anything that might be in effect elsewhere in the
compilation unit; although the RM doesn't say this explicitly, it looks
like this is the intent, and I haven't yet found any corner cases where
the RM doesn't provide a clear answer about what's supposed to happen.
So I guess you can ignore the last paragraph of my previous post.
-- Adam
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Aspect programming
2011-07-28 18:13 ` Adam Beneschan
2011-07-28 19:38 ` Adam Beneschan
@ 2011-07-29 16:09 ` Anh Vo
2011-07-29 19:48 ` Adam Beneschan
1 sibling, 1 reply; 11+ messages in thread
From: Anh Vo @ 2011-07-29 16:09 UTC (permalink / raw)
On Jul 28, 11:13 am, Adam Beneschan <a...@irvine.com> wrote:
> On 7/27/2011 9:56 PM, AdaMagica wrote:
>
> > You're using GNAT, which requires one compilation unit per file.
> > Thus your pragma Assertion_Policy applies only to the unit where it is
> > in the context clause.
>
> > If you want it to apply to all units, you have to use it as a
> > configuration pragma.
>
> It's not clear which one applies in the original poster's case. If GNAT
> does disallow more than one compilation unit per file, then clearly the
> source in the original post must actually be multiple files (or else it
> wouldn't have worked), and we weren't really told where the dividing
> lines between the files are. For all we know, the first
> Assertion_Policy pragma could have been in its own file.
Actually, each program unit is in a separate file per GNAT convention.
While posting, I just copy and past their contents one after the
other.
When using switch -gnata, GNAT crashes with a bug box. Harry Tucker
already submitted a bug reported.
Anh Vo
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Aspect programming
2011-07-29 16:09 ` Anh Vo
@ 2011-07-29 19:48 ` Adam Beneschan
0 siblings, 0 replies; 11+ messages in thread
From: Adam Beneschan @ 2011-07-29 19:48 UTC (permalink / raw)
On 7/29/2011 9:09 AM, Anh Vo wrote:
>>> If you want it to apply to all units, you have to use it as a
>>> configuration pragma.
>>
>> It's not clear which one applies in the original poster's case. If GNAT
>> does disallow more than one compilation unit per file, then clearly the
>> source in the original post must actually be multiple files (or else it
>> wouldn't have worked), and we weren't really told where the dividing
>> lines between the files are. For all we know, the first
>> Assertion_Policy pragma could have been in its own file.
>
> Actually, each program unit is in a separate file per GNAT convention.
> While posting, I just copy and past their contents one after the
> other.
In that case, where was the Assertion_Policy pragma that you included at
the top of your source? In the same file as Aspect_Programming_Test, or
in its own file? If "file" == "compilation" on GNAT, then according to
the language rules, if you included it in the same file (compilation) as
the procedure, it would have applied only to the procedure.
However it's done, I believe that Assertion_Policy(Check) has to be
applied to the specification of the Stacks generic package in order for
you to get the checks to happen. I don't know what works on GNAT or
what doesn't. But adding the pragma to the top of stacks.ads should
work. Compiling it as a configuration pragma that applies to "all
future compilation_units compiled into the same environment" (10.1.5(8))
should work too, according to the language rules, but Martin's earlier
comment seems to imply that it doesn't.
-- Adam
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Aspect programming
2011-07-28 4:56 ` AdaMagica
2011-07-28 14:25 ` Robert A Duff
2011-07-28 18:13 ` Adam Beneschan
@ 2011-07-29 11:03 ` Martin
2011-07-30 2:31 ` Harry Tucker
2011-08-01 18:20 ` Anh Vo
3 siblings, 1 reply; 11+ messages in thread
From: Martin @ 2011-07-29 11:03 UTC (permalink / raw)
On Jul 28, 5:56 am, AdaMagica <christ-usch.gr...@t-online.de> wrote:
> You're using GNAT, which requires one compilation unit per file.
> Thus your pragma Assertion_Policy applies only to the unit where it is
> in the context clause.
>
> If you want it to apply to all units, you have to use it as a
> configuration pragma.
Behaviour doesn't change even if you provide the configuration
pragma's in a file and specify the Global_Configuration_Pragmas in
the .gpr file...
-- Martin
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Aspect programming
2011-07-29 11:03 ` Martin
@ 2011-07-30 2:31 ` Harry Tucker
0 siblings, 0 replies; 11+ messages in thread
From: Harry Tucker @ 2011-07-30 2:31 UTC (permalink / raw)
But then when the compiler outputs the below when compiling his code I
think that something else is going on.
+===========================GNAT BUG
DETECTED==============================+
| GPL 2011 (20110428) (i686-pc-mingw32) GCC
error: |
| in gnat_to_gnu_entity, at ada/gcc-interface/decl.c:
329 |
| Error detected at stacks.ads:28:23 [aspect_programming_test.adb:
26:4] |
| Please submit a bug report by email to
report@adacore.com. |
| GAP members can alternatively use GNAT
Tracker: |
| http://www.adacore.com/ section 'send a
report'. |
| See gnatinfo.txt for full info on procedure for submitting
bugs. |
| Use a subject line meaningful to you and us to track the
bug. |
| Include the entire contents of this bug box in the
report. |
| Include the exact gcc or gnatmake command that you
entered. |
| Also include sources listed below in gnatchop
format |
| (concatenated together with no headers between
files). |
| Use plain ASCII or MIME
attachment. |
+==========================================================================
+
And from the GNAT RM, Sec 13:
"AI-0183 Aspect specifications (2010-08-16)
Aspect specifications have been fully implemented except for pre and
post- conditions, and type invariants, which have their own separate
AI's. All forms of declarations listed in the AI are supported..."
So I would expect some issues to arise.
In my own play with aspects I haven't seen this bug-box.
Harry
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Aspect programming
2011-07-28 4:56 ` AdaMagica
` (2 preceding siblings ...)
2011-07-29 11:03 ` Martin
@ 2011-08-01 18:20 ` Anh Vo
3 siblings, 0 replies; 11+ messages in thread
From: Anh Vo @ 2011-08-01 18:20 UTC (permalink / raw)
On Jul 27, 9:56 pm, AdaMagica <christ-usch.gr...@t-online.de> wrote:
> You're using GNAT, which requires one compilation unit per file.
> Thus your pragma Assertion_Policy applies only to the unit where it is
> in the context clause.
>
> If you want it to apply to all units, you have to use it as a
> configuration pragma.
Actually, each program unit is contained in a separate file per GNAT
file / unit convention. Interestingly enough GNAT crashes with a bug
box when -gnata switch is used. In fact, Harry Tucker submitted a bug
report already. In addition, based on Adam's comments, I am convinced
that this is a compiler's bug. By the way, thank you for all replies.
Anh Vo
^ permalink raw reply [flat|nested] 11+ messages in thread