diff options
Diffstat (limited to 'gcc/ada/libgnat/a-nbnbig.ads')
| -rw-r--r-- | gcc/ada/libgnat/a-nbnbig.ads | 241 |
1 files changed, 0 insertions, 241 deletions
diff --git a/gcc/ada/libgnat/a-nbnbig.ads b/gcc/ada/libgnat/a-nbnbig.ads deleted file mode 100644 index 04aa62a..0000000 --- a/gcc/ada/libgnat/a-nbnbig.ads +++ /dev/null @@ -1,241 +0,0 @@ ------------------------------------------------------------------------------- --- -- --- GNAT RUN-TIME COMPONENTS -- --- -- --- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS_GHOST -- --- -- --- S p e c -- --- -- --- This specification is derived from the Ada Reference Manual for use with -- --- GNAT. In accordance with the copyright of that document, you can freely -- --- copy and modify this specification, provided that if you redistribute a -- --- modified version, any changes that you have made are clearly indicated. -- --- -- ------------------------------------------------------------------------------- - --- 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. 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. - -pragma Assertion_Policy (Ghost => Ignore); - -package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with - SPARK_Mode, - Ghost, - Pure, - Always_Terminates -is - - 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; - - function "<" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function "<=" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function ">" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function ">=" (L, R : Valid_Big_Integer) return Boolean with - Import, - Global => null; - - function To_Big_Integer (Arg : Integer) return Valid_Big_Integer - 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 - is (Low <= Arg and Arg <= High) - with - Import, - Global => null; - -- Check whether Arg is in the range Low .. High - - function To_Integer (Arg : Valid_Big_Integer) return Integer - with - Import, - Pre => In_Range (Arg, - Low => To_Big_Integer (Integer'First), - 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 - Pre => In_Range (Arg, - Low => To_Big_Integer (Int'First), - 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 - Pre => In_Range (Arg, - Low => To_Big_Integer (Int'First), - 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; - - function From_String (Arg : String) return Valid_Big_Integer - 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, - Global => null; - - function "-" (L : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "abs" (L : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "+" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "-" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "*" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "/" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "mod" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "rem" (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function "**" (L : Valid_Big_Integer; R : Natural) return Valid_Big_Integer - with - Import, - Global => null; - - function Min (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function Max (L, R : Valid_Big_Integer) return Valid_Big_Integer - with - Import, - Global => null; - - function Greatest_Common_Divisor - (L, R : Valid_Big_Integer) return Big_Positive - 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; |