Re: SPARK left/right shift.

[Rod Chapman <roderick.chapman@googlemail.com>]

OK - it's done as follows.  We create a SPARK "shadow" specification
of
package Interfaces and a new package SPARK_Interfaces for which there
is an Ada version (for the compiler) and a shadow version (for the
Examiner.)

1) Add the following to your Examiner index file:

interfaces spec is in interfaces.shs
spark_interfaces spec is in spark_interfaces.shs

2) interfaces.shs contains

package Interfaces
is
   type Unsigned_32 is mod 2**32;
   -- ... and similarly for other Unsigned_XX types
end Interfaces;

3) spark_interfaces.shs contains

with Interfaces;
--# inherit Interfaces;
package SPARK_Interfaces
is
   function Rotate_Left_32
     (Value  : Interfaces.Unsigned_32;
      Amount : Natural) return Interfaces.Unsigned_32;

end SPARK_Interfaces;

(note this removes the overloading, and declares the function so it's
legal SPARK)

4) spark_interfaces.ads contains

with Interfaces;
package SPARK_Interfaces
is
   function Rotate_Left_32
     (Value  : Interfaces.Unsigned_32;
      Amount : Natural) return Interfaces.Unsigned_32 renames
Interfaces.Rotate_Left;

end SPARK_Interfaces;

(note this _renames_ the original function from Interfaces, so you
still
get the efficiency of the Intrinsic version.)

OK?
 - Rod