/usr/lib/spark/current/spark-unsigned.shs is in spark 2012.0.deb-11build1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 | -------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
-------------------------------------------------------------------------------
-- --
-- SPARK.Unsigned --
-- --
-- Description --
-- This file is a "Shadow" specification for package SPARK.Unsigned. --
-- It must be kept in sync with the corresponding specification in --
-- spark-unsigned.ads --
-- --
-- This package presents a SPARK-compatible binding to the various Shift --
-- and Rotate functions that are supplied in Ada's package Interfaces. --
-- --
-- This package provides a de-overloading of these functions names to be --
-- compatible with SPARK. --
-- --
-- This package declares the functions using the same naming scheme as --
-- package Interfaces but with the suffix "_32", "_64" and so on --
-- appended to disambiguate each name. --
-- --
-- For efficiency, we also supply an Ada (not SPARK) version of this --
-- specification (in "spark-unsigned.ads") that must be submitted to your --
-- Ada compiler. This declares the new functions as renamings of the --
-- original versions, which are normally Intrinsic in most implementations --
-- of Ada. --
-- --
-- Language --
-- Specification : SPARK --
-- Private Part : N/A --
-- Body : Ada --
-- --
-- Runtime Requirements and Dependencies --
-- No Ada Runtime, assuming Shift_ and Rotate_ functions are --
-- Intrinsic on the target platform. --
-- --
-- Verification --
-- N/A --
-- --
-- Exceptions --
-- None --
-- --
-------------------------------------------------------------------------------
with Interfaces;
--# inherit Interfaces;
package SPARK.Unsigned
is
--------------------------------------------------------------------
-- Shorthand names for common unsigned types
--------------------------------------------------------------------
type U6 is mod 2**6;
type U7 is mod 2**7;
subtype Byte is Interfaces.Unsigned_8;
subtype U16 is Interfaces.Unsigned_16;
subtype U32 is Interfaces.Unsigned_32;
subtype U64 is Interfaces.Unsigned_64;
--------------------------------------------------------------------
-- Shift and Rotate functions
--
-- These functions supply a non-overloaded, and therefore
-- SPARK-compatible, declaration of the standard Shift and
-- Rotate functions for the standard modular types.
--
-- For the Examiner, these are declared as just plain function
-- declarations with no body.
--
-- For a compiler, a distinct version of this package specification
-- supplies these declarations as renamings of the (overloaded)
-- functions in package Interfaces, thus yielded the efficiency
-- of the Intrinsic functions.
--
-- The de-overloading scheme used is to replace function
-- XXX for type Unsigned_N with a function called
-- XXX_N which renames the original entity.
--------------------------------------------------------------------
-- Interfaces uses "Natural" for the Amount parameter of each
-- function below, but we choose to introduce a named subtype here
-- to ease RTC proof of calling units in SPARK.
subtype Shift_Count is Natural range 0 .. 64;
-- Rotate towards MSB
function Rotate_Left_8
(Value : Interfaces.Unsigned_8;
Amount : Shift_Count) return Interfaces.Unsigned_8;
-- Rotate towards LSB
function Rotate_Right_8
(Value : Interfaces.Unsigned_8;
Amount : Shift_Count) return Interfaces.Unsigned_8;
-- Shift towards MSB
function Shift_Left_8
(Value : Interfaces.Unsigned_8;
Amount : Shift_Count) return Interfaces.Unsigned_8;
-- Shift towards LSB
function Shift_Right_8
(Value : Interfaces.Unsigned_8;
Amount : Shift_Count) return Interfaces.Unsigned_8;
-- Arithmetic Shift towards LSB
function Shift_Right_Arithmetic_8
(Value : Interfaces.Unsigned_8;
Amount : Shift_Count) return Interfaces.Unsigned_8;
-- Rotate towards MSB
function Rotate_Left_16
(Value : Interfaces.Unsigned_16;
Amount : Shift_Count) return Interfaces.Unsigned_16;
-- Rotate towards LSB
function Rotate_Right_16
(Value : Interfaces.Unsigned_16;
Amount : Shift_Count) return Interfaces.Unsigned_16;
-- Shift towards MSB
function Shift_Left_16
(Value : Interfaces.Unsigned_16;
Amount : Shift_Count) return Interfaces.Unsigned_16;
-- Shift towards LSB
function Shift_Right_16
(Value : Interfaces.Unsigned_16;
Amount : Shift_Count) return Interfaces.Unsigned_16;
-- Arithmetic Shift towards LSB
function Shift_Right_Arithmetic_16
(Value : Interfaces.Unsigned_16;
Amount : Shift_Count) return Interfaces.Unsigned_16;
-- Rotate towards MSB
function Rotate_Left_32
(Value : Interfaces.Unsigned_32;
Amount : Shift_Count) return Interfaces.Unsigned_32;
-- Rotate towards LSB
function Rotate_Right_32
(Value : Interfaces.Unsigned_32;
Amount : Shift_Count) return Interfaces.Unsigned_32;
-- Shift towards MSB
function Shift_Left_32
(Value : Interfaces.Unsigned_32;
Amount : Shift_Count) return Interfaces.Unsigned_32;
-- Shift towards LSB
function Shift_Right_32
(Value : Interfaces.Unsigned_32;
Amount : Shift_Count) return Interfaces.Unsigned_32;
-- Arithmetic Shift towards LSB
function Shift_Right_Arithmetic_32
(Value : Interfaces.Unsigned_32;
Amount : Shift_Count) return Interfaces.Unsigned_32;
-- Rotate towards MSB
function Rotate_Left_64
(Value : Interfaces.Unsigned_64;
Amount : Shift_Count) return Interfaces.Unsigned_64;
-- Rotate towards LSB
function Rotate_Right_64
(Value : Interfaces.Unsigned_64;
Amount : Shift_Count) return Interfaces.Unsigned_64;
-- Shift towards MSB
function Shift_Left_64
(Value : Interfaces.Unsigned_64;
Amount : Shift_Count) return Interfaces.Unsigned_64;
-- Shift towards LSB
function Shift_Right_64
(Value : Interfaces.Unsigned_64;
Amount : Shift_Count) return Interfaces.Unsigned_64;
-- Arithmetic Shift towards LSB
function Shift_Right_Arithmetic_64
(Value : Interfaces.Unsigned_64;
Amount : Shift_Count) return Interfaces.Unsigned_64;
--------------------------------------------------------------------
-- Endian-ness conversion functions
--------------------------------------------------------------------
-- Returns W in Little-Endian format.
--
-- On a machine which is naturally Little-Endian, this function is a no-op.
-- On a big-endian machine, the 8 bytes of W are reversed.
function To_LittleEndian
(W : in Interfaces.Unsigned_64) return Interfaces.Unsigned_64;
pragma Inline (To_LittleEndian);
end SPARK.Unsigned;
|