Re: pragma Import with 'Address clause

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

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.