Re: pragma Import with 'Address clause

[rod.chapman@praxis-cs.co.uk (Rod Chapman)]

Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb7guml.nt.lutz@taranis.iks-jena.de>...
> A common technique to reinterpret data is:
>   a : AT;
>   [...]
>   b : BT;
>   for b'Address use a'Address;
>   pragma Import(Ada, b);

This is really bad style, especially in SPARK.  You are deliberately
creating an aliasing that the Examiner can't detect, so this will
cause great confusion for the information-flow analysis of your program.

A better way might be to use a hidden, in-lined instantiation of
Unchecked_Conversion, thus:

   function AT_To_BT (A : in AT) return BT
   is
      --# hide AT_To_BT;
      function C is new Unchecked_Conversion (AT, BT);
   begin
      return C(A);
   end AT_To_BT;
   pragma Inline (AT_To_BT);

Of course, a good compiler will generate absolutely no code for this
at all, which is good news.  You can then create a BT-typed "view" onto
A where and when required without having to introduce aliasing.


If A and B are both library level objects, and the address of A is static,
then you can create two views onto the same area of memory, and use SPARK's
data refinement mechanism to pretend to the outside world that it's
only 1 object really.  Something like:

 package ROM
 --# own Contents;
 --# initializes Contents; -- probably...
 is
    ...
 end ROM;

 package body ROM
 --# own Contents is Raw_View, Typed_View;
 is
   Typed_View : AT;
   for A'Address use Wibble;

   Raw_View   : BT;
   for B'Address use Wibble;

   ...

 end ROM;

You still have to think hard here about which object gets
initialized and when.

This kind of trick is just about justifiable when you want two views of
something like a ROM - one "raw" (Array-of-words or something) view for
checksumming, and one strongly-typed view for strucured access.

Oh - there's one other case where we've done this trick - for I/O
devices that overload a single address port with both a write-only control
register and a read-only status register.  For those things, we simply
declare 2 library level variables which have an identical address
clause, since in this case, we really would prefer to treat them
as distinct objects anyway... :-)

 - Rod, SPARK Team.