Prev: using jGRASP to compile Ada
Next: GNAT GPL 2008 is out
From: leeerussell on 3 Jan 2008 06:59 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
From: roderick.chapman on 3 Jan 2008 22:16 On Jan 3, 11:59 am, leeeruss...(a)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(a)praxis-his.com - posting to comp.lang.ada does not guarantee a response (well..certainly not from SPARK Team anyway...)
|
Pages: 1 Prev: using jGRASP to compile Ada Next: GNAT GPL 2008 is out |