Re: [Spark] Using defered constants

[Lutz Donnerhacke <lutz@iks-jena.de>]

* Hyman Rosen wrote:
> Lutz Donnerhacke wrote:
>> It's an example. I need an access type there.
>
> SPARK doesn't have access types, I hear. I'm told that this is so that
> the correctness of the code is easier to prove, and that code that needs
> access types should be written in plain Ada.

Your ears are working fine. I can use a sufficient Integer type, too, but
playing with such brain damages is subject of the other side of the Spark
border. I only have to fullfill the API constraints. You may suggest to not
use Spark everytime, an enviroment is accessed, but this is clearly not an
option, because it requires the whole programm to be written in Ada not
Spark consequently.

OTOH my question does not deal with this topic, but with a Spark strangeness.
So please keep the ball in the field. Thank you.

PS: I use Spark to shrink the executable's size: By proofing the absence of
run time errors, I can drop the run time checks completely. In order to not
introduce those error handlers again in the patch code written in Ada, the
Ada parts has to be as simple as possible. That's why the mix is free from
run time errors despite I use glue code! (Otherwise the linker will complain.)