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

[roderick.chapman@googlemail.com]

On Mar 26, 3:18 pm, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:

> My outdated copy of the SPARK book describe a Spark I/O package.
> Also, package Interfaces does not pass, so if that is an important
> base for run-time support ...

You'll need what we call a "shadow" package specification that
offers a SPARK-friendly (i.e. legal SPARK) version of an
otherwise non-SPARK package.

You then use the Examiner's "index file" mechamisn to
make the Examiner read in the shadow specification, while
your compiler, of course, uses the "real" Ada version.

More info in the book in section 13.1.

Ada.Strings.Unbounded is likely to be very hard
to shadow, though, since it is full on non-SPARK
things like String_Access and returning String
from a function, which is beyond the run-time
library profile support by SPARK.


Same goes for Interfaces - most of it is legal SPARK,
but (in GNAT anyway) the overloading of the various
Shift_ and Rotate_ functions is not legal in SPARK.

If you really need access to those things, then
create a "thick binding" that "un-overloads" those
functions in a distinct package.   SPARK_IO
is an example of this - it offers a thick-binding
to the underlying Ada.Text_IO package.

 - Rod Chapman, SPARK Team