Minor SPARK problem concerning 'redundant' with clauses.

Minor SPARK problem concerning 'redundant' with clauses.

[xorquewasp]

I have a package P1 that uses the value of a constant defined in P2.

SPARK requires me to --# inherit P2 and the only place the annotation
can appear is in the spec of P1. The Ada compiler, however, sees that
the constant is only referenced in the body and complains loudly that
the 'with' clause is redundant and might be moved into the body of P2.

Is there a sensible solution to stop the two systems treading on each
other like this? In most cases, I can hack around the problem with a
spurious 'use type' clause (as much as I dislike it).

I tried to use pragma Warnings (Off) to wrap the "redundant" with
clauses, but of course SPARK immediately rejected it:

***        Syntax Error      : No complete PRAGMA_REP can be followed
by
           reserved word "WITH" here.

Re: Minor SPARK problem concerning 'redundant' with clauses.

[sjw]

On Jun 10, 8:31 pm, xorquew...@googlemail.com wrote:
> I have a package P1 that uses the value of a constant defined in P2.
>
> SPARK requires me to --# inherit P2 and the only place the annotation
> can appear is in the spec of P1. The Ada compiler, however, sees that
> the constant is only referenced in the body and complains loudly that
> the 'with' clause is redundant and might be moved into the body of P2.
>
> Is there a sensible solution to stop the two systems treading on each
> other like this? In most cases, I can hack around the problem with a
> spurious 'use type' clause (as much as I dislike it).

You could explore the options available with -gnatw, perhaps? None
look appropriate at first glance, but ..

Re: Minor SPARK problem concerning 'redundant' with clauses.

[britt.snodgrass]

I'm getting a bit rusty with my SPARK, but I think the with clause can
be moved to the package body (only the body) while the inherit
annotation remains in the package spec.  We always build with the -
gnatwa switch to enable all optional warnings and I think this warning
was easy to fix by moving the "with" to the body.

- Britt

Re: Minor SPARK problem concerning 'redundant' with clauses.

[xorque]

On Jun 10, 9:55 pm, britt.snodgr...@gmail.com wrote:
> I'm getting a bit rusty with my SPARK, but I think the with clause can
> be moved to the package body (only the body) while the inherit
> annotation remains in the package spec.  We always build with the -
> gnatwa switch to enable all optional warnings and I think this warning
> was easy to fix by moving the "with" to the body.

I see, thanks. I wasn't aware that 'with' and 'inherit' could be
distinct like that.

Re: Minor SPARK problem concerning 'redundant' with clauses.

[Robin Messer]

Britt is right. The correct solution is to move the "with" to the
package
body. As an aside, the SPARK Examiner recognises certain pragmas, but
in
the majority of cases it just issues a warning and continues its
analysis.
It is, however, a bit more fussy about where pragmas can be placed.
The following code is accepted by the Examiner (with a warning about
the
pragma).

pragma Warnings (Off);
with Q;
--# inherit Q;
package P
is
      type T is range 0 .. 100;
end P;

--
Robin