public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-4544] [Ada] Add ghost code version of Ada.Numerics.Big_Numbers.Big_Integers
@ 2021-10-20 10:18 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-10-20 10:18 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:0f074aa4aa248e9602765155acff57604c1d9778
commit r12-4544-g0f074aa4aa248e9602765155acff57604c1d9778
Author: Johannes Kliemann <kliemann@adacore.com>
Date: Thu Sep 30 13:41:13 2021 +0200
[Ada] Add ghost code version of Ada.Numerics.Big_Numbers.Big_Integers
gcc/ada/
* libgnat/a-nbnbin__ghost.ads: Add ghost package.
Diff:
---
gcc/ada/libgnat/a-nbnbin__ghost.ads | 206 ++++++++++++++++++++++++++++++++++++
1 file changed, 206 insertions(+)
diff --git a/gcc/ada/libgnat/a-nbnbin__ghost.ads b/gcc/ada/libgnat/a-nbnbin__ghost.ads
new file mode 100644
index 00000000000..bf79d0576c7
--- /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;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2021-10-20 10:18 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-10-20 10:18 [gcc r12-4544] [Ada] Add ghost code version of Ada.Numerics.Big_Numbers.Big_Integers Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).