From: Johannes Kliemann Date: Thu, 30 Sep 2021 11:41:13 +0000 (+0200) Subject: [Ada] Add ghost code version of Ada.Numerics.Big_Numbers.Big_Integers X-Git-Tag: basepoints/gcc-13~3769 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=0f074aa4aa248e9602765155acff57604c1d9778;p=thirdparty%2Fgcc.git [Ada] Add ghost code version of Ada.Numerics.Big_Numbers.Big_Integers gcc/ada/ * libgnat/a-nbnbin__ghost.ads: Add ghost package. --- diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.ads b/gcc/ada/libgnat/a-nbnbin__ghost.ads new file mode 100644 index 000000000000..bf79d0576c7e --- /dev/null +++ b/gcc/ada/libgnat/a-nbnbin__ghost.ads @@ -0,0 +1,206 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT RUN-TIME COMPONENTS -- +-- -- +-- ADA.NUMERICS.BIG_NUMBERS.BIG_INTEGERS -- +-- -- +-- 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. -- +-- -- +------------------------------------------------------------------------------ + +package Ada.Numerics.Big_Numbers.Big_Integers with + SPARK_Mode, + Ghost, + Preelaborate +is + type Big_Integer is private + with Integer_Literal => From_Universal_Image; + + function Is_Valid (Arg : Big_Integer) return Boolean + with + Import, + Global => null; + + subtype Valid_Big_Integer is Big_Integer + with Dynamic_Predicate => Is_Valid (Valid_Big_Integer), + Predicate_Failure => raise Program_Error; + + 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; + + 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); + + 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); + + function In_Range + (Arg : Valid_Big_Integer; Low, High : Big_Integer) return Boolean + is (Low <= Arg and Arg <= High) + with + Import, + Global => null; + + 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; + + generic + type Int is range <>; + package Signed_Conversions is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer + with + Import, + Global => null; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int + with + Import, + Pre => In_Range (Arg, + Low => To_Big_Integer (Int'First), + High => To_Big_Integer (Int'Last)) + or else (raise Constraint_Error), + Global => null; + end Signed_Conversions; + + generic + type Int is mod <>; + package Unsigned_Conversions is + + function To_Big_Integer (Arg : Int) return Valid_Big_Integer + with + Import, + Global => null; + + function From_Big_Integer (Arg : Valid_Big_Integer) return Int + with + Import, + Pre => In_Range (Arg, + Low => To_Big_Integer (Int'First), + High => To_Big_Integer (Int'Last)) + or else (raise Constraint_Error), + Global => null; + + end Unsigned_Conversions; + + function From_String (Arg : String) return Valid_Big_Integer + with + Import, + Global => null; + + function From_Universal_Image (Arg : String) return Valid_Big_Integer + renames From_String; + + 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; + +private + pragma SPARK_Mode (Off); + + type Big_Integer is null record; + +end Ada.Numerics.Big_Numbers.Big_Integers;