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 14:29:01 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 14:29:01 -0800
Organization: http://groups.google.com/
Message-ID: <cf2c6063.0303191429.53f2fc13@posting.google.com>
References: <slrnb7guml.nt.lutz@taranis.iks-jena.de> <uof47z4dg.fsf@nasa.gov>
 <slrnb7h93l.nt.lutz@taranis.iks-jena.de>
NNTP-Posting-Host: 213.152.53.239
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1048112941 30195 127.0.0.1 (19 Mar 2003 22:29:01
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: 19 Mar 2003 22:29:01 GMT
Xref: archiver1.google.com comp.lang.ada:35531
Date: 2003-03-19T22:29:01+00:00
List-Id: <comp.lang.ada>

Lutz Donnerhacke <lutz@iks-jena.de> wrote in message news:<slrnb7h93l.nt.lutz@taranis.iks-jena.de>...

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

Again, this is really bad style.  Giving Address clauses to local
variable is dubious at best and also defeats SPARK's information flow
model in various ways.  Try something like this:

package Simple_Port
--# own in B; -- volatile "in" mode external variable
is
   function Get_B return BT;
   --# global in B;
end Simple_Port;

package body Simple_Port
is
   B : BT;
   for B'Address use ...; -- external variable with Address clause;
   pragma Volatile (B);   -- probably needed, so better safe than sorry...

   function Get_B return BT
   is
      Raw_B, Result : BT;
   begin
      Raw_B := B; -- simple assignment OK.
      if Raw_B'Valid then
         Result := Raw_B + Raw_B; -- or whatever...
      else
         Result := BT'First; -- or some other safe value
      end if;
      return Result;
   end Get_B;
end Simple_Port;

This is 100% SPARK and freedom from exceptions and invalid values
can be proven.  Note that 

1) The Examiner DOESN'T assert that "Local_B in BT" directly following
the first assignment, since the Examiner is clever enough to know
that something coming from a memory-mapped location might not have a
valid representation.

2) 'Valid can be used to re-establish validity.

3) In this context, an assignment such as

    Raw_B := B + B;

is illegal in SPARK, since B is known to be Volatile, and therefore
such expressions are susceptible to undesirable evaluation
order dependencies.

We thought about these issues very hard indeed when designing the
external-variable and volatility model in SPARK! :-)

 - Rod, SPARK Team.