SPARK hide directive, hiding separate declaration.

SPARK hide directive, hiding separate declaration.

[leeerussell]

Hello everyone

I think I may have found a similar problem discussed when searching,
but I felt that this problem is sufficiently different to warrant a
new post.

I am getting the following error code when using SPARK examiner:

Semantic Error   : 10: Illegal redeclaration of identifier foo.

The error is happening because I have a declaration of a separate in a
body that is otherwise all hidden from SPARK (using --# hide).  The
SPARK examiner cannot see the hidden declaration, so is complaining
about the separate.

Is there any thing like an --# unhide directive that would allow me to
let SPARK see the declaration in the body, but nothing else?

Thanks for any help

Lee Russell

Re: SPARK hide directive, hiding separate declaration.

[roderick.chapman]

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