Re: pragma Import with 'Address clause

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

* Stephen Leake wrote:
> Lutz Donnerhacke <lutz@iks-jena.de> writes:
>> A common technique to reinterpret data is:
>>   a : AT;
>>   [...]
>>   b : BT;
>>   for b'Address use a'Address;
>>   pragma Import(Ada, b);
>>
>> Is the "pragma Import" really necessary? Of course, the ARM says, that
>> elaboration and definition of the imported object is externally defined. So
>> they are omitted from the Ada code itself.
>>
>> Assume BT is a record without any default expressions. Does this mean, the
>> pragma can be omitted from the source code?
>>
>> Background: Spark prohibits the use of Pragma Import on objects.
>
> I would hope Spark would prohibit the address clause as well!

Spark does handle the 'Address clause much more carefully than Ada95.
The following function is problematic in Spark for two reasons:
  - Calculating with external variables is undeterministic.
  - Imported variables might not conform the type restrictions.

function get_b return BT is
  b : BT;
  for b'Address use xxx;
begin
  return b+b;
end get_b;


> you are totally defeating the Ada type system!

No.