diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -29,9 +29,24 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  Preconditions, postconditions, ghost code, loop invariants and assertions
+--  in this unit are meant for analysis only, not for run-time checking, as it
+--  would be too costly otherwise. This is enforced by setting the assertion
+--  policy to Ignore.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 with Ada.Unchecked_Conversion;
 
-package body System.Arith_32 is
+package body System.Arith_32
+  with SPARK_Mode
+is
 
    pragma Suppress (Overflow_Check);
    pragma Suppress (Range_Check);
@@ -43,27 +58,65 @@ package body System.Arith_32 is
 
    function To_Int is new Ada.Unchecked_Conversion (Uns32, Int32);
 
+   package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns32);
+
+   function Big (Arg : Uns32) return Big_Integer is
+     (Unsigned_Conversion.To_Big_Integer (Arg))
+   with Ghost;
+
+   package Unsigned_Conversion_64 is new Unsigned_Conversions (Int => Uns64);
+
+   function Big (Arg : Uns64) return Big_Integer is
+     (Unsigned_Conversion_64.To_Big_Integer (Arg))
+   with Ghost;
+
+   pragma Warnings
+     (Off, "non-preelaborable call not allowed in preelaborated unit",
+      Reason => "Ghost code is not compiled");
+   Big_0 : constant Big_Integer :=
+     Big (Uns32'(0))
+   with Ghost;
+   Big_2xx32 : constant Big_Integer :=
+     Big (Uns32'(2 ** 32 - 1)) + 1
+   with Ghost;
+   Big_2xx64 : constant Big_Integer :=
+     Big (Uns64'(2 ** 64 - 1)) + 1
+   with Ghost;
+   pragma Warnings
+     (On, "non-preelaborable call not allowed in preelaborated unit");
+
    -----------------------
    -- Local Subprograms --
    -----------------------
 
    function "abs" (X : Int32) return Uns32 is
      (if X = Int32'First
-      then 2**31
+      then Uns32'(2**31)
       else Uns32 (Int32'(abs X)));
    --  Convert absolute value of X to unsigned. Note that we can't just use
    --  the expression of the Else since it overflows for X = Int32'First.
 
+   function Lo (A : Uns64) return Uns32 is (Uns32 (A and (2 ** 32 - 1)));
+   --  Low order half of 64-bit value
+
    function Hi (A : Uns64) return Uns32 is (Uns32 (Shift_Right (A, 32)));
    --  High order half of 64-bit value
 
-   function To_Neg_Int (A : Uns32) return Int32;
+   function To_Neg_Int (A : Uns32) return Int32
+   with
+     Annotate => (GNATprove, Terminating),
+     Pre      => In_Int32_Range (-Big (A)),
+     Post     => Big (To_Neg_Int'Result) = -Big (A);
    --  Convert to negative integer equivalent. If the input is in the range
    --  0 .. 2**31, then the corresponding nonpositive signed integer (obtained
    --  by negating the given value) is returned, otherwise constraint error is
    --  raised.
 
-   function To_Pos_Int (A : Uns32) return Int32;
+   function To_Pos_Int (A : Uns32) return Int32
+   with
+     Annotate => (GNATprove, Terminating),
+     Pre      => In_Int32_Range (Big (A)),
+     Post     => Big (To_Pos_Int'Result) = Big (A);
    --  Convert to positive integer equivalent. If the input is in the range
    --  0 .. 2**31 - 1, then the corresponding nonnegative signed integer is
    --  returned, otherwise constraint error is raised.
@@ -72,6 +125,168 @@ package body System.Arith_32 is
    pragma No_Return (Raise_Error);
    --  Raise constraint error with appropriate message
 
+   ------------------
+   -- Local Lemmas --
+   ------------------
+
+   procedure Lemma_Abs_Commutation (X : Int32)
+   with
+     Ghost,
+     Post => abs (Big (X)) = Big (Uns32'(abs X));
+
+   procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => abs (X / Y) = abs X / abs Y;
+
+   procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer)
+   with
+     Ghost,
+     Post => abs (X * Y) = abs X * abs Y;
+
+   procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => abs (X rem Y) = (abs X) rem (abs Y);
+
+   procedure Lemma_Div_Commutation (X, Y : Uns64)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => Big (X) / Big (Y) = Big (X / Y);
+
+   procedure Lemma_Div_Ge (X, Y, Z : Big_Integer)
+   with
+     Ghost,
+     Pre  => Z > 0 and then X >= Y * Z,
+     Post => X / Z >= Y;
+
+   procedure Lemma_Ge_Commutation (A, B : Uns32)
+   with
+     Ghost,
+     Pre  => A >= B,
+     Post => Big (A) >= Big (B);
+
+   procedure Lemma_Hi_Lo (Xu : Uns64; Xhi, Xlo : Uns32)
+   with
+     Ghost,
+     Pre  => Xhi = Hi (Xu) and Xlo = Lo (Xu),
+     Post => Big (Xu) = Big_2xx32 * Big (Xhi) + Big (Xlo);
+
+   procedure Lemma_Mult_Commutation (X, Y, Z : Uns64)
+   with
+     Ghost,
+     Pre  => Big (X) * Big (Y) < Big_2xx64 and then Z = X * Y,
+     Post => Big (X) * Big (Y) = Big (Z);
+
+   procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => (X >= Big_0 and then Y >= Big_0)
+       or else (X <= Big_0 and then Y <= Big_0),
+     Post => X * Y >= Big_0;
+
+   procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => (X <= Big_0 and then Y >= Big_0)
+       or else (X >= Big_0 and then Y <= Big_0),
+     Post => X * Y <= Big_0;
+
+   procedure Lemma_Neg_Div (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => X / Y = (-X) / (-Y);
+
+   procedure Lemma_Neg_Rem (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => X rem Y = X rem (-Y);
+
+   procedure Lemma_Not_In_Range_Big2xx32
+   with
+     Post => not In_Int32_Range (Big_2xx32)
+       and then not In_Int32_Range (-Big_2xx32);
+
+   procedure Lemma_Rem_Commutation (X, Y : Uns64)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => Big (X) rem Big (Y) = Big (X rem Y);
+
+   -----------------------------
+   -- Local lemma null bodies --
+   -----------------------------
+
+   procedure Lemma_Abs_Commutation (X : Int32) is null;
+   procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) is null;
+   procedure Lemma_Div_Commutation (X, Y : Uns64) is null;
+   procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null;
+   procedure Lemma_Ge_Commutation (A, B : Uns32) is null;
+   procedure Lemma_Mult_Commutation (X, Y, Z : Uns64) is null;
+   procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) is null;
+   procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) is null;
+   procedure Lemma_Neg_Rem (X, Y : Big_Integer) is null;
+   procedure Lemma_Not_In_Range_Big2xx32 is null;
+   procedure Lemma_Rem_Commutation (X, Y : Uns64) is null;
+
+   -------------------------------
+   -- Lemma_Abs_Div_Commutation --
+   -------------------------------
+
+   procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is
+   begin
+      if Y < 0 then
+         if X < 0 then
+            pragma Assert (abs (X / Y) = abs (X / (-Y)));
+         else
+            Lemma_Neg_Div (X, Y);
+            pragma Assert (abs (X / Y) = abs ((-X) / (-Y)));
+         end if;
+      end if;
+   end Lemma_Abs_Div_Commutation;
+
+   -------------------------------
+   -- Lemma_Abs_Rem_Commutation --
+   -------------------------------
+
+   procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer) is
+   begin
+      if Y < 0 then
+         Lemma_Neg_Rem (X, Y);
+         if X < 0 then
+            pragma Assert (X rem Y = -((-X) rem (-Y)));
+            pragma Assert (abs (X rem Y) = (abs X) rem (abs Y));
+         else
+            pragma Assert (abs (X rem Y) = (abs X) rem (abs Y));
+         end if;
+      end if;
+   end Lemma_Abs_Rem_Commutation;
+
+   -----------------
+   -- Lemma_Hi_Lo --
+   -----------------
+
+   procedure Lemma_Hi_Lo (Xu : Uns64; Xhi, Xlo : Uns32) is
+   begin
+      pragma Assert (Uns64 (Xhi) = Xu / Uns64'(2 ** 32));
+      pragma Assert (Uns64 (Xlo) = Xu mod 2 ** 32);
+   end Lemma_Hi_Lo;
+
+   -------------------
+   -- Lemma_Neg_Div --
+   -------------------
+
+   procedure Lemma_Neg_Div (X, Y : Big_Integer) is
+   begin
+      pragma Assert ((-X) / (-Y) = -(X / (-Y)));
+      pragma Assert (X / (-Y) = -(X / Y));
+   end Lemma_Neg_Div;
+
    -----------------
    -- Raise_Error --
    -----------------
@@ -79,6 +294,9 @@ package body System.Arith_32 is
    procedure Raise_Error is
    begin
       raise Constraint_Error with "32-bit arithmetic overflow";
+      pragma Annotate
+        (GNATprove, Intentional, "exception might be raised",
+         "Procedure Raise_Error is called to signal input errors");
    end Raise_Error;
 
    -------------------
@@ -101,51 +319,252 @@ package body System.Arith_32 is
       Ru : Uns32;
       --  Unsigned quotient and remainder
 
+      --  Local ghost variables
+
+      Mult  : constant Big_Integer := abs (Big (X) * Big (Y)) with Ghost;
+      Quot  : Big_Integer with Ghost;
+      Big_R : Big_Integer with Ghost;
+      Big_Q : Big_Integer with Ghost;
+
+      --  Local lemmas
+
+      procedure Prove_Negative_Dividend
+      with
+        Ghost,
+        Pre  => Z /= 0
+          and then ((X >= 0 and Y < 0) or (X < 0 and Y >= 0))
+          and then Big_Q =
+            (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                           Big (X) * Big (Y) / Big (Z),
+                                           Big (X) * Big (Y) rem Big (Z))
+             else Big (X) * Big (Y) / Big (Z)),
+         Post =>
+           (if Z > 0 then Big_Q <= Big_0 else Big_Q >= Big_0);
+      --  Proves the sign of rounded quotient when dividend is non-positive
+
+      procedure Prove_Overflow
+      with
+        Ghost,
+        Pre  => Z /= 0 and then Mult >= Big_2xx32 * Big (Uns32'(abs Z)),
+        Post => not In_Int32_Range (Big (X) * Big (Y) / Big (Z))
+          and then not In_Int32_Range
+            (Round_Quotient (Big (X) * Big (Y), Big (Z),
+                             Big (X) * Big (Y) / Big (Z),
+                             Big (X) * Big (Y) rem Big (Z)));
+      --  Proves overflow case
+
+      procedure Prove_Positive_Dividend
+      with
+        Ghost,
+        Pre  => Z /= 0
+          and then ((X >= 0 and Y >= 0) or (X < 0 and Y < 0))
+          and then Big_Q =
+            (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                           Big (X) * Big (Y) / Big (Z),
+                                           Big (X) * Big (Y) rem Big (Z))
+             else Big (X) * Big (Y) / Big (Z)),
+         Post =>
+           (if Z > 0 then Big_Q >= Big_0 else Big_Q <= Big_0);
+      --  Proves the sign of rounded quotient when dividend is non-negative
+
+      procedure Prove_Rounding_Case
+      with
+        Ghost,
+        Pre  => Z /= 0
+          and then Quot = Big (X) * Big (Y) / Big (Z)
+          and then Big_R = Big (X) * Big (Y) rem Big (Z)
+          and then Big_Q =
+            Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
+          and then Big (Ru) = abs Big_R
+          and then Big (Zu) = Big (Uns32'(abs Z)),
+        Post => abs Big_Q =
+          (if Ru > (Zu - Uns32'(1)) / Uns32'(2)
+           then abs Quot + 1
+           else abs Quot);
+      --  Proves correctness of the rounding of the unsigned quotient
+
+      procedure Prove_Sign_R
+      with
+        Ghost,
+        Pre  => Z /= 0 and then Big_R = Big (X) * Big (Y) rem Big (Z),
+        Post => In_Int32_Range (Big_R);
+
+      procedure Prove_Signs
+      with
+        Ghost,
+        Pre  => Z /= 0
+          and then Quot = Big (X) * Big (Y) / Big (Z)
+          and then Big_R = Big (X) * Big (Y) rem Big (Z)
+          and then Big_Q =
+            (if Round then
+               Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
+             else Quot)
+          and then Big (Ru) = abs Big_R
+          and then Big (Qu) = abs Big_Q
+          and then In_Int32_Range (Big_Q)
+          and then In_Int32_Range (Big_R)
+          and then R =
+            (if (X >= 0) = (Y >= 0) then To_Pos_Int (Ru) else To_Neg_Int (Ru))
+          and then Q =
+            (if ((X >= 0) = (Y >= 0)) = (Z >= 0) then To_Pos_Int (Qu)
+             else To_Neg_Int (Qu)),  --  need to ensure To_Pos_Int precondition
+        Post => Big (R) = Big_R and then Big (Q) = Big_Q;
+      --  Proves final signs match the intended result after the unsigned
+      --  division is done.
+
+      -----------------------------
+      -- Prove_Negative_Dividend --
+      -----------------------------
+
+      procedure Prove_Negative_Dividend is
+      begin
+         Lemma_Mult_Non_Positive (Big (X), Big (Y));
+      end Prove_Negative_Dividend;
+
+      --------------------
+      -- Prove_Overflow --
+      --------------------
+
+      procedure Prove_Overflow is
+      begin
+         Lemma_Div_Ge (Mult, Big_2xx32, Big (Uns32'(abs Z)));
+         Lemma_Abs_Commutation (Z);
+         Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
+      end Prove_Overflow;
+
+      -----------------------------
+      -- Prove_Positive_Dividend --
+      -----------------------------
+
+      procedure Prove_Positive_Dividend is
+      begin
+         Lemma_Mult_Non_Negative (Big (X), Big (Y));
+      end Prove_Positive_Dividend;
+
+      -------------------------
+      -- Prove_Rounding_Case --
+      -------------------------
+
+      procedure Prove_Rounding_Case is
+      begin
+         if Same_Sign (Big (X) * Big (Y), Big (Z)) then
+            null;
+         end if;
+      end Prove_Rounding_Case;
+
+      ------------------
+      -- Prove_Sign_R --
+      ------------------
+
+      procedure Prove_Sign_R is
+      begin
+         pragma Assert (In_Int32_Range (Big (Z)));
+      end Prove_Sign_R;
+
+      -----------------
+      -- Prove_Signs --
+      -----------------
+
+      procedure Prove_Signs is null;
+
+   --  Start of processing for Scaled_Divide32
+
    begin
       --  First do the 64-bit multiplication
 
       D := Uns64 (Xu) * Uns64 (Yu);
 
+      pragma Assert (Mult = Big (D));
+      Lemma_Hi_Lo (D, Hi (D), Lo (D));
+      pragma Assert (Mult = Big_2xx32 * Big (Hi (D)) + Big (Lo (D)));
+
+      --  If divisor is zero, raise error
+
+      if Z = 0 then
+         Raise_Error;
+      end if;
+
+      Quot := Big (X) * Big (Y) / Big (Z);
+      Big_R := Big (X) * Big (Y) rem Big (Z);
+      if Round then
+         Big_Q := Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R);
+      else
+         Big_Q := Quot;
+      end if;
+
       --  If dividend is too large, raise error
 
       if Hi (D) >= Zu then
+         Lemma_Ge_Commutation (Hi (D), Zu);
+         pragma Assert (Mult >= Big_2xx32 * Big (Zu));
+         Prove_Overflow;
          Raise_Error;
+      end if;
 
       --  Then do the 64-bit division
 
-      else
-         Qu := Uns32 (D / Uns64 (Zu));
-         Ru := Uns32 (D rem Uns64 (Zu));
-      end if;
+      Qu := Uns32 (D / Uns64 (Zu));
+      Ru := Uns32 (D rem Uns64 (Zu));
+
+      Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
+      Lemma_Abs_Rem_Commutation (Big (X) * Big (Y), Big (Z));
+      Lemma_Abs_Mult_Commutation (Big (X), Big (Y));
+      Lemma_Abs_Commutation (X);
+      Lemma_Abs_Commutation (Y);
+      Lemma_Abs_Commutation (Z);
+      Lemma_Mult_Commutation (Uns64 (Xu), Uns64 (Yu), D);
+      Lemma_Div_Commutation (D, Uns64 (Zu));
+      Lemma_Rem_Commutation (D, Uns64 (Zu));
+
+      pragma Assert (Big (Ru) = abs Big_R);
+      pragma Assert (Big (Qu) = abs Quot);
+      pragma Assert (Big (Zu) = Big (Uns32'(abs Z)));
 
       --  Deal with rounding case
 
-      if Round and then Ru > (Zu - Uns32'(1)) / Uns32'(2) then
+      if Round then
+         Prove_Rounding_Case;
 
-         --  Protect against wrapping around when rounding, by signaling
-         --  an overflow when the quotient is too large.
+         if Ru > (Zu - Uns32'(1)) / Uns32'(2) then
+            pragma Assert (abs Big_Q = Big (Qu) + 1);
 
-         if Qu = Uns32'Last then
-            Raise_Error;
-         end if;
+            --  Protect against wrapping around when rounding, by signaling
+            --  an overflow when the quotient is too large.
 
-         Qu := Qu + Uns32'(1);
+            if Qu = Uns32'Last then
+               pragma Assert (abs Big_Q = Big_2xx32);
+               Lemma_Not_In_Range_Big2xx32;
+               Raise_Error;
+            end if;
+
+            Qu := Qu + Uns32'(1);
+         end if;
       end if;
 
+      pragma Assert (Big (Qu) = abs Big_Q);
+      pragma Assert (Big (Ru) = abs Big_R);
+
       --  Set final signs (RM 4.5.5(27-30))
 
       --  Case of dividend (X * Y) sign positive
 
       if (X >= 0 and then Y >= 0) or else (X < 0 and then Y < 0) then
+         Prove_Positive_Dividend;
+
          R := To_Pos_Int (Ru);
          Q := (if Z > 0 then To_Pos_Int (Qu) else To_Neg_Int (Qu));
 
       --  Case of dividend (X * Y) sign negative
 
       else
+         Prove_Negative_Dividend;
+
          R := To_Neg_Int (Ru);
          Q := (if Z > 0 then To_Neg_Int (Qu) else To_Pos_Int (Qu));
       end if;
+
+      Prove_Sign_R;
+      Prove_Signs;
    end Scaled_Divide32;
 
    ----------------


diff --git a/gcc/ada/libgnat/s-arit32.ads b/gcc/ada/libgnat/s-arit32.ads
--- a/gcc/ada/libgnat/s-arit32.ads
+++ b/gcc/ada/libgnat/s-arit32.ads
@@ -33,17 +33,79 @@
 --  signed integer values in cases where either overflow checking is
 --  required, or intermediate results are longer than 32 bits.
 
+--  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.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
 with Interfaces;
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 
-package System.Arith_32 is
-   pragma Pure;
+package System.Arith_32
+  with Pure, SPARK_Mode
+is
+   use type Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer;
+   use type Interfaces.Integer_32;
 
    subtype Int32 is Interfaces.Integer_32;
 
+   subtype Big_Integer is
+     Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer
+   with Ghost;
+
+   package Signed_Conversion is new
+     Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Signed_Conversions
+     (Int => Int32);
+
+   function Big (Arg : Int32) return Big_Integer is
+     (Signed_Conversion.To_Big_Integer (Arg))
+   with Ghost;
+
+   function In_Int32_Range (Arg : Big_Integer) return Boolean is
+     (Ada.Numerics.Big_Numbers.Big_Integers_Ghost.In_Range
+       (Arg, Big (Int32'First), Big (Int32'Last)))
+   with Ghost;
+
+   function Same_Sign (X, Y : Big_Integer) return Boolean is
+     (X = Big (Int32'(0))
+        or else Y = Big (Int32'(0))
+        or else (X < Big (Int32'(0))) = (Y < Big (Int32'(0))))
+   with Ghost;
+
+   function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
+     (if abs R > (abs Y - Big (Int32'(1))) / Big (Int32'(2)) then
+       (if Same_Sign (X, Y) then Q + Big (Int32'(1))
+        else Q - Big (Int32'(1)))
+      else
+        Q)
+   with
+     Ghost,
+     Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
+
    procedure Scaled_Divide32
      (X, Y, Z : Int32;
       Q, R    : out Int32;
-      Round   : Boolean);
+      Round   : Boolean)
+   with
+     Pre  => Z /= 0
+       and then In_Int32_Range
+         (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                        Big (X) * Big (Y) / Big (Z),
+                                        Big (X) * Big (Y) rem Big (Z))
+          else Big (X) * Big (Y) / Big (Z)),
+     Post => Big (R) = Big (X) * Big (Y) rem Big (Z)
+       and then
+         (if Round then
+            Big (Q) = Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                      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


