From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,a691dc29968966aa
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-03-19 10:07:26 PST
Path: archiver1.google.com!postnews1.google.com!not-for-mail
From: rod.chapman@praxis-cs.co.uk (Rod Chapman)
Newsgroups: comp.lang.ada
Subject: Re: pragma Import with 'Address clause
Date: 19 Mar 2003 10:07:25 -0800
Organization: http://groups.google.com/
Message-ID: <cf2c6063.0303191007.2a1dd4b6@posting.google.com>
References: <slrnb7guml.nt.lutz@taranis.iks-jena.de>
NNTP-Posting-Host: 213.155.153.242
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1048097246 16132 127.0.0.1 (19 Mar 2003 18:07:26
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: 19 Mar 2003 18:07:26 GMT
Xref: archiver1.google.com comp.lang.ada:35520
Date: 2003-03-19T18:07:26+00:00
List-Id: <comp.lang.ada>

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.