-- --
------------------------------------------------------------------------------
+-- This unit implements dynamic priority support for Ada tasking as defined
+-- in ARM D.5.1. It allows a tasks priority to be changed after the task has
+-- been created.
+
with System;
with Ada.Task_Identification;
-- --
------------------------------------------------------------------------------
+-- Package ``Ada.Real_Time`` provides basic definitions and operations related
+-- to the types defined ``Time`` and ``Time_Span`` as defined by ARM D.8. The
+-- types ``Time`` and ``Time_Span`` are implemented by the ``Duration`` type.
+--
+-- This software layer provides the Ada abstraction for time handling and
+-- delays, using the services provided by lower layers.
+
with System.Task_Primitives.Operations;
pragma Elaborate_All (System.Task_Primitives.Operations);
-- --
------------------------------------------------------------------------------
+-- This package implements functionality defined by ARM D.10.1 to
+-- synchronously release multiple blocked tasks after the number
+-- of blocked tasks has reached a specified threshold.
+
package Ada.Synchronous_Barriers with SPARK_Mode => Off is
pragma Preelaborate (Synchronous_Barriers);
-- --
------------------------------------------------------------------------------
+-- This package implements Ada task identification as defined by ARM C.7.1.
+
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised.
-- This is enforced by setting the corresponding assertion policy to Ignore.
-- intended to be used in a restricted run time.
-- This package represents the high level tasking interface used by the
--- compiler to expand Ada 95 tasking constructs into simpler run time calls
--- (aka GNARLI, GNU Ada Run-time Library Interface)
+-- compiler to expand Ada 95 tasking constructs into simpler run-time calls.
--- Note: the compiler generates direct calls to this interface, via Rtsfind.
--- Any changes to this interface may require corresponding compiler changes
--- in exp_ch9.adb and possibly exp_ch7.adb
+-- The compiler generates direct calls to this interface, via Rtsfind. Any
+-- changes to this interface may require corresponding compiler changes in
+-- exp_ch9.adb and possibly exp_ch7.adb.
-- The restricted GNARLI is also composed of System.Protected_Objects and
-- System.Protected_Objects.Single_Entry
------------------------------------------------------------------------------
-- This package contains the definitions and routines associated with the
--- implementation and use of the Task_Info pragma. It is specialized
+-- implementation and use of the ``Task_Info`` pragma. It is specialized
-- appropriately for targets that make use of this pragma.
--- Note: the compiler generates direct calls to this interface, via Rtsfind.
--- Any changes to this interface may require corresponding compiler changes.
+-- The compiler generates direct calls to this interface, via Rtsfind. Any
+-- changes to this interface may require corresponding compiler changes.
-- The functionality in this unit is now provided by the predefined package
-- System.Multiprocessors and the CPU aspect. This package is obsolescent.
-- --
------------------------------------------------------------------------------
--- This is a POSIX-like version of this package
+-- This is the POSIX compliant systems implementation
+
+-- This package and its children provide a binding to the underlying platform.
+-- The base types are defined here while the functional implementations
+-- are in ``Task_Primitives.Operations``.
-- Note: this file can only be used for POSIX compliant systems
-- --
------------------------------------------------------------------------------
+-- This package provides primitives used for protected objects on
+-- multiprocessor systems.
+
package System.Tasking.Protected_Objects.Multiprocessors is
procedure Served (Entry_Call : Entry_Call_Link);
-- --
------------------------------------------------------------------------------
+-- This package provides the assertion feature defined by ARM 11.4.2
+
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised when calling Assert.
-- This is enforced by setting the corresponding assertion policy to Ignore.
-- --
------------------------------------------------------------------------------
+-- This language package providing support for obtaining the values of its
+-- command line arguments and to set the exit status of the program as defined
+-- by ARM A.15.
+
package Ada.Command_Line is
pragma Preelaborate;
-- --
------------------------------------------------------------------------------
--- This unit is provided as a replacement for the standard unit
--- Ada.Numerics.Big_Numbers.Big_Integers when only proof with SPARK is
--- intended. It cannot be used for execution, as all subprograms are marked
--- imported with no definition.
+-- This package provides a reduced and non-executable implementation of the
+-- ARM A.5.6 defined ``Ada.Numerics.Big_Numbers.Big_Integers`` for use in
+-- SPARK proofs in the runtime. As it is only intended for SPARK proofs, this
+-- package is marked as a Ghost package and consequently does not have a
+-- runtime footprint.
-- Contrary to Ada.Numerics.Big_Numbers.Big_Integers, this unit does not
-- depend on System or Ada.Finalization, which makes it more convenient for
--- use in run-time units.
+-- use in run-time units. Note, since it is a ghost unit, all subprograms are
+-- marked as imported.
-- Ghost code in this unit is meant for analysis only, not for run-time
-- checking. This is enforced by setting the assertion policy to Ignore.
type Big_Integer is private
with Integer_Literal => From_Universal_Image;
+ -- Private type that holds the integer value
function Is_Valid (Arg : Big_Integer) return Boolean
with
Import,
Global => null;
+ -- Return whether a passed big integer is valid
subtype Valid_Big_Integer is Big_Integer
with Dynamic_Predicate => Is_Valid (Valid_Big_Integer),
Predicate_Failure => raise Program_Error;
+ -- Holds a valid Big_Integer
+ -- Comparison operators defined for valid Big_Integer values
function "=" (L, R : Valid_Big_Integer) return Boolean with
Import,
Global => null;
with
Import,
Global => null;
+ -- Create a Big_Integer from an Integer value
subtype Big_Positive is Big_Integer
with Dynamic_Predicate =>
(if Is_Valid (Big_Positive)
then Big_Positive > To_Big_Integer (0)),
Predicate_Failure => raise Constraint_Error;
+ -- Positive subtype of Big_Integers, analogous to Positive and Integer
subtype Big_Natural is Big_Integer
with Dynamic_Predicate =>
(if Is_Valid (Big_Natural)
then Big_Natural >= To_Big_Integer (0)),
Predicate_Failure => raise Constraint_Error;
+ -- Natural subtype of Big_Integers, analogous to Natural and Integer
function In_Range
(Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean
with
Import,
Global => null;
+ -- Check whether Arg is in the range Low .. High
function To_Integer (Arg : Valid_Big_Integer) return Integer
with
High => To_Big_Integer (Integer'Last))
or else raise Constraint_Error,
Global => null;
+ -- Convert a valid Big_Integer into an Integer
generic
type Int is range <>;
package Signed_Conversions is
+ -- Generic package to implement conversion functions for
+ -- arbitrary ranged types.
function To_Big_Integer (Arg : Int) return Valid_Big_Integer
with
Global => null;
+ -- Convert a ranged type into a valid Big_Integer
function From_Big_Integer (Arg : Valid_Big_Integer) return Int
with
High => To_Big_Integer (Int'Last))
or else raise Constraint_Error,
Global => null;
+ -- Convert a valid Big_Integer into a ranged type
end Signed_Conversions;
generic
type Int is mod <>;
package Unsigned_Conversions is
+ -- Generic package to implement conversion functions for
+ -- arbitrary modular types.
function To_Big_Integer (Arg : Int) return Valid_Big_Integer
with
Global => null;
+ -- Convert a modular type into a valid Big_Integer
function From_Big_Integer (Arg : Valid_Big_Integer) return Int
with
High => To_Big_Integer (Int'Last))
or else raise Constraint_Error,
Global => null;
+ -- Convert a valid Big_Integer into a modular type
end Unsigned_Conversions;
with
Import,
Global => null;
+ -- Create a valid Big_Integer from a String
function From_Universal_Image (Arg : String) return Valid_Big_Integer
renames From_String;
+ -- Mathematical operators defined for valid Big_Integer values
function "+" (L : Valid_Big_Integer) return Valid_Big_Integer
with
Import,
Pre => (L /= To_Big_Integer (0) and R /= To_Big_Integer (0))
or else raise Constraint_Error,
Global => null;
+ -- Calculate the greatest common divisor for two Big_Integer values
private
pragma SPARK_Mode (Off);
type Big_Integer is null record;
+ -- Solely consists of Ghost code
end Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
-- --
------------------------------------------------------------------------------
+-- This package defines the base types used for big numbers in Ada as defined
+-- by ARM A.5.5.
+
package Ada.Numerics.Big_Numbers
with Pure
is
subtype Field is Integer range 0 .. 255;
+ -- The width of a big number. This is used when converting
+ -- the internal representation into a string.
+
subtype Number_Base is Integer range 2 .. 16;
+ -- The base of a big number. This is used when converting
+ -- the internal representation into a string.
+
end Ada.Numerics.Big_Numbers;
-- --
------------------------------------------------------------------------------
+-- This package is the top of the Ada.Numerics hierarchy as defined by ARM
+-- A.5. It provides an exception used by all children and basic mathematical
+-- constants.
+
package Ada.Numerics is
pragma Pure;
Argument_Error : exception;
+ -- The Argument_Error exception is raised whenever an invalid
+ -- value has passed as an argument to the subprograms defined
+ -- this this package and its children.
Pi : constant :=
3.14159_26535_89793_23846_26433_83279_50288_41971_69399_37511;
-
- -- ["03C0"] : constant := Pi;
- -- This is the Greek letter Pi (for Ada 2005 AI-388). Note that it is
- -- conforming to have this constant present even in Ada 95 mode, as there
- -- is no way for a normal mode Ada 95 program to reference this identifier.
- -- ???This is removed for now, because nobody uses it, and it causes
- -- trouble for tools other than the compiler. If people want to use the
- -- Greek letter in their programs, they can easily define it themselves.
+ -- The mathematical constant Pi
e : constant :=
2.71828_18284_59045_23536_02874_71352_66249_77572_47093_69996;
+ -- The mathematical constant e
end Ada.Numerics;
-- --
------------------------------------------------------------------------------
+-- This package is defined by ARM 13.9 to implement unchecked type
+-- conversions.
+
generic
type Source (<>) is limited private;
type Target (<>) is limited private;
function Ada.Unchecked_Conversion (S : Source) return Target;
+-- Returns the bit pattern of ``S`` for type ``Target``
pragma No_Elaboration_Code_All (Ada.Unchecked_Conversion);
pragma Pure (Ada.Unchecked_Conversion);
-- --
------------------------------------------------------------------------------
+-- This package is defined by ARM 13.11.2 to implement unchecked storage
+-- deallocation of an object designated by a value of an access type.
+
generic
type Object (<>) is limited private;
type Name is access Object;
Depends => (X => null, -- X on exit does not depend on its input value
null => X), -- X's input value has no effect
Post => X = null; -- X's output value is null
+-- Deallocate object denoted by X, and set X to null.
+
pragma Preelaborate (Unchecked_Deallocation);
pragma Import (Intrinsic, Ada.Unchecked_Deallocation);
-- --
------------------------------------------------------------------------------
+-- This is an empty package at the top of the Ada package hierarchy
+
package Ada is
pragma No_Elaboration_Code_All;
pragma Pure;
function Image (S : String) return String;
-- Returns a string image of S, obtained by prepending and appending
-- quote (") characters and doubling any quote characters in the string.
- -- The maximum length of the result is thus 2 ** S'Length + 2.
+ -- The maximum length of the result is thus 2 * S'Length + 2.
function Image (A : System.Address) return Image_String;
-- Returns a string of the form 16#hhhh_hhhh# for 32-bit addresses
-- --
------------------------------------------------------------------------------
--- This package provides facilities for obtaining information on secondary
--- stack usage. See System.Secondary_Stack for documentation.
+-- This package provides a public interface to the internal package
+-- ``System.Secondary_Stack``. It allows users to query the current high water
+-- mark of the secondary stack, the stack used to return unconstrained types.
with System.Secondary_Stack;
function SS_Get_Max return Long_Long_Integer
renames System.Secondary_Stack.SS_Get_Max;
+ -- Return the high water mark of the secondary stack for the current
+ -- secondary stack in bytes.
end GNAT.Secondary_Stack_Info;
Import, Convention => Intrinsic;
-- Return the name of the current file, not including the path information.
-- The result is considered to be a static string constant.
+ --
+ -- This function is an intrinsic, implemented by the compiler.
function Line return Positive with
Import, Convention => Intrinsic;
-- Return the current input line number. The result is considered to be a
-- static expression.
+ --
+ -- This function is an intrinsic, implemented by the compiler.
function Source_Location return String with
Volatile_Function,
-- additional suffixes of the same form are appended after the separating
-- string " instantiated at ". The result is considered to be a static
-- string constant.
+ --
+ -- This function is an intrinsic, implemented by the compiler.
function Enclosing_Entity return String with
Volatile_Function,
-- the string returned will be the name of the instance, not the generic
-- package itself. This is useful in identifying and logging information
-- from within generic templates.
+ --
+ -- This function is an intrinsic, implemented by the compiler.
function Compilation_ISO_Date return String with
Volatile_Function,
Global => Source_Code_Information,
Import, Convention => Intrinsic;
-- Returns date of compilation as a static string "yyyy-mm-dd".
+ --
+ -- This function is an intrinsic, implemented by the compiler.
function Compilation_Date return String with
Volatile_Function,
Import, Convention => Intrinsic;
-- Returns date of compilation as a static string "mmm dd yyyy". This is
-- in local time form, and is exactly compatible with C macro __DATE__.
+ --
+ -- This function is an intrinsic, implemented by the compiler.
function Compilation_Time return String with
Volatile_Function,
Import, Convention => Intrinsic;
-- Returns GMT time of compilation as a static string "hh:mm:ss". This is
-- in local time form, and is exactly compatible with C macro __TIME__.
+ --
+ -- This function is an intrinsic, implemented by the compiler.
end GNAT.Source_Info;
-- --
------------------------------------------------------------------------------
--- This is the parent package for a library of useful units provided with GNAT
+-- This is parent package of the GNAT package hierarchy, a collection of
+-- useful packages provided with GNAT. It contains types and exception
+-- definitions that a commonly used by GNAT child packages. As definitions
+-- these do not appear in the runtime code if they are not used.
--- Note: this unit is used during bootstrap, see ADA_GENERATED_FILES in
+-- This unit is used during bootstrap, see ADA_GENERATED_FILES in
-- gcc-interface/Make-lang.in for details on the constraints.
package GNAT is
-- --
------------------------------------------------------------------------------
--- This package contains additional C-related definitions, intended for use
--- with either manually or automatically generated bindings to C libraries.
+-- This package contains additional C type definitions that are not defined
+-- by ARM B.2 and is intended for use with manual or automatically generated
+-- bindings to C libraries. Specifically, it defines types for bitfields,
+-- C void types, incomplete and unknown structs and classes, C bool, 64-bit
+-- and 128-bit types, and 128-bit floating-point types.
with System;
type incomplete_class_def_ptr is access incomplete_class_def;
for incomplete_class_def_ptr'Storage_Size use 0;
- -- C bool
-
subtype bool is Interfaces.C.C_bool;
+ -- C bool
-- 64-bit integer types
subtype long_long is Interfaces.C.long_long;
subtype unsigned_long_long is Interfaces.C.unsigned_long_long;
- -- 128-bit integer type available on 64-bit platforms:
- -- typedef int signed_128 __attribute__ ((mode (TI)));
-
type Signed_128 is record
low, high : unsigned_long_long;
end record;
+ -- 128-bit integer type available on 64-bit platforms:
+ -- typedef int signed_128 __attribute__ ((mode (TI)));
+
pragma Convention (C_Pass_By_Copy, Signed_128);
for Signed_128'Alignment use unsigned_long_long'Alignment * 2;
- -- 128-bit floating-point type available on x86:
- -- typedef float float_128 __attribute__ ((mode (TF)));
-
type Float_128 is record
low, high : unsigned_long_long;
end record;
+ -- 128-bit floating-point type available on x86:
+ -- typedef float float_128 __attribute__ ((mode (TF)));
+
pragma Convention (C_Pass_By_Copy, Float_128);
for Float_128'Alignment use unsigned_long_long'Alignment * 2;
- -- 128-bit complex floating-point type available on x86:
- -- typedef _Complex float cfloat_128 __attribute__ ((mode (TC)));
-
type CFloat_128 is record
re, im : Float_128;
end record;
+ -- 128-bit complex floating-point type available on x86:
+ -- typedef _Complex float cfloat_128 __attribute__ ((mode (TC)));
+
pragma Convention (C_Pass_By_Copy, CFloat_128);
-- Types for bitfields
-- --
------------------------------------------------------------------------------
--- This package contains additional C-related definitions, intended for use
--- with either manually or automatically generated bindings to C libraries.
+-- This package contains additional C type definitions that are not defined
+-- by ARM B.2 and is intended for use with manual or automatically generated
+-- bindings to C libraries. Specifically, it defines types for bitfields,
+-- C void types, incomplete and unknown structs and classes, C bool, 64-bit
+-- and 128-bit types, and 128-bit floating-point types.
with System;
type incomplete_class_def_ptr is access incomplete_class_def;
for incomplete_class_def_ptr'Storage_Size use 0;
- -- C bool
-
subtype bool is Interfaces.C.C_bool;
+ -- C bool
-- 64-bit integer types
subtype long_long is Interfaces.C.long_long;
subtype unsigned_long_long is Interfaces.C.unsigned_long_long;
- -- 128-bit floating-point type available on x86:
- -- typedef float float_128 __attribute__ ((mode (TF)));
-
type Float_128 is record
low, high : unsigned_long_long;
end record;
+ -- 128-bit floating-point type available on x86:
+ -- typedef float float_128 __attribute__ ((mode (TF)));
+
pragma Convention (C_Pass_By_Copy, Float_128);
for Float_128'Alignment use unsigned_long_long'Alignment * 2;
- -- 128-bit complex floating-point type available on x86:
- -- typedef _Complex float cfloat_128 __attribute__ ((mode (TC)));
-
type CFloat_128 is record
re, im : Float_128;
end record;
+ -- 128-bit complex floating-point type available on x86:
+ -- typedef _Complex float cfloat_128 __attribute__ ((mode (TC)));
+
pragma Convention (C_Pass_By_Copy, CFloat_128);
-- Types for bitfields
-- since arbitrary addresses can be converted, and it is quite likely that
-- this type will in fact be used for aliasing values of other types.
+ -- Convert between chars_ptr and a C pointer
function To_chars_ptr is
new Ada.Unchecked_Conversion (System.Parameters.C_Address, chars_ptr);
function Memory_Alloc (Size : size_t) return chars_ptr;
pragma Import (C, Memory_Alloc, System.Parameters.C_Malloc_Linkname);
+ -- Allocate a chunk of memory on the heap
procedure Memory_Free (Address : chars_ptr);
pragma Import (C, Memory_Free, "__gnat_free");
+ -- Deallocate a previously allocated chunk of memory from the heap. On
+ -- runtimes that do not allow deallocation this is a no-op.
---------
-- "+" --
-- --
------------------------------------------------------------------------------
+-- This package declares types and subprograms that allow the allocation,
+-- reference, update and deallocation of C-style strings, as defined by
+-- ARM B.3.1.
+
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- setting the corresponding assertion policy to Ignore. These preconditions
is
pragma Preelaborate;
+ -- Definitions for C character arrays
type char_array_access is access all char_array;
for char_array_access'Size use System.Parameters.ptr_bits;
type chars_ptr_array is array (size_t range <>) of aliased chars_ptr;
Null_Ptr : constant chars_ptr;
+ -- Null value for private type chars_ptr
function To_Chars_Ptr
(Item : char_array_access;
Nul_Check : Boolean := False) return chars_ptr
with
SPARK_Mode => Off; -- To_Chars_Ptr'Result is aliased with Item
+ -- Extract raw chars_ptr from char_array access type
function New_Char_Array (Chars : char_array) return chars_ptr with
Volatile_Function,
Post => New_Char_Array'Result /= Null_Ptr,
Global => (Input => C_Memory);
+ -- Copy the contents of Chars into a newly allocated chars_ptr
function New_String (Str : String) return chars_ptr with
Volatile_Function,
Post => New_String'Result /= Null_Ptr,
Global => (Input => C_Memory);
+ -- Copy the contents of Str into a newly allocated chars_ptr
procedure Free (Item : in out chars_ptr) with
SPARK_Mode => Off;
-- When deallocation is prohibited (eg: cert runtimes) this routine
- -- will raise Program_Error
+ -- will raise Program_Error.
Dereference_Error : exception;
+ -- This exception is raised when a subprogram of this unit tries to
+ -- dereference a chars_ptr with the value Null_Ptr.
+ -- The Value functions copy the contents of a chars_ptr object
+ -- into a char_array/String.
function Value (Item : chars_ptr) return char_array with
Pre => Item /= Null_Ptr,
Global => (Input => C_Memory);
function Strlen (Item : chars_ptr) return size_t with
Pre => Item /= Null_Ptr,
Global => (Input => C_Memory);
+ -- Return the length of a string contained in a chars_ptr
+ -- Update the contents of a chars_ptr with a char_array/String. If the
+ -- update exceeds the original length of the chars_ptr the Update_Error
+ -- exception is raised.
procedure Update
(Item : chars_ptr;
Offset : size_t;
-- This is the runtime version of this unit (not used during GNAT build)
+-- ``Interfaces`` is the parent of several library packages that declare types
+-- and other entities useful for interfacing to foreign languages as defined
+-- by ARM B.2.
+--
+-- It defines signed and modular integer types of 8, 16, 32, 64 and 128 bits.
+-- For each such modular type, shifting and rotating intrinsic subprograms
+-- are specified. There is also the definition of IEEE 754 floating point
+-- types (``IEEE_Float_32``, ``IEEE_Float_64``, and ``IEEE_Extended_Float``).
+
package Interfaces with
Always_Terminates
is
pragma No_Elaboration_Code_All;
pragma Pure;
+ pragma Implementation_Defined;
-- All identifiers in this unit are implementation defined
- pragma Implementation_Defined;
+ -- Definitions of 8, 16, 24, 32, 64 and 128 bit signed and unsigned integer
+ -- types.
type Integer_8 is range -2 ** 7 .. 2 ** 7 - 1;
for Integer_8'Size use 8;
type Integer_64 is new Long_Long_Integer;
for Integer_64'Size use 64;
- -- Note: we use Long_Long_Integer'First instead of -2 ** 63 to allow this
- -- unit to compile when using custom target configuration files where the
- -- maximum integer is 32 bits. This is useful for static analysis tools
- -- such as SPARK or CodePeer. In the normal case Long_Long_Integer is
- -- always 64-bits so we get the desired 64-bit type.
+ -- We use Long_Long_Integer'First instead of -2 ** 63 to allow this unit to
+ -- compile when using custom target configuration files where the maximum
+ -- integer is 32 bits. This is useful for static analysis tools such as
+ -- SPARK or CodePeer. In the normal case Long_Long_Integer is 64-bits so we
+ -- get the desired 64-bit type.
type Integer_128 is new Long_Long_Long_Integer;
- -- Note: we use Long_Long_Long_Integer instead of literal bounds to allow
- -- this unit to be compiled with compilers not supporting 128-bit integers.
+ -- We use Long_Long_Long_Integer instead of literal bounds to allow this
+ -- unit to be compiled with compilers not supporting 128-bit integers.
-- We do not put a confirming size clause of 128 bits for the same reason.
type Unsigned_8 is mod 2 ** 8;
type Unsigned_128 is mod 2 ** Long_Long_Long_Integer'Size;
-- See comment on Integer_128 above
+ -- Compiler intrinsics implemented by the compiler
+
function Shift_Left
(Value : Unsigned_8;
Amount : Natural) return Unsigned_8
type IEEE_Float_64 is digits 15;
for IEEE_Float_64'Size use 64;
- -- If there is an IEEE extended float available on the machine, we assume
- -- that it is available as Long_Long_Float.
-
+ -- If there is an IEEE extended float available on the machine, we
+ -- assume that it is available as Long_Long_Float.
+ --
-- Note: it is harmless, and explicitly permitted, to include additional
-- types in interfaces, so it is not wrong to have IEEE_Extended_Float
-- defined even if the extended format is not available.
-- --
------------------------------------------------------------------------------
+-- This package is a renaming of :ref:`system.machine_code`
+
with System.Machine_Code;
package Machine_Code renames System.Machine_Code;
-- This package provides arithmetic and logical operations on type Address.
-- It is intended for use by other packages in the System hierarchy. For
--- applications requiring this capability, see System.Storage_Elements or
--- the operations introduced in System.Aux_DEC;
-
--- The reason we need this package is that arithmetic operations may not
--- be available in the case where type Address is non-private and the
--- operations have been made abstract in the spec of System (to avoid
--- inappropriate use by applications programs). In addition, the logical
--- operations may not be available if type Address is a signed integer.
+-- applications requiring this capability, use `System.Storage_Elements`
+-- instead.
+--
+-- The reason for this package is that arithmetic operations may not be
+-- available in the case where type Address is non-private and the operations
+-- have been made abstract in the spec of System (to avoid inappropriate use
+-- by applications programs). In addition, the logical operations may not be
+-- available if type Address is a signed integer.
package System.Address_Operations is
pragma Pure;
-- a modular type with the same length as Address, i.e. they provide
-- twos complement wrap around arithmetic treating the address value
-- as an unsigned value, with no overflow checking.
-
+ --
-- Note that we do not use the infix names for these operations to
-- avoid problems with ambiguities coming from declarations in package
-- Standard (which may or may not be visible depending on the exact
-- form of the declaration of type System.Address).
-
+ --
-- For addition, subtraction, and multiplication, the effect of overflow
-- is 2's complement wrapping (as though the type Address were unsigned).
-
+ --
-- For division and modulus operations, the caller is responsible for
-- ensuring that the Right argument is non-zero, and the effect of the
-- call is not specified if a zero argument is passed.
function AddA (Left, Right : Address) return Address;
+ -- Computes the sum of ``Left`` and ``Right``
function SubA (Left, Right : Address) return Address;
+ -- Computes the difference between ``Left`` and ``Right``
function MulA (Left, Right : Address) return Address;
+ -- Computes the product of ``Left`` and ``Right``
function DivA (Left, Right : Address) return Address;
+ -- Computes the quotient of ``Left`` and ``Right``
function ModA (Left, Right : Address) return Address;
+ -- Computes the modulus of ``Left`` and ``Right``
-- The semantics of the logical operations are those that apply to
-- a modular type with the same length as Address, i.e. they provide
-- bit if Address is a signed integer type).
function AndA (Left, Right : Address) return Address;
+ -- Computes the bit-wise 'and' mask of ``Left`` and ``Right``
function OrA (Left, Right : Address) return Address;
+ -- Computes the bit-wise 'or' mask of ``Left`` and ``Right``
pragma Inline_Always (AddA);
pragma Inline_Always (SubA);
-- --
------------------------------------------------------------------------------
--- This package provides software routines for doing arithmetic on "double"
--- signed integer values in cases where either overflow checking is required,
--- or intermediate results are longer than the result type.
+-- This generic package provides software routines for doing arithmetic on
+-- double word signed integer values in cases where either overflow checking
+-- is required, or intermediate results are longer than the result type.
with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
with
Pre => In_Double_Int_Range (Big (X) + Big (Y)),
Post => Add_With_Ovflo_Check'Result = X + Y;
- -- Raises Constraint_Error if sum of operands overflows Double_Int,
- -- otherwise returns the signed integer sum.
+ -- Raises Constraint_Error if sum of operands overflows 64 bits,
+ -- otherwise returns the 64-bit signed integer sum.
+ --
+ -- The sum of ``X`` and ``Y`` is first computed using wrap-around
+ -- semantics.
+ --
+ -- If the sign of ``X`` and ``Y`` are opposed, no overflow is possible and
+ -- the result is correct.
+ --
+ -- Otherwise, ``X`` and ``Y`` have the same sign; if the sign of the result
+ -- is not identical to ``X`` (or ``Y``), then an overflow occurred and
+ -- the exception *Constraint_Error* is raised; otherwise the result is
+ -- correct.
function Subtract_With_Ovflo_Check (X, Y : Double_Int) return Double_Int
with
Pre => In_Double_Int_Range (Big (X) - Big (Y)),
Post => Subtract_With_Ovflo_Check'Result = X - Y;
- -- Raises Constraint_Error if difference of operands overflows Double_Int,
- -- otherwise returns the signed integer difference.
+ -- Raises Constraint_Error if difference of operands overflows 64
+ -- bits, otherwise returns the 64-bit signed integer difference.
+ --
+ -- The logic of the implementation is reversed from *Add_With_Ovflo_Check*:
+ -- if ``X`` and ``Y`` have the same sign, no overflow is checked, otherwise
+ -- a sign of the result is compared with the sign of ``X`` to check for
+ -- overflow.
function Multiply_With_Ovflo_Check (X, Y : Double_Int) return Double_Int
with
Pre => In_Double_Int_Range (Big (X) * Big (Y)),
Post => Multiply_With_Ovflo_Check'Result = X * Y;
pragma Convention (C, Multiply_With_Ovflo_Check);
- -- Raises Constraint_Error if product of operands overflows Double_Int,
- -- otherwise returns the signed integer product. Gigi may also call this
- -- routine directly.
+ -- Raises Constraint_Error if product of operands overflows 64
+ -- bits, otherwise returns the 64-bit signed integer product.
+ -- GIGI may also call this routine directly.
+ --
+ -- The multiplication is done using pencil and paper algorithm using base
+ -- 2**32. The multiplication is done on unsigned values, then the correct
+ -- signed value is returned. Overflow check is performed by looking at
+ -- higher digits.
function Same_Sign (X, Y : Big_Integer) return Boolean is
(X = Big (Double_Int'(0))
Big (X) * Big (Y) / Big (Z), Big (R))
else
Big (Q) = Big (X) * Big (Y) / Big (Z));
- -- Performs the division of (X * Y) / Z, storing the quotient in Q
- -- and the remainder in R. Constraint_Error is raised if Z is zero,
- -- or if the quotient does not fit in Double_Int. Round indicates if
- -- the result should be rounded. If Round is False, then Q, R are
- -- the normal quotient and remainder from a truncating division.
- -- If Round is True, then Q is the rounded quotient. The remainder
- -- R is not affected by the setting of the Round flag.
+ -- Performs the division of (``X`` * ``Y``) / ``Z``, storing the quotient
+ -- in ``Q`` and the remainder in ``R``.
+ --
+ -- Constraint_Error is raised if ``Z`` is zero, or if the quotient does not
+ -- fit in ``Double_Int``.
+ --
+ -- ``Round`` indicates if the result should be rounded. If ``Round`` is
+ -- False, then ``Q``, ``R`` are the normal quotient and remainder from a
+ -- truncating division. If ``Round`` is True, then ``Q`` is the rounded
+ -- quotient. The remainder ``R`` is not affected by the setting of the
+ -- ``Round`` flag.
+ --
+ -- The multiplication is done using pencil and paper algorithm using base
+ -- 2**32. The multiplication is done on unsigned values. The result is a
+ -- 128 bit value.
+ --
+ -- The overflow is detected on the intermediate value.
+ --
+ -- If Z is a 32 bit value, the division is done using pencil and paper
+ -- algorithm.
+ --
+ -- Otherwise, the division is performed using the algorithm D from section
+ -- 4.3.1 of "The Art of Computer Programming Vol. 2" [TACP2]. Rounding is
+ -- applied on the result.
+ --
+ -- Finally, the sign is applied to the result and returned.
procedure Double_Divide
(X, Y, Z : Double_Int;
Big (X) / (Big (Y) * Big (Z)), Big (R))
else
Big (Q) = Big (X) / (Big (Y) * Big (Z)));
- -- Performs the division X / (Y * Z), storing the quotient in Q and
- -- the remainder in R. Constraint_Error is raised if Y or Z is zero,
- -- or if the quotient does not fit in Double_Int. Round indicates if the
- -- result should be rounded. If Round is False, then Q, R are the normal
- -- quotient and remainder from a truncating division. If Round is True,
- -- then Q is the rounded quotient. The remainder R is not affected by the
- -- setting of the Round flag.
+ -- Performs the division ``X`` / (``Y`` * ``Z``), storing the quotient in
+ -- ``Q`` and the remainder in ``R``. Constraint_Error is raised if ``Y`` or
+ -- ``Z`` is zero, or if the quotient does not fit in ``Double_Int``.
+ --
+ -- ``Round`` indicates if the result should be rounded. If ``Round`` is
+ -- False, then ``Q``, ``R`` are the normal quotient and remainder from a
+ -- truncating division. If ``Round`` is True, then ``Q`` is the rounded
+ -- quotient. The remainder ``R`` is not affected by the setting of the
+ -- ``Round`` flag.
+ --
+ -- Division by 0 is first detected.
+ --
+ -- The intermediate value ``Y`` * ``Z`` is then computed on 128 bits. The
+ -- multiplication is done on unsigned values.
+ --
+ -- If the high 64 bits of the intermediate value is not 0, then 0 is
+ -- returned. The overflow case of the largest negative number divided by
+ -- -1 is detected here.
+ --
+ -- 64-bit division is then performed, the result is rounded, its sign is
+ -- corrected, and then returned.
end System.Arith_Double;
Big (X) * Big (Y) / Big (Z), Big (R))
else
Big (Q) = Big (X) * Big (Y) / Big (Z));
- -- Performs the division of (X * Y) / Z, storing the quotient in Q
- -- and the remainder in R. Constraint_Error is raised if Z is zero,
- -- or if the quotient does not fit in 32 bits. Round indicates if
- -- the result should be rounded. If Round is False, then Q, R are
- -- the normal quotient and remainder from a truncating division.
- -- If Round is True, then Q is the rounded quotient. The remainder
- -- R is not affected by the setting of the Round flag.
+ -- Performs the division of (``X`` * ``Y``) / ``Z``, storing the quotient
+ -- in ``Q`` and the remainder in ``R``.
+ --
+ -- Constraint_Error is raised if ``Z`` is zero, or if the quotient does not
+ -- fit in 32-bits.
+ --
+ -- ``Round`` indicates if the result should be rounded. If ``Round`` is
+ -- False, then ``Q``, ``R`` are the normal quotient and remainder from a
+ -- truncating division. If ``Round`` is True, then ``Q`` is the rounded
+ -- quotient. The remainder ``R`` is not affected by the setting of the
+ -- ``Round`` flag.
+ --
+ -- The multiplication is done using pencil and paper algorithm using base
+ -- 2**32. The multiplication is done on unsigned values. The result is a
+ -- 128 bit value.
+ --
+ -- The overflow is detected on the intermediate value.
+ --
+ -- If Z is a 32 bit value, the division is done using pencil and paper
+ -- algorithm.
+ --
+ -- Otherwise, the division is performed using the algorithm D from section
+ -- 4.3.1 of "The Art of Computer Programming Vol. 2" [TACP2]. Rounding is
+ -- applied on the result.
+ --
+ -- Finally, the sign is applied to the result and returned.
end System.Arith_32;
Post => Add_With_Ovflo_Check64'Result = X + Y;
-- Raises Constraint_Error if sum of operands overflows 64 bits,
-- otherwise returns the 64-bit signed integer sum.
+ --
+ -- The sum of ``X`` and ``Y`` is first computed using wrap-around
+ -- semantics.
+ --
+ -- If the sign of ``X`` and ``Y`` are opposed, no overflow is possible and
+ -- the result is correct.
+ --
+ -- Otherwise, ``X`` and ``Y`` have the same sign; if the sign of the result
+ -- is not identical to ``X`` (or ``Y``), then an overflow occurred and
+ -- the exception *Constraint_Error* is raised; otherwise the result is
+ -- correct.
function Subtract_With_Ovflo_Check64 (X, Y : Int64) return Int64
with
Post => Subtract_With_Ovflo_Check64'Result = X - Y;
-- Raises Constraint_Error if difference of operands overflows 64
-- bits, otherwise returns the 64-bit signed integer difference.
+ --
+ -- The logic of the implementation is reversed from *Add_With_Ovflo_Check*:
+ -- if ``X`` and ``Y`` have the same sign, no overflow is checked, otherwise
+ -- a sign of the result is compared with the sign of ``X`` to check for
+ -- overflow.
function Multiply_With_Ovflo_Check64 (X, Y : Int64) return Int64
with
pragma Export (C, Multiply_With_Ovflo_Check64, "__gnat_mulv64");
-- Raises Constraint_Error if product of operands overflows 64
-- bits, otherwise returns the 64-bit signed integer product.
- -- Gigi may also call this routine directly.
+ -- GIGI may also call this routine directly.
+ --
+ -- The multiplication is done using pencil and paper algorithm using base
+ -- 2**32. The multiplication is done on unsigned values, then the correct
+ -- signed value is returned. Overflow check is performed by looking at
+ -- higher digits.
function Same_Sign (X, Y : Big_Integer) return Boolean is
(X = Big (Int64'(0))
Big (X) * Big (Y) / Big (Z), Big (R))
else
Big (Q) = Big (X) * Big (Y) / Big (Z));
- -- Performs the division of (X * Y) / Z, storing the quotient in Q
- -- and the remainder in R. Constraint_Error is raised if Z is zero,
- -- or if the quotient does not fit in 64 bits. Round indicates if
- -- the result should be rounded. If Round is False, then Q, R are
- -- the normal quotient and remainder from a truncating division.
- -- If Round is True, then Q is the rounded quotient. The remainder
- -- R is not affected by the setting of the Round flag.
+ -- Performs the division of (``X`` * ``Y``) / ``Z``, storing the quotient
+ -- in ``Q`` and the remainder in ``R``.
+ --
+ -- Constraint_Error is raised if ``Z`` is zero, or if the quotient does not
+ -- fit in 64-bits.
+ --
+ -- ``Round`` indicates if the result should be rounded. If ``Round`` is
+ -- False, then ``Q``, ``R`` are the normal quotient and remainder from a
+ -- truncating division. If ``Round`` is True, then ``Q`` is the rounded
+ -- quotient. The remainder ``R`` is not affected by the setting of the
+ -- ``Round`` flag.
+ --
+ -- The multiplication is done using pencil and paper algorithm using base
+ -- 2**32. The multiplication is done on unsigned values. The result is a
+ -- 128 bit value.
+ --
+ -- The overflow is detected on the intermediate value.
+ --
+ -- If Z is a 32 bit value, the division is done using pencil and paper
+ -- algorithm.
+ --
+ -- Otherwise, the division is performed using the algorithm D from section
+ -- 4.3.1 of "The Art of Computer Programming Vol. 2" [TACP2]. Rounding is
+ -- applied on the result.
+ --
+ -- Finally, the sign is applied to the result and returned.
procedure Scaled_Divide
(X, Y, Z : Int64;
Big (X) / (Big (Y) * Big (Z)), Big (R))
else
Big (Q) = Big (X) / (Big (Y) * Big (Z)));
- -- Performs the division X / (Y * Z), storing the quotient in Q and
- -- the remainder in R. Constraint_Error is raised if Y or Z is zero,
- -- or if the quotient does not fit in 64 bits. Round indicates if the
- -- result should be rounded. If Round is False, then Q, R are the normal
- -- quotient and remainder from a truncating division. If Round is True,
- -- then Q is the rounded quotient. The remainder R is not affected by the
- -- setting of the Round flag.
+ -- Performs the division ``X`` / (``Y`` * ``Z``), storing the quotient in
+ -- ``Q`` and the remainder in ``R``. Constraint_Error is raised if ``Y`` or
+ -- ``Z`` is zero, or if the quotient does not fit in 64-bits.
+ --
+ -- ``Round`` indicates if the result should be rounded. If ``Round`` is
+ -- False, then ``Q``, ``R`` are the normal quotient and remainder from a
+ -- truncating division. If ``Round`` is True, then ``Q`` is the rounded
+ -- quotient. The remainder ``R`` is not affected by the setting of the
+ -- ``Round`` flag.
+ --
+ -- Division by 0 is first detected.
+ --
+ -- The intermediate value ``Y`` * ``Z`` is then computed on 128 bits. The
+ -- multiplication is done on unsigned values.
+ --
+ -- If the high 64 bits of the intermediate value is not 0, then 0 is
+ -- returned. The overflow case of the largest negative number divided by
+ -- -1 is detected here.
+ --
+ -- 64-bit division is then performed, the result is rounded, its sign is
+ -- corrected, and then returned.
procedure Double_Divide
(X, Y, Z : Int64;
-- --
------------------------------------------------------------------------------
--- This package provides support for assertions (including pragma Assert,
--- pragma Debug, and Precondition/Postcondition/Predicate/Invariant aspects
--- and their corresponding pragmas).
+-- This package provides support for assertions (including ``pragma Assert``,
+-- ``pragma Debug``, and Precondition/Postcondition/Predicate/Invariant
+-- aspects and their corresponding pragmas).
-- This unit may be used directly from an application program by providing
-- an appropriate WITH, and the interface can be expected to remain stable.
-- --
------------------------------------------------------------------------------
+-- Provides the means to convert addresses to access types as defined by ARM
+-- 13.7.2.
+
generic
type Object (<>) is limited private;
type Object_Pointer is access all Object;
for Object_Pointer'Size use Standard'Address_Size;
+ -- Access type definition to the object
pragma No_Strict_Aliasing (Object_Pointer);
-- Strictly speaking, this routine should not be used to generate pointers
function To_Pointer (Value : Address) return Object_Pointer with
Global => null;
+ -- Return ``Value`` as an access to *Object*.
+ --
+ -- This function is an intrinsic so implemented by the compiler.
+
function To_Address (Value : Object_Pointer) return Address with
SPARK_Mode => Off;
+ -- Return ``Value`` as an *Address*.
+ --
+ -- This function is an intrinsic so implemented by the compiler.
pragma Import (Intrinsic, To_Pointer);
pragma Import (Intrinsic, To_Address);
-- --
------------------------------------------------------------------------------
--- This package provides atomic counter on platforms where it is supported:
+-- This package provides atomic counters routines
+
+-- This package support the following platforms:
-- - all Alpha platforms
-- - all AARCH64 platforms
-- - all ARM platforms
-- --
------------------------------------------------------------------------------
--- This package implements Atomic_Counter and Atomic_Unsigned operations for
--- platforms where GCC supports __atomic_add_fetch and __atomic_sub_fetch
--- builtins.
+-- This package implements unsigned and signed atomic counters using GCC's
+-- __atomic_add_fetch and __atomic_sub_fetch builtins.
with System.Atomic_Primitives; use System.Atomic_Primitives;
-- --
------------------------------------------------------------------------------
--- This package contains both atomic primitives defined from GCC built-in
+-- This package contains atomic primitives defined from GCC built-in
-- functions and operations used by the compiler to generate the lock-free
-- implementation of protected objects.
-- --
------------------------------------------------------------------------------
--- Operations on packed bit strings
+-- This package provides subprograms on bit strings. The compiler uses these
+-- subprograms for packed array operations.
package System.Bit_Ops is
- -- Note: in all the following routines, the System.Address parameters
+ -- In all the following routines, the System.Address parameters
-- represent the address of the first byte of an array used to represent
-- a packed array (of type System.Unsigned_Types.Packed_Bytes{1,2,4})
-- The length in bits is passed as a separate parameter. Note that all
Right : System.Address;
Rlen : Natural;
Result : System.Address);
- -- Bitwise "and" of given bit string with result being placed in Result.
- -- The and operation is allowed to destroy unused bits in the last byte,
- -- i.e. to leave them set in an undefined manner. Note that Left, Right
- -- and Result always have the same length in bits (Len).
+ -- Bitwise "and" of given bit string with result being placed in
+ -- ``Result``. The and operation is allowed to destroy unused bits in
+ -- the last byte, i.e. to leave them set in an undefined manner. Note that
+ -- ``Left``, ``Right`` and ``Result`` always have the same length in bits.
+ --
+ -- The procedure raises Constraint_Error if ``Llen`` and ``Rlen`` are not
+ -- equal.
+ --
+ -- The bitwise "and" operation is performed byte per byte, where the number
+ -- of bytes is the smallest number not less than ``Llen`` (or ``Rlen``)
+ -- divided by the 8.
function Bit_Eq
(Left : System.Address;
Llen : Natural;
Right : System.Address;
Rlen : Natural) return Boolean;
- -- Left and Right are the addresses of two bit packed arrays with Llen
- -- and Rlen being the respective length in bits. The routine compares the
- -- two bit strings for equality, being careful not to include the unused
- -- bits in the final byte. Note that the result is always False if Rlen
- -- is not equal to Llen.
+ -- ``Left`` and ``Right`` are the addresses of two bit packed arrays with
+ -- ``Llen`` and ``Rlen`` being the respective length in bits. The routine
+ -- compares the two bit strings for equality, being careful not to include
+ -- the unused bits in the final byte.
+ --
+ -- Note that the result is always False if ``Rlen`` is not equal to
+ -- ``Llen``.
+ --
+ -- Otherwise all the bytes but the last one are compared, and False is
+ -- returned if they aren't equal. Only the ``Llen`` mod 8 bits of the last
+ -- byte are compared, and false is returned if they aren't equal.
+ --
+ -- Otherwise, True is returned.
procedure Bit_Not
(Opnd : System.Address;
Len : Natural;
Result : System.Address);
- -- Bitwise "not" of given bit string with result being placed in Result.
- -- The not operation is allowed to destroy unused bits in the last byte,
- -- i.e. to leave them set in an undefined manner. Note that Result and
- -- Opnd always have the same length in bits (Len).
+ -- Bitwise "not" of given bit string with result being placed in
+ -- ``Result``. The not operation is allowed to destroy unused bits in the
+ -- last byte, i.e. to leave them set in an undefined manner. Note that
+ -- ``Result`` and ``Opnd`` always have the same length in bits (``Len``).
+ --
+ -- The bitwise "not" operation is performed byte per byte, where the
+ -- number of bytes is the smallest number not less that ``Len`` divided by
+ -- the number of bits in a byte (8).
procedure Bit_Or
(Left : System.Address;
Right : System.Address;
Rlen : Natural;
Result : System.Address);
- -- Bitwise "or" of given bit string with result being placed in Result.
+ -- Bitwise "or" of given bit string with result being placed in ``Result``.
-- The or operation is allowed to destroy unused bits in the last byte,
- -- i.e. to leave them set in an undefined manner. Note that Left, Right
- -- and Result always have the same length in bits (Len).
+ -- i.e. to leave them set in an undefined manner. Note that ``Left``,
+ -- ``Right`` and ``Result`` always have the same length in bits.
+ --
+ -- The implementation is similar to *Bit_And* but for the bitwise "or"
+ -- operation.
procedure Bit_Xor
(Left : System.Address;
Right : System.Address;
Rlen : Natural;
Result : System.Address);
- -- Bitwise "xor" of given bit string with result being placed in Result.
- -- The xor operation is allowed to destroy unused bits in the last byte,
- -- i.e. to leave them set in an undefined manner. Note that Left, Right
- -- and Result always have the same length in bits (Len).
+ -- Bitwise "xor" of given bit string with result being placed in
+ -- ``Result``. The xor operation is allowed to destroy unused bits in the
+ -- last byte, i.e. to leave them set in an undefined manner. Note that
+ -- ``Left``, ``Right`` and ``Result`` always have the same length in bits.
+ --
+ -- The implementation is similar to *Bit_And* but for the bitwise "xor"
+ -- operation.
end System.Bit_Ops;
pragma Pure;
type Boolean_Array is array (Integer range <>) of Boolean;
+ -- The base type for the boolean array operations
package Boolean_Operations renames System.Vectors.Boolean_Operations;
procedure Vector_Not is
new Unary_Operation ("not", Boolean_Operations."not");
+ -- Instantiation of Unary_Operation with function *not*
+
procedure Vector_And is new Binary_Operation ("and", System.Vectors."and");
+ -- Instantiation of Binary_Operation with function *and*
+
procedure Vector_Or is new Binary_Operation ("or", System.Vectors."or");
+ -- Instantiation of Binary_Operation with function *or*
+
procedure Vector_Xor is new Binary_Operation ("xor", System.Vectors."xor");
+ -- Instantiation of Binary_Operation with function *xor*
procedure Vector_Nand is
new Binary_Operation (Boolean_Operations.Nand, Boolean_Operations.Nand);
+ -- Instantiation of Binary_Operation with function *nand*
+
procedure Vector_Nor is
new Binary_Operation (Boolean_Operations.Nor, Boolean_Operations.Nor);
+ -- Instantiation of Binary_Operation with function *nor*
+
procedure Vector_Nxor is
new Binary_Operation (Boolean_Operations.Nxor, Boolean_Operations.Nxor);
+ -- Instantiation of Binary_Operation with function *nxor*
+
end System.Boolean_Array_Operations;
------------------------------------------------------------------------------
-- Intrinsic routines for byte swapping. These are used by the expanded code
--- (supporting alternative byte ordering), and by the GNAT.Byte_Swapping run
--- time package which provides user level routines for byte swapping.
+-- (supporting alternative byte ordering), and by the ``GNAT.Byte_Swapping``
+-- run-time package which provides user level routines for byte swapping.
with Interfaces;
Right : System.Address;
Left_Len : Natural;
Right_Len : Natural) return Integer;
- -- Compare the array starting at address Left of length Left_Len
- -- with the array starting at address Right of length Right_Len.
+ -- Compare the array starting at address ``Left`` of length ``Left_Len``
+ -- with the array starting at address ``Right`` of length ``Right_Len``.
-- The comparison is in the normal Ada semantic sense of array
- -- comparison. The result is -1,0,+1 for Left<Right, Left=Right,
- -- Left>Right respectively. This function works with 4 byte words
- -- if the operands are aligned on 4-byte boundaries and long enough.
+ -- comparison.
+ --
+ -- The result is -1, 0, +1 for ``Left`` < ``Right``, ``Left`` = ``Right``,
+ -- ``Left`` > ``Right`` respectively.
+ --
+ -- If addresses are not word aligned or if the length is less than a word,
+ -- then the result of *Compare_Array_S8_Unaligned* is returned.
+ --
+ -- This function iterates on the common number of words, comparing words.
+ -- If two words are not equal, the result of *Compare_Array_S8_Unaligned*
+ -- on these words is returned.
+ --
+ -- Finally, the result of *Compare_Array_S8_Unaligned* on the remaining
+ -- bytes is returned.
function Compare_Array_S8_Unaligned
(Left : System.Address;
-- Same functionality as Compare_Array_S8 but always proceeds by
-- bytes. Used when the caller knows that the operands are unaligned,
-- or short enough that it makes no sense to go by words.
+ --
+ -- This subprogram compares ``Left`` and ``Right`` byte per byte and
+ -- returns immediately when two bytes differ.
end System.Compare_Array_Signed_8;
Right : System.Address;
Left_Len : Natural;
Right_Len : Natural) return Integer;
- -- Compare the array starting at address Left of length Left_Len with the
- -- array starting at address Right of length Right_Len. The comparison is
- -- in the normal Ada semantic sense of array comparison. The result is -1,
- -- 0, +1 for Left < Right, Left = Right, Left > Right respectively. This
- -- function works with 4 byte words if the operands are aligned on 4-byte
- -- boundaries and long enough.
+ -- Compare the array starting at address ``Left`` of length ``Left_Len``
+ -- with the array starting at address ``Right`` of length ``Right_Len``.
+ -- The comparison is in the normal Ada semantic sense of array
+ -- comparison.
+ --
+ -- The result is -1, 0, +1 for ``Left`` < ``Right``, ``Left`` = ``Right``,
+ -- ``Left`` > ``Right`` respectively.
+ --
+ -- The same algorithm is used as in package
+ -- ``System.Compare_Array_Signed_8``.
function Compare_Array_U8_Unaligned
(Left : System.Address;
-- Same functionality as Compare_Array_U8 but always proceeds by bytes.
-- Used when the caller knows that the operands are unaligned, or short
-- enough that it makes no sense to go by words.
+ --
+ -- The same algorithm is used as in package
+ -- ``System.Compare_Array_Signed_8``.
end System.Compare_Array_Unsigned_8;
Right : System.Address;
Left_Len : Natural;
Right_Len : Natural) return Integer;
- -- Compare the array starting at address Left of length Left_Len
- -- with the array starting at address Right of length Right_Len.
+ -- Compare the array starting at address ``Left`` of length ``Left_Len``
+ -- with the array starting at address ``Right`` of length ``Right_Len``.
-- The comparison is in the normal Ada semantic sense of array
- -- comparison. The result is -1,0,+1 for Left<Right, Left=Right,
- -- Left>Right respectively. This function works with 4 byte words
- -- if the operands are aligned on 4-byte boundaries and long enough.
+ -- comparison.
+ --
+ -- The result is -1, 0, +1 for ``Left`` < ``Right``, ``Left`` = ``Right``,
+ -- ``Left`` > ``Right`` respectively.
+ --
+ -- If both addresses are word aligned, the function iterates through all
+ -- of the equal words.
+ --
+ -- Then, if the addresses are half word aligned, the function iterates on
+ -- the remaining half words, and returns as soon as two half words are not
+ -- equal.
+ --
+ -- Otherwise, the function iterates on the remaining unaligned half words,
+ -- compares them using unaligned accesses, and returns as soon as two half
+ -- words are not equal.
+ --
+ -- Finally, at this point, all the words are equal. The result is decided
+ -- by comparing their lengths.
end System.Compare_Array_Signed_16;
Right : System.Address;
Left_Len : Natural;
Right_Len : Natural)
- return Integer;
- -- Compare the array starting at address Left of length Left_Len
- -- with the array starting at address Right of length Right_Len.
+ return Integer;
+ -- Compare the array starting at address ``Left`` of length ``Left_Len``
+ -- with the array starting at address ``Right`` of length ``Right_Len``.
-- The comparison is in the normal Ada semantic sense of array
- -- comparison. The result is -1,0,+1 for Left<Right, Left=Right,
- -- Left>Right respectively.
+ -- comparison.
+ --
+ -- The result is -1, 0, +1 for ``Left`` < ``Right``, ``Left`` = ``Right``,
+ -- ``Left`` > ``Right`` respectively.
+ --
+ -- If the addresses are word aligned, the function iterates on the words,
+ -- and returns as soon as two words are not equal.
+ --
+ -- Otherwise, the function iterates on the unaligned words, compares them
+ -- using unaligned accesses, and returns as soon as two words are not
+ -- equal.
+ --
+ -- Finally, at this point all the words are equal. The result is decided
+ -- by comparing their lengths.
end System.Compare_Array_Signed_32;
Right : System.Address;
Left_Len : Natural;
Right_Len : Natural) return Integer;
- -- Compare the array starting at address Left of length Left_Len
- -- with the array starting at address Right of length Right_Len.
+ -- Compare the array starting at address ``Left`` of length ``Left_Len``
+ -- with the array starting at address ``Right`` of length ``Right_Len``.
-- The comparison is in the normal Ada semantic sense of array
- -- comparison. The result is -1,0,+1 for Left<Right, Left=Right,
- -- Left>Right respectively.
+ -- comparison.
+ --
+ -- The result is -1, 0, +1 for ``Left`` < ``Right``, ``Left`` = ``Right``,
+ -- ``Left`` > ``Right`` respectively.
+ --
+ -- If the addresses are double word aligned, the function iterates on the
+ -- double words, and returns as soon as two double words are not equal.
+ --
+ -- Otherwise, the function iterates on the unaligned double words, compares
+ -- them using unaligned accesses, and returns as soon as two double words
+ -- are not equal.
+ --
+ -- Finally, at this point all the double words are equal. The result is
+ -- decided by comparing their lengths.
end System.Compare_Array_Signed_64;
Right : System.Address;
Left_Len : Natural;
Right_Len : Natural) return Integer;
- -- Compare the array starting at address Left of length Left_Len
- -- with the array starting at address Right of length Right_Len.
+ -- Compare the array starting at address ``Left`` of length ``Left_Len``
+ -- with the array starting at address ``Right`` of length ``Right_Len``.
-- The comparison is in the normal Ada semantic sense of array
- -- comparison. The result is -1,0,+1 for Left<Right, Left=Right,
- -- Left>Right respectively. This function works with 4 byte words
- -- if the operands are aligned on 4-byte boundaries and long enough.
+ -- comparison.
+ --
+ -- The result is -1, 0, +1 for ``Left`` < ``Right``, ``Left`` = ``Right``,
+ -- ``Left`` > ``Right`` respectively.
+ --
+ -- The same algorithm is used as in package
+ -- ``System.Compare_Array_Signed_16``.
end System.Compare_Array_Unsigned_16;
Right : System.Address;
Left_Len : Natural;
Right_Len : Natural) return Integer;
- -- Compare the array starting at address Left of length Left_Len
- -- with the array starting at address Right of length Right_Len.
+ -- Compare the array starting at address ``Left`` of length ``Left_Len``
+ -- with the array starting at address ``Right`` of length ``Right_Len``.
-- The comparison is in the normal Ada semantic sense of array
- -- comparison. The result is -1,0,+1 for Left<Right, Left=Right,
- -- Left>Right respectively.
+ -- comparison.
+ --
+ -- The result is -1, 0, +1 for ``Left`` < ``Right``, ``Left`` = ``Right``,
+ -- ``Left`` > ``Right`` respectively.
+ --
+ -- The same algorithm is used as in package
+ -- ``System.Compare_Array_Signed_32``.
end System.Compare_Array_Unsigned_32;
Right : System.Address;
Left_Len : Natural;
Right_Len : Natural) return Integer;
- -- Compare the array starting at address Left of length Left_Len
- -- with the array starting at address Right of length Right_Len.
+ -- Compare the array starting at address ``Left`` of length ``Left_Len``
+ -- with the array starting at address ``Right`` of length ``Right_Len``.
-- The comparison is in the normal Ada semantic sense of array
- -- comparison. The result is -1,0,+1 for Left<Right, Left=Right,
- -- Left>Right respectively.
+ -- comparison.
+ --
+ -- The result is -1, 0, +1 for ``Left`` < ``Right``, ``Left`` = ``Right``,
+ -- ``Left`` > ``Right`` respectively.
+ --
+ -- The same algorithm is used as in package
+ -- ``System.Compare_Array_Signed_64``.
end System.Compare_Array_Unsigned_64;
-- --
------------------------------------------------------------------------------
--- Integer exponentiation (checks off)
+-- This package implements Integer exponentiation (checks off)
-- Preconditions, postconditions, ghost code, loop invariants and assertions
-- in this unit are meant for analysis only, not for run-time checking, as it
function Exn_Integer (Left : Integer; Right : Natural) return Integer
renames Exponn_Integer.Expon;
+ -- Return the power of ``Left`` by ``Right`` where ``Left`` is an Integer.
+ -- No check is made on the validity of the result.
+ --
+ -- This function is implemented using the standard logarithmic approach:
+ -- ``Right`` gets shifted right testing successive low order bits, and
+ -- ``Left`` is raised to the next power of 2.
+ --
+ -- As checks aren't enabled for this service, the result is not defined
+ -- in case of overflow.
end System.Exn_Int;
-- --
------------------------------------------------------------------------------
--- Long_Long_Float exponentiation (checks off)
+-- This package implements ``[Long_[Long_]]Float`` exponentiation
+-- (checks off).
with System.Exponr;
-- --
------------------------------------------------------------------------------
--- Long_Long_Integer exponentiation (checks off)
+-- This package implements Long_Long_Integer exponentiation (checks off)
-- Preconditions, postconditions, ghost code, loop invariants and assertions
-- in this unit are meant for analysis only, not for run-time checking, as it
function Exn_Long_Long_Integer
(Left : Long_Long_Integer; Right : Natural) return Long_Long_Integer
renames Exponn_Integer.Expon;
+ -- Return the power of ``Left`` by ``Right`` where ``Left`` is a
+ -- Long_Long_Integer. No check is made on the validity of the result.
+ --
+ -- This function is implemented using the standard logarithmic approach:
+ -- ``Right`` gets shifted right testing successive low order bits, and
+ -- ``Left`` is raised to the next power of 2.
+ --
+ -- As checks aren't enabled for this service, the result is not defined
+ -- in case of overflow.
end System.Exn_LLI;
-- --
------------------------------------------------------------------------------
--- Integer exponentiation (checks on)
+-- This package implements Integer exponentiation (checks on)
-- Preconditions, postconditions, ghost code, loop invariants and assertions
-- in this unit are meant for analysis only, not for run-time checking, as it
function Exp_Integer (Left : Integer; Right : Natural) return Integer
renames Expont_Integer.Expon;
+ -- Return the power of ``Left`` by ``Right`` where ``Left`` is an
+ -- Integer.
+ --
+ -- This function is implemented using the standard logarithmic approach:
+ -- ``Right`` gets shifted right testing successive low order bits, and
+ -- ``Left`` is raised to the next power of 2.
+ --
+ -- In case of overflow, Constraint_Error is raised.
end System.Exp_Int;
-- --
------------------------------------------------------------------------------
--- Long_Long_Integer exponentiation (checks on)
+-- This package implements Long_Long_Integer exponentiation
-- Preconditions, postconditions, ghost code, loop invariants and assertions
-- in this unit are meant for analysis only, not for run-time checking, as it
function Exp_Long_Long_Integer
(Left : Long_Long_Integer; Right : Natural) return Long_Long_Integer
renames Expont_Integer.Expon;
+ -- Return the power of ``Left`` by ``Right`` where ``Left`` is a
+ -- Long_Long_Integer.
+ --
+ -- This function is implemented using the standard logarithmic approach:
+ -- ``Right`` gets shifted right testing successive low order bits, and
+ -- ``Left`` is raised to the next power of 2.
+ --
+ -- In case of overflow, Constraint_Error is raised.
end System.Exp_LLI;
-- --
------------------------------------------------------------------------------
--- This function performs exponentiation of unsigned types with binary modulus
--- values exceeding that of System.Unsigned_Types.Unsigned.
--- The result is always full width, the caller must do a masking operation if
--- the modulus is less than 2 ** Long_Long_Unsigned'Size.
+-- This function performs exponentiation of unsigned types (with binary
+-- modulus values exceeding that of Unsigned_Types.Unsigned). The result
+-- is always full width, the caller must do a masking operation if the
+-- modulus is less than 2 ** (Long_Long_Unsigned'Size).
--- Preconditions in this unit are meant for analysis only, not for run-time
--- checking, so that the expected exceptions are raised. This is enforced
--- by setting the corresponding assertion policy to Ignore. Postconditions
--- and contract cases should not be executed at runtime as well, in order
--- not to slow down the execution of these functions.
+-- Note: preconditions in this unit are meant for analysis only, not for
+-- run-time checking, so that the expected exceptions are raised. This is
+-- enforced by setting the corresponding assertion policy to Ignore.
+-- Postconditions and contract cases should not be executed at run-time as
+-- well, in order not to slow down the execution of these functions.
pragma Assertion_Policy (Pre => Ignore,
Post => Ignore,
function Exp_Long_Long_Unsigned is new Exponu (Long_Long_Unsigned);
pragma Pure_Function (Exp_Long_Long_Unsigned);
+ -- Return the power of ``Left`` by ``Right`` where ``Left`` is a
+ -- Long_Long_Unsigned.
+ --
+ -- This function is implemented using the standard logarithmic approach:
+ -- ``Right`` gets shifted right testing successive low order bits, and
+ -- ``Left`` is raised to the next power of 2.
+ --
+ -- In case of overflow, Constraint_Error is raised.
end System.Exp_LLU;
-- This function performs exponentiation of a modular type with nonbinary
-- modulus values. Arithmetic is done in Long_Long_Unsigned, with explicit
-- accounting for the modulus value which is passed as the second argument.
+--
-- Note that 1 is a binary modulus (2**0), so the compiler should not (and
-- will not) call this function with Modulus equal to 1.
with
Pre => Modulus /= 0 and then Modulus not in Power_Of_2,
Post => Big (Exp_Modular'Result) = Big (Left) ** Right mod Big (Modulus);
+ -- Return the power of ``Left`` by ``Right` modulo ``Modulus``.
+ --
+ -- This function is implemented using the standard logarithmic approach:
+ -- ``Right`` gets shifted right testing successive low order bits, and
+ -- ``Left`` is raised to the next power of 2. The multiplications are
+ -- performed using modular multiplications.
end System.Exp_Mod;
-- --
------------------------------------------------------------------------------
--- Signed integer exponentiation (checks off)
+-- This package provides functions for signed integer exponentiation. This
+-- is the version of the package with checks disabled.
with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
with
Pre => In_Int_Range (Big (Left) ** Right),
Post => Expon'Result = Left ** Right;
+ -- Calculate ``Left`` ** ``Right``. If ``Left`` is 0 then 0 is returned
+ -- and if ``Right`` is 0 then 1 is returned. In all other cases the result
+ -- is set to 1 and then computed in a loop as follows:
+ -- If ``Right`` is a multiple of 2 then multiply the result with ``Left``.
+ -- Divide ``Right`` by 2.
+ -- If ``Right is 0, return.
+ -- Multiply ``Left`` with itself.
end System.Exponn;
-- --
------------------------------------------------------------------------------
--- Signed integer exponentiation (checks on)
+-- This package provides functions for signed integer exponentiation. This
+-- is the version of the package with checks enabled.
with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
with
Pre => In_Int_Range (Big (Left) ** Right),
Post => Expon'Result = Left ** Right;
+ -- Calculate ``Left`` ** ``Right``. If ``Left`` is 0 then 0 is returned
+ -- and if ``Right`` is 0 then 1 is returned. In all other cases the result
+ -- is set to 1 and then computed in a loop as follows:
+ -- If ``Right`` is a multiple of 2 then multiply the result with ``Left``.
+ -- Divide ``Right`` by 2.
+ -- If ``Right is 0, return.
+ -- Multiply ``Left`` with itself.
end System.Expont;
-- --
------------------------------------------------------------------------------
--- Modular integer exponentiation
+-- This function implements unsigned integer exponentiation
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced
with
SPARK_Mode,
Post => System.Exponu'Result = Left ** Right;
+-- Calculate ``Left`` ** ``Right``. If ``Left`` is 0 then 0 is returned
+-- and if ``Right`` is 0 then 1 is returned. In all other cases the result
+-- is set to 1 and then computed in a loop as follows:
+-- If ``Right`` is a multiple of 2 then multiply the result with ``Left``.
+-- Divide ``Right`` by 2.
+-- If ``Right is 0, return.
+-- Multiply ``Left`` with itself.
-- --
------------------------------------------------------------------------------
--- This function performs exponentiation of unsigned types with binary modulus
--- values up to and including that of System.Unsigned_Types.Unsigned.
--- The result is always full width, the caller must do a masking operation if
--- the modulus is less than 2 ** Unsigned'Size.
+-- This function performs exponentiation of unsigned types (with binary
+-- modulus values up to and including that of Unsigned_Types.Unsigned).
+--
+-- The result is always full width, the caller must do a masking operation
+-- the modulus is less than 2 ** (Unsigned'Size).
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced
function Exp_Unsigned is new Exponu (Unsigned);
pragma Pure_Function (Exp_Unsigned);
+ -- Return the power of ``Left`` by ``Right`` where ``Left`` is an
+ -- Unsigned.
+ --
+ -- This function is implemented using the standard logarithmic approach:
+ -- ``Right`` gets shifted right testing successive low order bits, and
+ -- ``Left`` is raised to the next power of 2.
+ --
+ -- In case of overflow, Constraint_Error is raised.
end System.Exp_Uns;
------------------------------------------------------------------------------
-- This package contains an instantiation of the floating-point attribute
--- runtime routines for the type Float.
+-- runtime routines for the type Float. It is an instantiation of
+-- ``System.Fat_Gen`` for Float.
with System.Fat_Gen;
-- This generic package provides a target independent implementation of the
-- floating-point attributes that denote functions. The implementations here
--- should be portable and reasonably efficient. The runtime contains a set of
--- instantiations of this package for all predefined floating-point types.
+-- are portable, but very slow. The runtime contains a set of instantiations
+-- of this package for all predefined floating-point types, and these should
+-- be replaced by efficient assembly language code where possible.
generic
type T is digits <>;
-- problem, but the resulting inefficiency would be annoying.
function Adjacent (X, Towards : T) return T;
+ -- If ``Towards`` = ``X``, the function returns ``X``; oterwise, it yields
+ -- the machien number of the type *T* adjacent to ``X`` in the direction
+ -- ``Towards``, if that machine number exists.
function Ceiling (X : T) return T;
+ -- Truncate ``X``. If the truncation is equal to ``X`` return ``X``. If
+ -- ``X`` is less than zero, return the truncation, otherwise add one
+ -- to the truncation.
function Compose (Fraction : T; Exponent : UI) return T;
+ -- Decompose the ``Fraction`` into its fraction and exponent parts. Call
+ -- *Scaling* with the returned fraction part and ``Exponent``.
function Copy_Sign (Value, Sign : T) return T;
+ -- Take the absolute value of ``Value``. Negate the result if ``Sign`` is
+ -- less than zero.
function Exponent (X : T) return UI;
+ -- Decompose `X`` and return the exponent part.
function Floor (X : T) return T;
+ -- Truncate ``X``. If the truncation is equal to ``X`` return ``X``. If
+ -- ``X`` is greater than zero, return the truncation, otherwise subtract
+ -- one from the truncation.
function Fraction (X : T) return T;
+ -- Decompose `X`` and return the fraction part
function Leading_Part (X : T; Radix_Digits : UI) return T;
+ -- Return ``X`` if the ``Radix_Digits`` is larger than the type's machine
+ -- mantissa. Otherwise scale down and truncate ``X`` by the difference
+ -- between the exponent of ``X`` and ``Radix_Digits``, then scale the
+ -- result back up.
function Machine (X : T) return T;
+ -- Force ``X`` to be stored in memory and retrieve the result
function Machine_Rounding (X : T) return T;
+ -- Truncate the absolute value of ``X`` + 0.5. If ``X`` is negative, negate
+ -- the result.
function Model (X : T) return T;
+ -- If ``X`` is a model number of *T*, the function returns ``X``;
+ -- otherwise it yields the value obtained by rounding or truncating ``X``
+ -- to either one of the adjacent model numbers of *T*.
+ --
+ -- We treat *Model* as identical to *Machine*. This is true of IEEE and
+ -- other nice floating-point systems, but not necessarily true of all
+ -- systems.
function Pred (X : T) return T;
+ -- Return the machine number immediately below the value of ``X``.
+ --
+ -- If zero, return the negative of *Succ* (``X``).
+ --
+ -- If ``X`` = *T*'First, return negative infinity.
+ --
+ -- If ``X`` is already infinity, return ``X``.
+ --
+ -- Otherwise, subtract from ``X`` a number equivalent to the value of its
+ -- least significant bit.
function Remainder (X, Y : T) return T;
+ -- Return the remainder (n) of ``X`` divided by ``Y``.
+ -- If abs(n - ``X`` / ``Y``) = 1/2 then n is chosen to be even.
+ --
+ -- Calculate the modulus remainder: if abs(``X``) < abs(``Y``) then the
+ -- remainder is abs(``X``). Otherwise, decompose abs(``X``) and abs(``Y``).
+ -- Then:
+ --
+ -- .. code-block:: ada
+ --
+ -- P := Compose (Y_Frac, X_Exp);
+ -- K := X_Exp - Y_Exp;
+ -- Rem := |X|;
+ -- for J in reverse 0 .. K loop
+ -- if Rem >= P then
+ -- Rem := Rem - P;
+ -- end if;
+ -- P := P * 0.5;
+ -- end loop;
+ --
+ -- Return the IEEE remainder by adjusting result such that if
+ -- abs(n - X/Y) = 1/2 then n is even.
function Rounding (X : T) return T;
+ -- The function yields the integral value nearest to ``X``, rounding away
+ -- from zero if ``X`` lies exactly halfway between two integers.
+ --
+ -- The function truncates the absolute value of ``X`` + 0.5. If ``X`` is
+ -- negative, negate the result.
function Scaling (X : T; Adjustment : UI) return T;
+ -- Let v be the value ``X`` * *T*'Machine_RadixAdjustment. If v is a
+ -- machine number of the type *T*, or if abs(v) >= *T*'Model_Small, the
+ -- function yields v; otherwise, it yields either one of the machine
+ -- numbers of the type *T* adjacent to v.
+ --
+ -- If ``X`` or ``Adjustment`` equal zero, return ``X``. Otherwise, return
+ -- ``X`` * Machine_Radix ** ``Adjustment``.
function Succ (X : T) return T;
+ -- Returns the machine number immediately above the value of X.
+ --
+ -- If zero, return the smallest denormal.
+ --
+ -- If ``X`` = *T*'Last, return infinity.
+ --
+ -- If ``X`` is already infinity, return ``X``.
+ --
+ -- Otherwise, add to X a number equivalent to the value of its least
+ -- significant bit.
function Truncation (X : T) return T;
+ -- The function yields the value *Ceiling* (``X``) when ``X`` is negative,
+ -- and *Floor* (``X``) otherwise.
+ --
+ -- Return *T*'Machine (RM1 + N) - RM1 where N is abs(``X``) and
+ -- RM1 = radix ** (mantissa - 1). Negate the result where ``X`` is
+ -- negative.
function Unbiased_Rounding (X : T) return T;
+ -- The integral value nearest to ``X``, rounding toward the even integer
+ -- if ``X`` lies exactly halfway between two integers.
+ --
+ -- This function truncates abs(``X``). If the tail of the result is greater
+ -- than 0.5 add one to the result. If the tail equals 0.5, round to the
+ -- nearest even integer. Negate the result if ``X`` is negative.
function Valid (X : not null access T) return Boolean;
- -- This function checks if the object of type T referenced by X is valid,
- -- and returns True/False accordingly. The parameter is passed by reference
- -- (access) here, as the object of type T may be an abnormal value that
- -- cannot be passed in a floating-point register, and the whole point of
- -- 'Valid is to prevent exceptions. Note that the object of type T must
- -- have the natural alignment for type T.
+ -- This function checks if the object of type *T* referenced by ``X`` is
+ -- valid, and returns True/False accordingly. The parameter is passed by
+ -- reference (access) here, as the object of type T may be an abnormal
+ -- value that cannot be passed in a floating-point register, and the whole
+ -- point of 'Valid is to prevent exceptions. Note that the object of
+ -- type *T* must have the natural alignment for type *T*.
+ --
+ -- If denormalized numbers are valid: return True unless ``X`` is infinity
+ -- or NaN. If denormalized numbers are not valid, return False if ``X`` is
+ -- a denormal number.
type S is new String (1 .. T'Size / Character'Size);
type P is access all S with Storage_Size => 0;
------------------------------------------------------------------------------
-- This package contains an instantiation of the floating-point attribute
--- runtime routines for the type Long_Float.
+-- runtime routines for the type Long_Float. It is an instantiation of
+-- ``System.Fat_Gen`` for Long_Float.
with System.Fat_Gen;
------------------------------------------------------------------------------
-- This package contains an instantiation of the floating-point attribute
--- runtime routines for the type Long_Long_Float.
+-- runtime routines for the type Long_Long_Float. It is an instantiation of
+-- ``System.Fat_Gen`` for Long_Long_Float.
with System.Fat_Gen;
--
-- The call to Reset simply has no effect if the target environment
-- does not give rise to such concerns.
+
+ -- The *Reset* procedure is a no-op on all Bareboard targets, the FPU
+ -- configuration being under full control there.
+
end System.Float_Control;
-- If the arguments are aligned on word boundaries and the word size is a
-- multiple M of the element size, the operations will be done M elements
-- at a time using vector operations on a word.
-
+--
-- All routines assume argument arrays have the same length, and arguments
-- with mode "in" do not alias arguments with mode "out" or "in out".
-- If the number N of elements to be processed is not a multiple of M
procedure Binary_Operation
(R, X, Y : System.Address;
Length : System.Storage_Elements.Storage_Count);
+ -- *Binary_Operation* iterates on the elements pointed to by `X` and `Y`
+ -- and places the result in `R`.
generic
with function Element_Op (X : Element) return Element;
procedure Unary_Operation
(R, X : System.Address;
Length : System.Storage_Elements.Storage_Count);
+ -- *Unary_Operation* iterates on the elements pointed to by `X`
+ -- and places the result in `R`.
+
end System.Generic_Vector_Operations;
------------------------------------------------------------------------------
-- Contains the routine for computing the image in based format of signed and
--- unsigned integers for use by Text_IO.Integer_IO and Text_IO.Modular_IO.
+-- unsigned integers for use by ``Text_IO.Integer_IO`` and
+-- ``Text_IO.Modular_IO``.
generic
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- decimal fixed point types, and also for conversion operations required in
--- Text_IO.Decimal_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Decimal_IO`` conversions routines for decimal fixed point
+-- types.
generic
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- ordinary fixed point types whose Small is the ratio of two Int values, and
--- also for conversion operations required in Text_IO.Fixed_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Fixed_IO`` conversions routines for for ordinary fixed
+-- point types whose Small is the ratio of two Int values.
generic
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- signed integer types, and also for conversion operations required in
--- Text_IO.Integer_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Integer_IO`` conversions routines for signed integer
+-- types.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- --
------------------------------------------------------------------------------
--- Enumeration_Type'Image for all enumeration types except those in package
--- Standard (where we have no opportunity to build image tables), and in
--- package System (where it is too early to start building image tables).
+-- ``Image`` attribute support for all enumeration types except those in
+-- package Standard (where we have no opportunity to build image tables), and
+-- in package System (where it is too early to start building image tables).
-- Special routines exist for the enumeration types in these packages.
generic
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- modular integer types, and also for conversion operations required in
--- Text_IO.Modular_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Modular_IO`` conversions routines for modular integer
+-- types.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- --
------------------------------------------------------------------------------
--- Contains the routine for computing the image of signed and unsigned
--- integers up to Integer for use by Text_IO.Integer_IO and
--- Text_IO.Modular_IO.
+-- Contains the routines for computing the image of signed and unsigned
+-- integers up to ``Integer`` for use by ``Ada.Text_IO.Integer_IO`` and
+-- ``Ada.Text_IO.Modular_IO``.
generic
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- decimal fixed point types up to 128-bit mantissa, and also for conversion
--- operations required in Text_IO.Decimal_IO for them.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Decimal_IO`` conversions routines for decimal fixed point
+-- types up to 128-bit mantissa.
with Interfaces;
with System.Image_D;
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- decimal fixed point types up to 32-bit mantissa, and also for conversion
--- operations required in Text_IO.Decimal_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Decimal_IO`` conversions routines for decimal fixed point
+-- types up to 32-bit mantissa.
with Interfaces;
with System.Image_D;
P : out Natural;
Scale : Integer)
renames Impl.Image_Decimal;
+ -- Computes fixed_type'Image (V), where V is the integer value (in units of
+ -- delta) of a decimal type whose Scale is as given and stores the result
+ -- S (1 .. P), updating P on return. The result is computed according to
+ -- the rules for image for fixed-point types (RM 3.5(34)). The caller
+ -- guarantees that S is long enough to hold the result and has a lower
+ -- bound of 1.
procedure Set_Image_Decimal32
(V : Int32;
Aft : Natural;
Exp : Natural)
renames Impl.Set_Image_Decimal;
+ -- Sets the image of V, where V is the integer value (in units of delta)
+ -- of a decimal type with the specified Scale, starting at S (P + 1) and
+ -- updating P to point to the last character stored, the caller promises
+ -- that the buffer is large enough and no check is made. Constraint_Error
+ -- will not necessarily be raised if this requirement is violated, since
+ -- it is perfectly valid to compile this unit with checks off. The Fore,
+ -- Aft and Exp values can be set to any valid values for the case of use
+ -- by Text_IO.Decimal_IO.
end System.Img_Decimal_32;
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- decimal fixed point types up to 64-bit mantissa, and also for conversion
--- operations required in Text_IO.Decimal_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Decimal_IO`` conversions routines for decimal fixed point
+-- types up to 64-bit mantissa.
with Interfaces;
with System.Image_D;
P : out Natural;
Scale : Integer)
renames Impl.Image_Decimal;
+ -- Computes fixed_type'Image (V), where V is the integer value (in units of
+ -- delta) of a decimal type whose Scale is as given and stores the result
+ -- S (1 .. P), updating P on return. The result is computed according to
+ -- the rules for image for fixed-point types (RM 3.5(34)). The caller
+ -- guarantees that S is long enough to hold the result and has a lower
+ -- bound of 1.
procedure Set_Image_Decimal64
(V : Int64;
Aft : Natural;
Exp : Natural)
renames Impl.Set_Image_Decimal;
+ -- Sets the image of V, where V is the integer value (in units of delta)
+ -- of a decimal type with the specified Scale, starting at S (P + 1) and
+ -- updating P to point to the last character stored, the caller promises
+ -- that the buffer is large enough and no check is made. Constraint_Error
+ -- will not necessarily be raised if this requirement is violated, since
+ -- it is perfectly valid to compile this unit with checks off. The Fore,
+ -- Aft and Exp values can be set to any valid values for the case of use
+ -- by Text_IO.Decimal_IO.
end System.Img_Decimal_64;
-- --
------------------------------------------------------------------------------
--- Instantiation of System.Image_N for enumeration types whose names table
+-- Instantiation of ``System.Image_N`` for enumeration types whose names table
-- has a length that fits in a 16-bit but not a 8-bit integer.
with Interfaces;
Names : String;
Indexes : System.Address)
renames Impl.Image_Enumeration;
+ -- Used to compute Enum'Image (Str) where Enum is some enumeration type
+ -- other than those defined in package Standard. Names is a string with
+ -- a lower bound of 1 containing the characters of all the enumeration
+ -- literals concatenated together in sequence. Indexes is the address of
+ -- an array of type array (0 .. N) of Interfaces.Integer_16, where N is the
+ -- number of enumeration literals in the type. The Indexes values are the
+ -- starting subscript of each enumeration literal, indexed by Pos values,
+ -- with an extra entry at the end containing Names'Length + 1. The reason
+ -- that Indexes is passed by address is that the actual type is created on
+ -- the fly by the expander. The desired 'Image value is stored in S
+ -- (1 .. P) and P is set on return. The caller guarantees that S is long
+ -- enough to hold the result and that the lower bound is 1.
end System.Img_Enum_16;
-- --
------------------------------------------------------------------------------
--- Instantiation of System.Image_N for enumeration types whose names table
+-- Instantiation of ``System.Image_N`` for enumeration types whose names table
-- has a length that fits in a 32-bit but not a 16-bit integer.
with Interfaces;
Names : String;
Indexes : System.Address)
renames Impl.Image_Enumeration;
+ -- Used to compute Enum'Image (Str) where Enum is some enumeration type
+ -- other than those defined in package Standard. Names is a string with
+ -- a lower bound of 1 containing the characters of all the enumeration
+ -- literals concatenated together in sequence. Indexes is the address of
+ -- an array of type array (0 .. N) of Interfaces.Integer_32, where N is the
+ -- number of enumeration literals in the type. The Indexes values are the
+ -- starting subscript of each enumeration literal, indexed by Pos values,
+ -- with an extra entry at the end containing Names'Length + 1. The reason
+ -- that Indexes is passed by address is that the actual type is created on
+ -- the fly by the expander. The desired 'Image value is stored in S
+ -- (1 .. P) and P is set on return. The caller guarantees that S is long
+ -- enough to hold the result and that the lower bound is 1.
end System.Img_Enum_32;
-- --
------------------------------------------------------------------------------
--- Instantiation of System.Image_N for enumeration types whose names table
+-- Instantiation of ``System.Image_N`` for enumeration types whose names table
-- has a length that fits in a 8-bit integer.
with Interfaces;
Names : String;
Indexes : System.Address)
renames Impl.Image_Enumeration;
+ -- Used to compute Enum'Image (Str) where Enum is some enumeration type
+ -- other than those defined in package Standard. Names is a string with
+ -- a lower bound of 1 containing the characters of all the enumeration
+ -- literals concatenated together in sequence. Indexes is the address of
+ -- an array of type array (0 .. N) of Interfaces.Integer_8, where N is the
+ -- number of enumeration literals in the type. The Indexes values are the
+ -- starting subscript of each enumeration literal, indexed by Pos values,
+ -- with an extra entry at the end containing Names'Length + 1. The reason
+ -- that Indexes is passed by address is that the actual type is created on
+ -- the fly by the expander. The desired 'Image value is stored in S
+ -- (1 .. P) and P is set on return. The caller guarantees that S is long
+ -- enough to hold the result and that the lower bound is 1.
end System.Img_Enum_8;
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- ordinary fixed point types up to 32-bit small and mantissa.
+-- This package contains the routines for supporting the ``Image`` attribute
+-- for ordinary fixed point types up to 32-bit small and mantissa.
with Interfaces;
with System.Arith_32;
For0 : Natural;
Aft0 : Natural)
renames Impl.Image_Fixed;
+ -- Computes fixed_type'Image (V), where V is the integer value (in units of
+ -- small) of an ordinary fixed point type with small Num/Den, and stores
+ -- the result in S (1 .. P), updating P on return. The result is computed
+ -- according to the rules for image for fixed-point types (RM 3.5(34)).
+ -- For0 and Aft0 are the values of the Fore and Aft attributes for the
+ -- fixed point type whose mantissa type is Int32 and whose small is
+ -- Num/Den. This function is used only for fixed point whose Small is an
+ -- integer or its reciprocal (see package System.Image_R for the handling
+ -- of other ordinary fixed-point types). The caller guarantees that S is
+ -- long enough to hold the result and has a lower bound of 1.
procedure Set_Image_Fixed32
(V : Int32;
Aft : Natural;
Exp : Natural)
renames Impl.Set_Image_Fixed;
+ -- Sets the image of V, where V is the integer value (in units of small)
+ -- of a fixed point type with small Num/Den, starting at S (P + 1) and
+ -- updating P to point to the last character stored, the caller promises
+ -- that the buffer is large enough and no check is made. Constraint_Error
+ -- will not necessarily be raised if this requirement is violated, since
+ -- it is perfectly valid to compile this unit with checks off. For0 and
+ -- Aft0 are the values of the Fore and Aft attributes for the fixed point
+ -- type whose mantissa type is Int32 and whose small is Num/Den. The Fore,
+ -- Aft and Exp can be set to any valid values for use by Text_IO.Fixed_IO.
end System.Img_Fixed_32;
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- ordinary fixed point types up to 64-bit small and mantissa.
+-- This package contains the routines for supporting the ``Image`` attribute
+-- for ordinary fixed point types up to 64-bit small and mantissa.
with Interfaces;
with System.Arith_64;
For0 : Natural;
Aft0 : Natural)
renames Impl.Image_Fixed;
+ -- Computes fixed_type'Image (V), where V is the integer value (in units of
+ -- small) of an ordinary fixed point type with small Num/Den, and stores
+ -- the result in S (1 .. P), updating P on return. The result is computed
+ -- according to the rules for image for fixed-point types (RM 3.5(34)).
+ -- For0 and Aft0 are the values of the Fore and Aft attributes for the
+ -- fixed point type whose mantissa type is Int64 and whose small is
+ -- Num/Den. This function is used only for fixed point whose Small is an
+ -- integer or its reciprocal (see package System.Image_R for the handling
+ -- of other ordinary fixed-point types). The caller guarantees that S is
+ -- long enough to hold the result and has a lower bound of 1.
procedure Set_Image_Fixed64
(V : Int64;
Aft : Natural;
Exp : Natural)
renames Impl.Set_Image_Fixed;
+ -- Sets the image of V, where V is the integer value (in units of small)
+ -- of a fixed point type with small Num/Den, starting at S (P + 1) and
+ -- updating P to point to the last character stored, the caller promises
+ -- that the buffer is large enough and no check is made. Constraint_Error
+ -- will not necessarily be raised if this requirement is violated, since
+ -- it is perfectly valid to compile this unit with checks off. For0 and
+ -- Aft0 are the values of the Fore and Aft attributes for the fixed point
+ -- type whose mantissa type is Int64 and whose small is Num/Den. The Fore,
+ -- Aft and Exp can be set to any valid values for use by Text_IO.Fixed_IO.
end System.Img_Fixed_64;
------------------------------------------------------------------------------
-- Contains the routine for computing the image in based format of signed and
--- unsigned integers up to Integer for use by Text_IO.Integer_IO and
--- Text_IO.Modular_IO.
+-- unsigned integers up to ``Integer`` for use by ``Ada.Text_IO.Integer_IO``
+-- and ``Ada.Text_IO.Modular_IO``.
with System.Image_B;
with System.Unsigned_Types;
S : out String;
P : in out Natural)
renames Impl.Set_Image_Based_Integer;
+ -- Sets the signed image of V in based format, using base value B (2..16)
+ -- starting at S (P + 1), updating P to point to the last character stored.
+ -- The image includes a leading minus sign if necessary, but no leading
+ -- spaces unless W is positive, in which case leading spaces are output if
+ -- necessary to ensure that the output string is no less than W characters
+ -- long. The caller promises that the buffer is large enough and no check
+ -- is made for this. Constraint_Error will not necessarily be raised if
+ -- this is violated, since it is perfectly valid to compile this unit with
+ -- checks off.
procedure Set_Image_Based_Unsigned
(V : Unsigned;
S : out String;
P : in out Natural)
renames Impl.Set_Image_Based_Unsigned;
+ -- Sets the unsigned image of V in based format, using base value B (2..16)
+ -- starting at S (P + 1), updating P to point to the last character stored.
+ -- The image includes no leading spaces unless W is positive, in which case
+ -- leading spaces are output if necessary to ensure that the output string
+ -- is no less than W characters long. The caller promises that the buffer
+ -- is large enough and no check is made for this. Constraint_Error will not
+ -- necessarily be raised if this is violated, since it is perfectly valid
+ -- to compile this unit with checks off).
end System.Img_BIU;
-- Boolean'Image
+-- This package provides support for ``Image`` attribute on ``Boolean``. The
+-- compiler performs direct calls to this unit to implement the attribute.
+
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- setting the corresponding assertion policy to Ignore. Postconditions and
and then (if V then S'Length >= 4 else S'Length >= 5),
Post => (if V then P = 4 else P = 5)
and then System.Val_Spec.Is_Boolean_Image_Ghost (S (1 .. P), V);
- -- Computes Boolean'Image (V) and stores the result in S (1 .. P)
- -- setting the resulting value of P. The caller guarantees that S
- -- is long enough to hold the result, and that S'First is 1.
+ -- Computes Boolean'Image (``V``) and stores the result in
+ -- ``S`` (1 .. ``P``) setting the resulting value of ``P``. The caller
+ -- guarantees that ``S`` is long enough to hold the result, and that
+ -- ``S``'First is 1.
end System.Img_Bool;
-- Character'Image
+-- This package provides support for ``Image`` attribute on ``Character``. The
+-- compiler performs direct calls to this unit to implement the attribute.
+
package System.Img_Char is
pragma Pure;
(V : Character;
S : in out String;
P : out Natural);
- -- Computes Character'Image (V) and stores the result in S (1 .. P)
- -- setting the resulting value of P. The caller guarantees that S is
- -- long enough to hold the result, and that S'First is 1.
+ -- Computes Character'Image (``V``) and stores the result in
+ -- ``S`` (1 .. ``P``) setting the resulting value of ``P``. The caller
+ -- guarantees that ``S`` is long enough to hold the result, and that
+ -- ``S``'First is 1.
procedure Image_Character_05
(V : Character;
S : in out String;
P : out Natural);
- -- Computes Character'Image (V) and stores the result in S (1 .. P)
- -- setting the resulting value of P. The caller guarantees that S is
- -- long enough to hold the result, and that S'First is 1. This version
- -- is for use in Ada 2005 and beyond, where soft hyphen is a non-graphic
- -- and results in "SOFT_HYPHEN" as the output.
+ -- Computes Character'Image (``V``) and stores the result in
+ -- ``S`` (1 .. ``P``) setting the resulting value of ``P``. The caller
+ -- guarantees that ``S`` is long enough to hold the result, and that
+ -- ``S``'First is 1.
+ --
+ -- This version is for use in Ada 2005 and beyond, where soft hyphen is
+ -- a non-graphic and results in "SOFT_HYPHEN" as the output.
end System.Img_Char;
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- signed integer types up to Integer, and also for conversion operations
--- required in Text_IO.Integer_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Integer_IO`` conversions routines for signed integer
+-- types up to Size ``Integer'Size``.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
S : in out String;
P : out Natural)
renames Impl.Image_Integer;
+ -- Computes Integer'Image (``V``) and stores the result in
+ -- ``S`` (1 .. ``P``) setting the resulting value of ``P``.
+ -- The caller guarantees that ``S`` is long enough to hold the result,
+ -- and that ``S``'First is 1.
+ --
+ -- If ``V`` is not negative, the subprogram writes the leading blank in
+ -- ``S``. It then calls *Set_Image_Integer* unconditionally.
procedure Set_Image_Integer
(V : Integer;
S : in out String;
P : in out Natural)
renames Impl.Set_Image_Integer;
+ -- Stores the image of ``V`` in ``S`` starting at ``S`` (``P`` + 1), ``P``
+ -- is updated to point to the last character stored. The value stored is
+ -- identical to the value of Integer'Image (``V``) except that no leading
+ -- space is stored when ``V`` is non-negative. The caller guarantees that
+ -- ``S`` is long enough to hold the result. ``S`` need not have a lower
+ -- bound of 1.
+ --
+ -- If ``V`` is negative, the subprogram writes the leading '-' character,
+ -- otherwise work with -``V`` (always work with negative value to avoid
+ -- overflow: the largest negative number is not a special case).
+ --
+ -- This subprogram then uses recursion: if the value is equal or less than
+ -- -10, recurse with the value divided by 10. Then add the digit for the
+ -- remainder.
end System.Img_Int;
-- --
------------------------------------------------------------------------------
--- Contains the routine for computing the image in based format of signed and
--- unsigned integers larger than Integer for use by Text_IO.Integer_IO and
--- Text_IO.Modular_IO.
+-- Contains the routine for computing the image in based format
+-- of signed and unsigned integers larger than `Integer` for use
+-- by ``Ada.Text_IO.Integer_IO`` and ``Text_IO.Modular_IO``.
with System.Image_B;
with System.Unsigned_Types;
S : out String;
P : in out Natural)
renames Impl.Set_Image_Based_Integer;
+ -- Sets the signed image of V in based format, using base value B (2..16)
+ -- starting at S (P + 1), updating P to point to the last character stored.
+ -- The image includes a leading minus sign if necessary, but no leading
+ -- spaces unless W is positive, in which case leading spaces are output if
+ -- necessary to ensure that the output string is no less than W characters
+ -- long. The caller promises that the buffer is large enough and no check
+ -- is made for this. Constraint_Error will not necessarily be raised if
+ -- this is violated, since it is perfectly valid to compile this unit with
+ -- checks off.
procedure Set_Image_Based_Long_Long_Unsigned
(V : Long_Long_Unsigned;
S : out String;
P : in out Natural)
renames Impl.Set_Image_Based_Unsigned;
+ -- Sets the unsigned image of V in based format, using base value B (2..16)
+ -- starting at S (P + 1), updating P to point to the last character stored.
+ -- The image includes no leading spaces unless W is positive, in which case
+ -- leading spaces are output if necessary to ensure that the output string
+ -- is no less than W characters long. The caller promises that the buffer
+ -- is large enough and no check is made for this. Constraint_Error will not
+ -- necessarily be raised if this is violated, since it is perfectly valid
+ -- to compile this unit with checks off).
end System.Img_LLB;
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- signed integer types larger than Integer, and also for conversion
--- operations required in Text_IO.Integer_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Integer_IO`` conversions routines for signed integer
+-- types larger than Size ``Integer'Size``.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
S : in out String;
P : out Natural)
renames Impl.Image_Integer;
+ -- Computes Long_Long_Integer'Image (``V``) and stores the result in
+ -- ``S`` (1 .. ``P``) setting the resulting value of ``P``. The caller
+ -- guarantees that ``S`` is long enough to hold the result, and that
+ -- ``S``'First is 1.
+ --
+ -- If ``V`` is not negative, the subprogram writes the leading blank in
+ -- ``S``. It then calls *Set_Image_Long_Long_Integer*.
procedure Set_Image_Long_Long_Integer
(V : Long_Long_Integer;
S : in out String;
P : in out Natural)
renames Impl.Set_Image_Integer;
+ -- Stores the image of ``V`` in ``S`` starting at ``S`` (``P`` + 1),
+ -- ``P`` is updated to point to the last character stored. The value
+ -- stored is identical to the value of Long_Long_Integer'Image (``V``)
+ -- except that no leading space is stored when ``V`` is non-negative. The
+ -- caller guarantees that ``S`` is long enough to hold the result. ``S``
+ -- need not have a lower bound of 1.
+ --
+ -- If ``V`` is negative, the subprogram writes the leading '-' character,
+ -- otherwise work with -``V`` (always work with negative value to avoid
+ -- overflow: the largest negative number is not a special case).
+ --
+ -- This subprogram then uses recursion: if the value is equal or less than
+ -- -10, recurse with the value divided by 10. Then add the digit for the
+ -- remainder.
end System.Img_LLI;
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- modular integer types larger than Unsigned, and also for conversion
--- operations required in Text_IO.Modular_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Modular_IO`` conversions routines for unsigned (modular)
+-- integer types larger than Size ``Unsigned'Size``.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
S : in out String;
P : out Natural)
renames Impl.Image_Unsigned;
+ -- Computes Long_Long_Unsigned'Image (``V``) and stores the result in
+ -- ``S`` (1 .. ``P``) setting the resulting value of ``P``. The caller
+ -- guarantees that ``S`` is long enough to hold the result, and that
+ -- ``S``'First is 1.
+ --
+ -- The subprogram writes the leading blank in ``S`` and calls
+ -- *Set_Image_Long_Long_Unsigned*.
procedure Set_Image_Long_Long_Unsigned
(V : Long_Long_Unsigned;
S : in out String;
P : in out Natural)
renames Impl.Set_Image_Unsigned;
+ -- Stores the image of ``V`` in ``S`` starting at ``S`` (``P`` + 1),
+ -- ``P`` is updated to point to the last character stored. The value
+ -- stored is identical to the value of Long_Long_Unsigned'Image (``V``)
+ -- except that no leading space is stored.
+ -- The caller guarantees that ``S`` is long enough to hold the result.
+ -- ``S`` need not have a lower bound of 1.
+ --
+ -- This subprogram uses recursion: if the value is equal or greater than
+ -- 10, recurse with the value divided by 10. Then add the digit for the
+ -- remainder.
end System.Img_LLU;
S : out String;
P : in out Natural)
renames Impl.Set_Image_Width_Integer;
+ -- Sets the signed image of V in based format, using base value B (2..16)
+ -- starting at S (P + 1), updating P to point to the last character stored.
+ -- The image includes a leading minus sign if necessary, but no leading
+ -- spaces unless W is positive, in which case leading spaces are output if
+ -- necessary to ensure that the output string is no less than W characters
+ -- long. The caller promises that the buffer is large enough and no check
+ -- is made for this. Constraint_Error will not necessarily be raised if
+ -- this is violated, since it is perfectly valid to compile this unit with
+ -- checks off.
procedure Set_Image_Width_Long_Long_Unsigned
(V : Long_Long_Unsigned;
S : out String;
P : in out Natural)
renames Impl.Set_Image_Width_Unsigned;
+ -- Sets the unsigned image of V in based format, using base value B (2..16)
+ -- starting at S (P + 1), updating P to point to the last character stored.
+ -- The image includes no leading spaces unless W is positive, in which case
+ -- leading spaces are output if necessary to ensure that the output string
+ -- is no less than W characters long. The caller promises that the buffer
+ -- is large enough and no check is made for this. Constraint_Error will not
+ -- necessarily be raised if this is violated, since it is perfectly valid
+ -- to compile this unit with checks off).
end System.Img_LLW;
-- --
------------------------------------------------------------------------------
+-- Image for fixed and float types (also used for Float_IO/Fixed_IO output)
+
-- This obsolete package is preserved for the sake of backward compatibility
with System.Img_LLF;
Aft : Natural;
Exp : Natural)
renames System.Img_LLF.Set_Image_Long_Long_Float;
+ -- Sets the image of ``V`` starting at ``S`` (``P`` + 1), updating ``P``
+ -- to point to the last character stored, the caller promises that the
+ -- buffer is large enough and no check is made for this. Constraint_Error
+ -- will not necessarily be raised if this is violated, since it is
+ -- perfectly valid to compile this unit with checks off). The ``Fore``,
+ -- ``Aft`` and ``Exp`` values can be set to any valid values for the case
+ -- of use from Text_IO. Note that no space is stored at the start for
+ -- non-negative values.
end System.Img_Real;
-- --
------------------------------------------------------------------------------
--- This package contains the routines for supporting the Image attribute for
--- modular integer types up to Unsigned, and also for conversion operations
--- required in Text_IO.Modular_IO for such types.
+-- This package provides the subprograms supporting the ``Image`` attribute
+-- and ``Ada.Text_IO.Modular_IO`` conversions routines for modular integer
+-- types up to size ``Unsigned'Size``.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
S : in out String;
P : out Natural)
renames Impl.Image_Unsigned;
+ -- Computes Unsigned'Image (``V``) and stores the result in
+ -- ``S`` (1 .. ``P``) setting the resulting value of ``P``. The caller
+ -- guarantees that ``S`` is long enough to hold the result, and that
+ -- ``S``'First is 1.
+ --
+ -- The subprogram writes the leading blank in ``S`` and calls
+ -- *Set_Image_Unsigned*.
procedure Set_Image_Unsigned
(V : Unsigned;
S : in out String;
P : in out Natural)
renames Impl.Set_Image_Unsigned;
+ -- Stores the image of ``V`` in ``S`` starting at ``S`` (``P`` + 1), ``P``
+ -- is updated to point to the last character stored. The value stored is
+ -- identical to the value of Unsigned'Image (``V``) except that no leading
+ -- space is stored. The caller guarantees that ``S`` is long enough to hold
+ -- the result. ``S`` need not have a lower bound of 1.
+ --
+ -- This subprogram uses recursion: if the value is equal or greater than
+ -- 10, recurse with the value divided by 10. Then add the digit for the
+ -- remainder.
end System.Img_Uns;
-- --
------------------------------------------------------------------------------
--- This package provides some common utilities used by the s-imgxxx files
+-- This package provides some common utilities used by the `System.Img_*`
+-- packages. It contains subprograms to set the decimal digits for a string
+-- and set the string for a floating-point invalid value.
package System.Img_Util is
------------------------------------------------------------------------------
-- Contains the routine for computing the image of signed and unsigned
--- integers up to Integer for use by Text_IO.Integer_IO and
--- Text_IO.Modular_IO.
+-- integers up to Integer for use by ``Ada.Text_IO.Integer_IO`` and
+-- ``Ada.Text_IO.Modular_IO``.
with System.Image_W;
with System.Unsigned_Types;
------------------------------------------------------------------------------
-- This package provides machine code support, both for intrinsic machine
--- operations, and also for machine code statements. See GNAT documentation
--- for full details.
+-- operations, and also for machine code statements. It implements the
+-- *System.Machine_code* package defined in ARM 13.8 and GNAT Reference Manual
+-- (chapter 'Implementation of Specific Ada Features', 'Machine Code
+-- Insertions').
package System.Machine_Code
with SPARK_Mode => Off
pragma No_Elaboration_Code_All;
pragma Pure;
- -- All identifiers in this unit are implementation defined
-
pragma Implementation_Defined;
+ -- All identifiers in this unit are implementation defined
type Asm_Input_Operand is private;
type Asm_Output_Operand is private;
No_Input_Operands : constant Asm_Input_Operand;
No_Output_Operands : constant Asm_Output_Operand;
+ -- These constants are used as default value to denote respectively no
+ -- input operands and no output operands.
type Asm_Input_Operand_List is
array (Integer range <>) of Asm_Input_Operand;
type Asm_Output_Operand_List is
array (Integer range <>) of Asm_Output_Operand;
+ -- The types *Asm_Input_Operand_List* and *Asm_Output_Operand_List* are
+ -- arrays of respectively *Asm_Input_Operand* and *Asm_Output_Operand*.
+ -- They are used to describe lists of operands for the Asm subprograms.
type Asm_Insn is private;
-- This type is not used directly. It is declared only so that the
Inputs : Asm_Input_Operand := No_Input_Operands;
Clobber : String := "";
Volatile : Boolean := False) return Asm_Insn;
+ -- The parameters are described in the GNAT Reference Manual [GRM].
+ --
+ -- These are intrinsic subprograms, fully implemented by the compiler.
pragma Import (Intrinsic, Asm);
-- --
------------------------------------------------------------------------------
+-- This is the top level unit for multiprocessor task support as defined by
+-- ARM D.16. It provides the base types to enumerate CPUs and the
+-- functionality to get the number of CPUs on the current system.
+
package System.Multiprocessors is
pragma Preelaborate (Multiprocessors);
package System.Pack_03 is
pragma Preelaborate;
+ -- 3-bit element type definition
+
Bits : constant := 3;
type Bits_03 is mod 2 ** Bits;
package System.Pack_05 is
pragma Preelaborate;
+ -- 5-bit element type definition
+
Bits : constant := 5;
type Bits_05 is mod 2 ** Bits;
package System.Pack_06 is
pragma Preelaborate;
+ -- 6-bit element type definition
+
Bits : constant := 6;
type Bits_06 is mod 2 ** Bits;
package System.Pack_07 is
pragma Preelaborate;
+ -- 7-bit element type definition
+
Bits : constant := 7;
type Bits_07 is mod 2 ** Bits;
package System.Pack_09 is
pragma Preelaborate;
+ -- 9-bit element type definition
+
Bits : constant := 9;
type Bits_09 is mod 2 ** Bits;
package System.Pack_10 is
pragma Preelaborate;
+ -- 10-bit element type definition
+
Bits : constant := 10;
type Bits_10 is mod 2 ** Bits;
package System.Pack_100 is
pragma Preelaborate;
+ -- 100-bit element type definition
+
Bits : constant := 100;
type Bits_100 is mod 2 ** Bits;
package System.Pack_101 is
pragma Preelaborate;
+ -- 101-bit element type definition
+
Bits : constant := 101;
type Bits_101 is mod 2 ** Bits;
package System.Pack_102 is
pragma Preelaborate;
+ -- 102-bit element type definition
+
Bits : constant := 102;
type Bits_102 is mod 2 ** Bits;
package System.Pack_103 is
pragma Preelaborate;
+ -- 103-bit element type definition
+
Bits : constant := 103;
type Bits_103 is mod 2 ** Bits;
package System.Pack_104 is
pragma Preelaborate;
+ -- 104-bit element type definition
+
Bits : constant := 104;
type Bits_104 is mod 2 ** Bits;
package System.Pack_105 is
pragma Preelaborate;
+ -- 105-bit element type definition
+
Bits : constant := 105;
type Bits_105 is mod 2 ** Bits;
package System.Pack_106 is
pragma Preelaborate;
+ -- 106-bit element type definition
+
Bits : constant := 106;
type Bits_106 is mod 2 ** Bits;
package System.Pack_107 is
pragma Preelaborate;
+ -- 107-bit element type definition
+
Bits : constant := 107;
type Bits_107 is mod 2 ** Bits;
package System.Pack_108 is
pragma Preelaborate;
+ -- 108-bit element type definition
+
Bits : constant := 108;
type Bits_108 is mod 2 ** Bits;
package System.Pack_109 is
pragma Preelaborate;
+ -- 109-bit element type definition
+
Bits : constant := 109;
type Bits_109 is mod 2 ** Bits;
package System.Pack_11 is
pragma Preelaborate;
+ -- 11-bit element type definition
+
Bits : constant := 11;
type Bits_11 is mod 2 ** Bits;
package System.Pack_110 is
pragma Preelaborate;
+ -- 110-bit element type definition
+
Bits : constant := 110;
type Bits_110 is mod 2 ** Bits;
package System.Pack_111 is
pragma Preelaborate;
+ -- 111-bit element type definition
+
Bits : constant := 111;
type Bits_111 is mod 2 ** Bits;
package System.Pack_112 is
pragma Preelaborate;
+ -- 112-bit element type definition
+
Bits : constant := 112;
type Bits_112 is mod 2 ** Bits;
package System.Pack_113 is
pragma Preelaborate;
+ -- 113-bit element type definition
+
Bits : constant := 113;
type Bits_113 is mod 2 ** Bits;
package System.Pack_114 is
pragma Preelaborate;
+ -- 114-bit element type definition
+
Bits : constant := 114;
type Bits_114 is mod 2 ** Bits;
package System.Pack_115 is
pragma Preelaborate;
+ -- 115-bit element type definition
+
Bits : constant := 115;
type Bits_115 is mod 2 ** Bits;
package System.Pack_116 is
pragma Preelaborate;
+ -- 116-bit element type definition
+
Bits : constant := 116;
type Bits_116 is mod 2 ** Bits;
package System.Pack_117 is
pragma Preelaborate;
+ -- 117-bit element type definition
+
Bits : constant := 117;
type Bits_117 is mod 2 ** Bits;
package System.Pack_118 is
pragma Preelaborate;
+ -- 118-bit element type definition
+
Bits : constant := 118;
type Bits_118 is mod 2 ** Bits;
package System.Pack_119 is
pragma Preelaborate;
+ -- 119-bit element type definition
+
Bits : constant := 119;
type Bits_119 is mod 2 ** Bits;
package System.Pack_12 is
pragma Preelaborate;
+ -- 12-bit element type definition
+
Bits : constant := 12;
type Bits_12 is mod 2 ** Bits;
package System.Pack_120 is
pragma Preelaborate;
+ -- 120-bit element type definition
+
Bits : constant := 120;
type Bits_120 is mod 2 ** Bits;
package System.Pack_121 is
pragma Preelaborate;
+ -- 121-bit element type definition
+
Bits : constant := 121;
type Bits_121 is mod 2 ** Bits;
package System.Pack_122 is
pragma Preelaborate;
+ -- 122-bit element type definition
+
Bits : constant := 122;
type Bits_122 is mod 2 ** Bits;
package System.Pack_123 is
pragma Preelaborate;
+ -- 123-bit element type definition
+
Bits : constant := 123;
type Bits_123 is mod 2 ** Bits;
package System.Pack_124 is
pragma Preelaborate;
+ -- 124-bit element type definition
+
Bits : constant := 124;
type Bits_124 is mod 2 ** Bits;
package System.Pack_125 is
pragma Preelaborate;
+ -- 125-bit element type definition
+
Bits : constant := 125;
type Bits_125 is mod 2 ** Bits;
package System.Pack_126 is
pragma Preelaborate;
+ -- 126-bit element type definition
+
Bits : constant := 126;
type Bits_126 is mod 2 ** Bits;
package System.Pack_127 is
pragma Preelaborate;
+ -- 127-bit element type definition
+
Bits : constant := 127;
type Bits_127 is mod 2 ** Bits;
package System.Pack_13 is
pragma Preelaborate;
+ -- 13-bit element type definition
+
Bits : constant := 13;
type Bits_13 is mod 2 ** Bits;
package System.Pack_14 is
pragma Preelaborate;
+ -- 14-bit element type definition
+
Bits : constant := 14;
type Bits_14 is mod 2 ** Bits;
package System.Pack_15 is
pragma Preelaborate;
+ -- 15-bit element type definition
+
Bits : constant := 15;
type Bits_15 is mod 2 ** Bits;
package System.Pack_17 is
pragma Preelaborate;
+ -- 17-bit element type definition
+
Bits : constant := 17;
type Bits_17 is mod 2 ** Bits;
package System.Pack_18 is
pragma Preelaborate;
+ -- 18-bit element type definition
+
Bits : constant := 18;
type Bits_18 is mod 2 ** Bits;
package System.Pack_19 is
pragma Preelaborate;
+ -- 19-bit element type definition
+
Bits : constant := 19;
type Bits_19 is mod 2 ** Bits;
package System.Pack_20 is
pragma Preelaborate;
+ -- 20-bit element type definition
+
Bits : constant := 20;
type Bits_20 is mod 2 ** Bits;
package System.Pack_21 is
pragma Preelaborate;
+ -- 21-bit element type definition
+
Bits : constant := 21;
type Bits_21 is mod 2 ** Bits;
package System.Pack_22 is
pragma Preelaborate;
+ -- 22-bit element type definition
+
Bits : constant := 22;
type Bits_22 is mod 2 ** Bits;
package System.Pack_23 is
pragma Preelaborate;
+ -- 23-bit element type definition
+
Bits : constant := 23;
type Bits_23 is mod 2 ** Bits;
package System.Pack_24 is
pragma Preelaborate;
+ -- 24-bit element type definition
+
Bits : constant := 24;
type Bits_24 is mod 2 ** Bits;
package System.Pack_25 is
pragma Preelaborate;
+ -- 25-bit element type definition
+
Bits : constant := 25;
type Bits_25 is mod 2 ** Bits;
package System.Pack_26 is
pragma Preelaborate;
+ -- 26-bit element type definition
+
Bits : constant := 26;
type Bits_26 is mod 2 ** Bits;
package System.Pack_27 is
pragma Preelaborate;
+ -- 27-bit element type definition
+
Bits : constant := 27;
type Bits_27 is mod 2 ** Bits;
package System.Pack_28 is
pragma Preelaborate;
+ -- 28-bit element type definition
+
Bits : constant := 28;
type Bits_28 is mod 2 ** Bits;
package System.Pack_29 is
pragma Preelaborate;
+ -- 29-bit element type definition
+
Bits : constant := 29;
type Bits_29 is mod 2 ** Bits;
package System.Pack_30 is
pragma Preelaborate;
+ -- 30-bit element type definition
+
Bits : constant := 30;
type Bits_30 is mod 2 ** Bits;
package System.Pack_31 is
pragma Preelaborate;
+ -- 31-bit element type definition
+
Bits : constant := 31;
type Bits_31 is mod 2 ** Bits;
package System.Pack_33 is
pragma Preelaborate;
+ -- 33-bit element type definition
+
Bits : constant := 33;
type Bits_33 is mod 2 ** Bits;
package System.Pack_34 is
pragma Preelaborate;
+ -- 34-bit element type definition
+
Bits : constant := 34;
type Bits_34 is mod 2 ** Bits;
package System.Pack_35 is
pragma Preelaborate;
+ -- 35-bit element type definition
+
Bits : constant := 35;
type Bits_35 is mod 2 ** Bits;
package System.Pack_36 is
pragma Preelaborate;
+ -- 36-bit element type definition
+
Bits : constant := 36;
type Bits_36 is mod 2 ** Bits;
package System.Pack_37 is
pragma Preelaborate;
+ -- 37-bit element type definition
+
Bits : constant := 37;
type Bits_37 is mod 2 ** Bits;
package System.Pack_38 is
pragma Preelaborate;
+ -- 38-bit element type definition
+
Bits : constant := 38;
type Bits_38 is mod 2 ** Bits;
package System.Pack_39 is
pragma Preelaborate;
+ -- 39-bit element type definition
+
Bits : constant := 39;
type Bits_39 is mod 2 ** Bits;
package System.Pack_40 is
pragma Preelaborate;
+ -- 40-bit element type definition
+
Bits : constant := 40;
type Bits_40 is mod 2 ** Bits;
package System.Pack_41 is
pragma Preelaborate;
+ -- 41-bit element type definition
+
Bits : constant := 41;
type Bits_41 is mod 2 ** Bits;
package System.Pack_42 is
pragma Preelaborate;
+ -- 42-bit element type definition
+
Bits : constant := 42;
type Bits_42 is mod 2 ** Bits;
package System.Pack_43 is
pragma Preelaborate;
+ -- 43-bit element type definition
+
Bits : constant := 43;
type Bits_43 is mod 2 ** Bits;
package System.Pack_44 is
pragma Preelaborate;
+ -- 44-bit element type definition
+
Bits : constant := 44;
type Bits_44 is mod 2 ** Bits;
package System.Pack_45 is
pragma Preelaborate;
+ -- 45-bit element type definition
+
Bits : constant := 45;
type Bits_45 is mod 2 ** Bits;
package System.Pack_46 is
pragma Preelaborate;
+ -- 46-bit element type definition
+
Bits : constant := 46;
type Bits_46 is mod 2 ** Bits;
package System.Pack_47 is
pragma Preelaborate;
+ -- 47-bit element type definition
+
Bits : constant := 47;
type Bits_47 is mod 2 ** Bits;
package System.Pack_48 is
pragma Preelaborate;
+ -- 48-bit element type definition
+
Bits : constant := 48;
type Bits_48 is mod 2 ** Bits;
package System.Pack_49 is
pragma Preelaborate;
+ -- 49-bit element type definition
+
Bits : constant := 49;
type Bits_49 is mod 2 ** Bits;
package System.Pack_50 is
pragma Preelaborate;
+ -- 50-bit element type definition
+
Bits : constant := 50;
type Bits_50 is mod 2 ** Bits;
package System.Pack_51 is
pragma Preelaborate;
+ -- 51-bit element type definition
+
Bits : constant := 51;
type Bits_51 is mod 2 ** Bits;
package System.Pack_52 is
pragma Preelaborate;
+ -- 52-bit element type definition
+
Bits : constant := 52;
type Bits_52 is mod 2 ** Bits;
package System.Pack_53 is
pragma Preelaborate;
+ -- 53-bit element type definition
+
Bits : constant := 53;
type Bits_53 is mod 2 ** Bits;
package System.Pack_54 is
pragma Preelaborate;
+ -- 54-bit element type definition
+
Bits : constant := 54;
type Bits_54 is mod 2 ** Bits;
package System.Pack_55 is
pragma Preelaborate;
+ -- 55-bit element type definition
+
Bits : constant := 55;
type Bits_55 is mod 2 ** Bits;
package System.Pack_56 is
pragma Preelaborate;
+ -- 56-bit element type definition
+
Bits : constant := 56;
type Bits_56 is mod 2 ** Bits;
package System.Pack_57 is
pragma Preelaborate;
+ -- 57-bit element type definition
+
Bits : constant := 57;
type Bits_57 is mod 2 ** Bits;
package System.Pack_58 is
pragma Preelaborate;
+ -- 58-bit element type definition
+
Bits : constant := 58;
type Bits_58 is mod 2 ** Bits;
package System.Pack_59 is
pragma Preelaborate;
+ -- 59-bit element type definition
+
Bits : constant := 59;
type Bits_59 is mod 2 ** Bits;
package System.Pack_60 is
pragma Preelaborate;
+ -- 60-bit element type definition
+
Bits : constant := 60;
type Bits_60 is mod 2 ** Bits;
package System.Pack_61 is
pragma Preelaborate;
+ -- 61-bit element type definition
+
Bits : constant := 61;
type Bits_61 is mod 2 ** Bits;
package System.Pack_62 is
pragma Preelaborate;
+ -- 62-bit element type definition
+
Bits : constant := 62;
type Bits_62 is mod 2 ** Bits;
package System.Pack_63 is
pragma Preelaborate;
+ -- 63-bit element type definition
+
Bits : constant := 63;
type Bits_63 is mod 2 ** Bits;
package System.Pack_65 is
pragma Preelaborate;
+ -- 65-bit element type definition
+
Bits : constant := 65;
type Bits_65 is mod 2 ** Bits;
package System.Pack_66 is
pragma Preelaborate;
+ -- 66-bit element type definition
+
Bits : constant := 66;
type Bits_66 is mod 2 ** Bits;
package System.Pack_67 is
pragma Preelaborate;
+ -- 67-bit element type definition
+
Bits : constant := 67;
type Bits_67 is mod 2 ** Bits;
package System.Pack_68 is
pragma Preelaborate;
+ -- 68-bit element type definition
+
Bits : constant := 68;
type Bits_68 is mod 2 ** Bits;
package System.Pack_69 is
pragma Preelaborate;
+ -- 69-bit element type definition
+
Bits : constant := 69;
type Bits_69 is mod 2 ** Bits;
package System.Pack_70 is
pragma Preelaborate;
+ -- 70-bit element type definition
+
Bits : constant := 70;
type Bits_70 is mod 2 ** Bits;
package System.Pack_71 is
pragma Preelaborate;
+ -- 71-bit element type definition
+
Bits : constant := 71;
type Bits_71 is mod 2 ** Bits;
package System.Pack_72 is
pragma Preelaborate;
+ -- 72-bit element type definition
+
Bits : constant := 72;
type Bits_72 is mod 2 ** Bits;
package System.Pack_73 is
pragma Preelaborate;
+ -- 73-bit element type definition
+
Bits : constant := 73;
type Bits_73 is mod 2 ** Bits;
package System.Pack_74 is
pragma Preelaborate;
+ -- 74-bit element type definition
+
Bits : constant := 74;
type Bits_74 is mod 2 ** Bits;
package System.Pack_75 is
pragma Preelaborate;
+ -- 75-bit element type definition
+
Bits : constant := 75;
type Bits_75 is mod 2 ** Bits;
package System.Pack_76 is
pragma Preelaborate;
+ -- 76-bit element type definition
+
Bits : constant := 76;
type Bits_76 is mod 2 ** Bits;
package System.Pack_77 is
pragma Preelaborate;
+ -- 77-bit element type definition
+
Bits : constant := 77;
type Bits_77 is mod 2 ** Bits;
package System.Pack_78 is
pragma Preelaborate;
+ -- 78-bit element type definition
+
Bits : constant := 78;
type Bits_78 is mod 2 ** Bits;
package System.Pack_79 is
pragma Preelaborate;
+ -- 79-bit element type definition
+
Bits : constant := 79;
type Bits_79 is mod 2 ** Bits;
package System.Pack_80 is
pragma Preelaborate;
+ -- 80-bit element type definition
+
Bits : constant := 80;
type Bits_80 is mod 2 ** Bits;
package System.Pack_81 is
pragma Preelaborate;
+ -- 81-bit element type definition
+
Bits : constant := 81;
type Bits_81 is mod 2 ** Bits;
package System.Pack_82 is
pragma Preelaborate;
+ -- 82-bit element type definition
+
Bits : constant := 82;
type Bits_82 is mod 2 ** Bits;
package System.Pack_83 is
pragma Preelaborate;
+ -- 83-bit element type definition
+
Bits : constant := 83;
type Bits_83 is mod 2 ** Bits;
package System.Pack_84 is
pragma Preelaborate;
+ -- 84-bit element type definition
+
Bits : constant := 84;
type Bits_84 is mod 2 ** Bits;
package System.Pack_85 is
pragma Preelaborate;
+ -- 85-bit element type definition
+
Bits : constant := 85;
type Bits_85 is mod 2 ** Bits;
package System.Pack_86 is
pragma Preelaborate;
+ -- 86-bit element type definition
+
Bits : constant := 86;
type Bits_86 is mod 2 ** Bits;
package System.Pack_87 is
pragma Preelaborate;
+ -- 87-bit element type definition
+
Bits : constant := 87;
type Bits_87 is mod 2 ** Bits;
package System.Pack_88 is
pragma Preelaborate;
+ -- 88-bit element type definition
+
Bits : constant := 88;
type Bits_88 is mod 2 ** Bits;
package System.Pack_89 is
pragma Preelaborate;
+ -- 89-bit element type definition
+
Bits : constant := 89;
type Bits_89 is mod 2 ** Bits;
package System.Pack_90 is
pragma Preelaborate;
+ -- 90-bit element type definition
+
Bits : constant := 90;
type Bits_90 is mod 2 ** Bits;
package System.Pack_91 is
pragma Preelaborate;
+ -- 91-bit element type definition
+
Bits : constant := 91;
type Bits_91 is mod 2 ** Bits;
package System.Pack_92 is
pragma Preelaborate;
+ -- 92-bit element type definition
+
Bits : constant := 92;
type Bits_92 is mod 2 ** Bits;
package System.Pack_93 is
pragma Preelaborate;
+ -- 93-bit element type definition
+
Bits : constant := 93;
type Bits_93 is mod 2 ** Bits;
package System.Pack_94 is
pragma Preelaborate;
+ -- 94-bit element type definition
+
Bits : constant := 94;
type Bits_94 is mod 2 ** Bits;
package System.Pack_95 is
pragma Preelaborate;
+ -- 95-bit element type definition
+
Bits : constant := 95;
type Bits_95 is mod 2 ** Bits;
package System.Pack_96 is
pragma Preelaborate;
+ -- 96-bit element type definition
+
Bits : constant := 96;
type Bits_96 is mod 2 ** Bits;
package System.Pack_97 is
pragma Preelaborate;
+ -- 97-bit element type definition
+
Bits : constant := 97;
type Bits_97 is mod 2 ** Bits;
package System.Pack_98 is
pragma Preelaborate;
+ -- 98-bit element type definition
+
Bits : constant := 98;
type Bits_98 is mod 2 ** Bits;
package System.Pack_99 is
pragma Preelaborate;
+ -- 99-bit element type definition
+
Bits : constant := 99;
type Bits_99 is mod 2 ** Bits;
-- Default version used when no target-specific version is provided
--- This package defines some system dependent parameters for GNAT. These
--- are values that are referenced by the runtime library and are therefore
--- relevant to the target machine.
+-- This package defines a number of system-dependent parameters for GNAT.
+-- These are values that are referenced by the runtime library and are
+-- therefore relevant to the target machine. This includes the default and
+-- minimum size and the length of a task name.
-- The parameters whose value is defined in the spec are not generally
-- expected to be changed. If they are changed, it will be necessary to
------------------------------------------------------------------------------
-- This package defines the set of restriction identifiers. It is a generic
--- package that is instantiated by the compiler/binder in package Rident, and
--- is instantiated in package System.Restrictions for use at run-time.
+-- package that is instantiated by the compiler/binder in package ``Rident``,
+-- and is instantiated in package ``System.Restrictions`` for use at
+-- run-time.
-- The reason that we make this a generic package is so that in the case of
-- the instantiation in Rident for use at compile time and bind time, we can
-- --
------------------------------------------------------------------------------
+-- This is the top level unit of the SPARK package. Its children
+-- contain helper functions to aid proofs.
+
package System.SPARK with
SPARK_Mode,
Pure
-- --
------------------------------------------------------------------------------
--- By and So are connectors used to manually help the proof of assertions by
--- introducing intermediate steps. They can only be used inside pragmas
--- Assert or Assert_And_Cut. They are handled in the following way:
---
--- * If A and B are two boolean expressions, proving By (A, B) requires
--- proving B, the premise, and then A assuming B, the side-condition. When
--- By (A, B) is assumed on the other hand, we only assume A. B is used
--- for the proof, but is not visible afterward.
---
--- * If A and B are two boolean expressions, proving So (A, B) requires
--- proving A, the premise, and then B assuming A, the side-condition. When
--- So (A, B) is assumed both A and B are assumed to be true.
+-- This package provides connectors used to manually help the proof of
+-- assertions by introducing intermediate steps. They can only be used inside
+-- pragmas Assert or Assert_And_Cut.
package System.SPARK.Cut_Operations with
SPARK_Mode,
function By (Consequence, Premise : Boolean) return Boolean with
Ghost,
Global => null;
+ -- If A and B are two boolean expressions, proving By (A, B) requires
+ -- proving B, the premise, and then A assuming B, the side-condition. When
+ -- By (A, B) is assumed on the other hand, we only assume A. B is used
+ -- for the proof, but is not visible afterward.
function So (Premise, Consequence : Boolean) return Boolean with
Ghost,
Global => null;
+ -- If A and B are two boolean expressions, proving So (A, B) requires
+ -- proving A, the premise, and then B assuming A, the side-condition. When
+ -- So (A, B) is assumed both A and B are assumed to be true.
end System.SPARK.Cut_Operations;
-- --
------------------------------------------------------------------------------
+-- This package provides the ``Storage_Elements`` package as defined by the
+-- Ada ARM 13.7.1 to allow for arithmetic operations on memory addresses.
+
-- Warning: declarations in this package are ambiguous with respect to the
-- extra declarations that can be introduced into System using Extend_System.
-- It is a good idea to avoid use clauses for this package.
type Storage_Offset is range -Memory_Size / 2 .. Memory_Size / 2 - 1;
subtype Storage_Count is Storage_Offset range 0 .. Storage_Offset'Last;
+ -- *Storage_Count* is a subtype of *Storage_Offset* with only the null or
+ -- positive values.
type Storage_Element is mod 2 ** Storage_Unit;
for Storage_Element'Size use Storage_Unit;
+ -- The type *Storage_Element* represents a byte
pragma Universal_Aliasing (Storage_Element);
-- This type is used by the expander to implement aggregate copy
type Storage_Array is
array (Storage_Offset range <>) of aliased Storage_Element;
for Storage_Array'Component_Size use Storage_Unit;
+ -- The type *Storage_Array* represents a part of the memory
-- Address arithmetic
function "+" (Left : Address; Right : Storage_Offset) return Address;
function "+" (Left : Storage_Offset; Right : Address) return Address;
pragma Import (Intrinsic, "+");
+ -- Returns the sum of ``Left`` and ``Right``
function "-" (Left : Address; Right : Storage_Offset) return Address;
function "-" (Left, Right : Address) return Storage_Offset;
pragma Import (Intrinsic, "-");
+ -- Returns the difference between ``Left`` and ``Right``
function "mod"
(Left : Address;
Right : Storage_Offset) return Storage_Offset;
pragma Import (Intrinsic, "mod");
+ -- Returns the modulus between ``Left`` and ``Right``
-- Conversion to/from integers
type Integer_Address is mod Memory_Size;
+ -- Finally, *Integer_Address* is a non-private modular
+ -- type that represents an address.
function To_Address (Value : Integer_Address) return Address;
pragma Import (Intrinsic, To_Address);
+ -- Converts the *Integer_Address* ``Value`` to an *Address*
function To_Integer (Value : Address) return Integer_Address;
pragma Import (Intrinsic, To_Integer);
+ -- Converts the *Address* ``Value`` to an *Integer_Address*
end System.Storage_Elements;
function PC_For (TB_Entry : Traceback_Entry) return System.Address;
pragma Inline (PC_For);
- -- Returns the address of the call instruction associated with the
- -- provided entry.
+ -- Returns the address of the call instruction associated with
+ -- the provided entry.
function TB_Entry_For (PC : System.Address) return Traceback_Entry;
pragma Inline (TB_Entry_For);
type Long_Unsigned is mod 2 ** Long_Integer'Size;
type Long_Long_Unsigned is mod 2 ** Long_Long_Integer'Size;
type Long_Long_Long_Unsigned is mod Max_Binary_Modulus;
+ -- These are modular types that correspon in size to the standard signed
+ -- types declared in Standard.
type Packed_Byte is mod 2 ** 8;
for Packed_Byte'Size use 8;
-- scalar storage order. But the Scalar_Storage_Order attribute cannot be
-- set directly here, see Exp_Pakd for more details.
+ -- Various aligned arrays of bytes. Those types may be unused on limited
+ -- run-times, but are still present for compatibility between run-times.
+
type Bits_1 is mod 2**1;
type Bits_2 is mod 2**2;
type Bits_4 is mod 2**4;
function Rotate_Right
(Value : Long_Long_Long_Unsigned;
Amount : Natural) return Long_Long_Long_Unsigned;
+ -- The shift and rotate primitives for the unsigned types are intrinsic,
+ -- fully implemented by the compiler.
pragma Import (Intrinsic, Shift_Left);
pragma Import (Intrinsic, Shift_Right);
-- --
------------------------------------------------------------------------------
--- This package contains the specification entities using for the formal
--- verification of the routines for scanning signed integer values.
+-- This package is part of a set of Ghost code packages used to proof the
+-- implementations of the Image and Value attributes. It provides the
+-- specification entities using for the formal verification of the routines
+-- for scanning signed integer values.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- --
------------------------------------------------------------------------------
--- This package provides some common specification functions used by the
--- s-valxxx files.
+-- This package is part of a set of Ghost code packages used to proof the
+-- implementations of the Image and Value attributes. It provides some common
+-- specification functions used by the s-valxxx files.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- --
------------------------------------------------------------------------------
--- This package contains the specification entities using for the formal
--- verification of the routines for scanning modular Unsigned values.
+-- This package is part of a set of Ghost code packages used to proof the
+-- implementations of the Image and Value attributes. It provides the
+-- specification entities using for the formal verification of the routines
+-- for scanning modular unsigned integer values.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
and then (for all J in 1 .. Vector_Boolean_Size =>
Model ("not"'Result) (J) = not Model (Item) (J));
- -- The three boolean operations "nand", "nor" and "nxor" are needed
- -- for cases where the compiler moves boolean array operations into
- -- the body of the loop that iterates over the array elements.
-
- -- Note the following equivalences:
- -- (not X) or (not Y) = not (X and Y) = Nand (X, Y)
- -- (not X) and (not Y) = not (X or Y) = Nor (X, Y)
- -- (not X) xor (not Y) = X xor Y
- -- X xor (not Y) = not (X xor Y) = Nxor (X, Y)
-
function Nand (Left, Right : Boolean) return Boolean
with
Post => Nand'Result = not (Left and Right);
and then (for all J in 1 .. Vector_Boolean_Size =>
Model (Nxor'Result) (J) =
Nxor (Model (Left) (J), Model (Right) (J)));
+ -- The three boolean operations "nand", "nor" and "nxor" are needed
+ -- for cases where the compiler moves boolean array operations into
+ -- the body of the loop that iterates over the array elements.
+ --
+ -- Note the following equivalences:
+ -- (not X) or (not Y) = not (X and Y) = Nand (X, Y)
+ -- (not X) and (not Y) = not (X or Y) = Nor (X, Y)
+ -- (not X) xor (not Y) = X xor Y
+ -- X xor (not Y) = not (X xor Y) = Nxor (X, Y)
pragma Inline_Always ("not");
pragma Inline_Always (Nand);
------------------------------------------------------------------------------
-- This package defines a datatype which is most efficient for performing
--- logical operations on large arrays. See System.Generic_Vector_Operations.
+-- logical operations on large arrays. See
+-- :ref:`System.Generic_Vector_Operations`.
-- In the future this package may also define operations such as element-wise
-- addition, subtraction, multiplication, minimum and maximum of vector-sized
for Vector'Alignment use Integer'Min
(Standard'Maximum_Alignment, System.Word_Size / System.Storage_Unit);
for Vector'Size use System.Word_Size;
+ -- The *Vector* type uses an alignment that allows translating it into
+ -- words.
end System.Vectors;
------------------------------------------------------------------------------
-- This package contains specification functions for scanning signed Integer
--- values for use in Text_IO.Integer_IO, and the Value attribute.
+-- values for use in ``Text_IO.Integer_IO``, and the Value attribute.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
------------------------------------------------------------------------------
-- This package contains specification functions for scanning
--- Long_Long_Integer values for use in Text_IO.Integer_IO, and the Value
+-- Long_Long_Integer values for use in ``Text_IO.Integer_IO``, and the Value
-- attribute.
-- Preconditions in this unit are meant for analysis only, not for run-time
------------------------------------------------------------------------------
-- This package contains specification functions for scanning
--- Long_Long_Unsigned values for use in Text_IO.Modular_IO, and the Value
+-- Long_Long_Unsigned values for use in ``Text_IO.Modular_IO``, and the Value
-- attribute.
-- Preconditions in this unit are meant for analysis only, not for run-time
------------------------------------------------------------------------------
-- This package contains specification functions for scanning modular Unsigned
--- values for use in Text_IO.Modular_IO, and the Value attribute.
+-- values for use in ``Text_IO.Modular_IO``, and the Value attribute.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
------------------------------------------------------------------------------
-- This package contains specification functions for scanning
--- Long_Long_Long_Integer values for use in Text_IO.Integer_IO, and the Value
--- attribute.
+-- ``Long_Long_Long_Integer`` values for use in ``Text_IO.Integer_IO``, and
+-- the Value attribute.
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- --
------------------------------------------------------------------------------
+-- This package is provided for compatibility with Ada 83. It renames
+-- :ref:`Ada.Text_IO` and provides the same functionality.
+
pragma Ada_2012;
-- Explicit setting of Ada 2012 mode is required here, since we want to with a
-- child unit (not possible in Ada 83 mode), and Text_IO is not considered to
-- --
------------------------------------------------------------------------------
+-- Renaming of :ref:`Ada.Unchecked_Conversion`
+
generic
type Source (<>) is limited private;
type Target (<>) is limited private;
function Unchecked_Conversion (S : Source) return Target;
pragma Import (Intrinsic, Unchecked_Conversion);
pragma Pure (Unchecked_Conversion);
+-- See ``Ada.Unchecked_Conversion``
-- --
------------------------------------------------------------------------------
+-- Renaming of :ref:`Ada.Unchecked_Deallocation`
+
generic
type Object (<>) is limited private;
type Name is access Object;
package System.Pack_@@ is
pragma Preelaborate;
+ -- @-bit element type definition
+
Bits : constant := @;
type Bits_@@ is mod 2 ** Bits;
projects / thirdparty / gcc.git / commitdiff
