Le 09/04/2026 à 11:11, Kevin Chadwick via Dng a écrit :
>
> -------- 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.
>
    Eh, my knowledge of Ada is dated. I wrote a lot of wrappers of
Linux syscalls and IOCTLS. It was actually a delightfull job to create
clear, simple, and safe interfaces to some complicated, tricky, and
dangerous IOCTLS of the VME driver. But this was before the advent of SPARK.

--     Didier