Re: SPARK hide directive, hiding separate declaration.

[roderick.chapman@googlemail.com]

On Jan 3, 11:59 am, leeeruss...@gmail.com wrote:
> Is there any thing like an --# unhide directive that would allow me to
> let SPARK see the declaration in the body, but nothing else?

Basically, the answer is "no".  Once something is hidden,
then that's that - it's Ada not SPARK.

If you're hiding an entire package body, then the
hide annotation is considered to hide the body AND
any subunits of it.

It's actually quite unusual to hide an entire package body,
since if the entire body is Ada (not SPARK), then just
don't submit it to the Examiner at all.

If the package body is mostly SPARK with hidden
subprograms, then move your subunit "up" into
the SPARK part of the package body and analyse it
there.

All the best,
 Rod Chapman, SPARK Team, Praxis

PS...if you're a supported SPARK customer, then
such enquiries should _always_ be sent to
sparkinfo@praxis-his.com - posting to comp.lang.ada
does not guarantee a response (well..certainly not from
SPARK Team anyway...)