-------- Original Message --------

>     The Ada program, needing to interface to the C library, the wrappers for the
> C functions would need to use the package Ada.Unchecked_Conversions, which
> certainly does not pass SPARK controls. So that there remains essentially
> nothing for SPARK.

People have a bee in their bonnet about Unchecked_Conversion. I use it quite
often and I was amased by the amount of checks on Unchecked_Conversion in SPARK.
It really shouldn't have been named unchecked but there are a few functions that
were renamed from unsafe as that wording was deemed overly cautious. It is
absolutely supported by SPARK today at least, as is using addresses. I'm sure
gnat prove will error on certain use cases in the use of both as there are on
volatile variables to avoid any potential side affects.

-- 
All the best,
             Kevin Chadwick