Re: SPARK Examiner -- visibility of Ada.Strings.Unbounded (and probably lots of other packages)

[Tim Rowe <spamtrap@tgrowe.plus.net>]

Ludovic Brenta wrote:

> I don't think Ada.Strings.Unbounded is part of SPARK. SPARK is a
> *subset* of Ada that removes everything not statically provable.

It isn't. But John Barnes, in High Integrity Software: The SPARK 
Approach to Safety and Security, says "where absolutely essential [...] 
any feature of full Ada [...] can be used in parts of a program covered 
by the special hide directive which tells the examiner that part of a 
program is not to be examined". I just can't work out how to hide the 
relevant bit -- I'm only allowed the hide after immediately after 
private, after is and after the begin of a body -- that means that I 
can't get the with inside the hidden part.