[Ada] Add ghost code version of Ada.Numerics.Big_Numbers.Big_Integers
authorJohannes Kliemann <kliemann@adacore.com>
Thu, 30 Sep 2021 11:41:13 +0000 (13:41 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 20 Oct 2021 10:17:04 +0000 (10:17 +0000)
gcc/ada/

* libgnat/a-nbnbin__ghost.ads: Add ghost package.

gcc/ada/libgnat/a-nbnbin__ghost.ads [new file with mode: 0644]

diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.ads b/gcc/ada/libgnat/a-nbnbin__ghost.ads
new file mode 100644 (file)
index 0000000..bf79d05
--- /dev/null
@@ -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;