From ad9d60128432221e9e1c14b3365ea1ac61e303f6 Mon Sep 17 00:00:00 2001
From: Johannes Kliemann <kliemann@componolit.com>
Date: Thu, 18 Jul 2019 14:51:00 +0200
Subject: [PATCH] prove subtract with overflow check ref #47

---
 src/minimal/s-arit64.adb | 18 +++++++++++++++---
 src/minimal/s-arit64.ads |  6 +++++-
 2 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/src/minimal/s-arit64.adb b/src/minimal/s-arit64.adb
index 4e88c83..e5e5530 100644
--- a/src/minimal/s-arit64.adb
+++ b/src/minimal/s-arit64.adb
@@ -66,7 +66,7 @@ is
               and U = To_Uns (To_Int (U));
    pragma Warnings (On, "procedure ""Lemma_Identity"" is not referenced");
 
-   procedure Lemma_Uns_Associativity (X, Y : Int64) with
+   procedure Lemma_Uns_Associativity_Add (X, Y : Int64) with
       Ghost,
       Pre      => (if X < 0 and Y <= 0 then Int64'First - X < Y)
                   and (if X >= 0 and Y >= 0 then Int64'Last - X >= Y),
@@ -74,6 +74,15 @@ is
       Annotate => (GNATprove, False_Positive, "postcondition",
                    "addition in 2 complement is associative");
 
+   procedure Lemma_Uns_Associativity_Sub (X, Y : Int64) with
+      Ghost,
+      Pre      => (if X >= 0 and Y <= 0 then Y > Int64'First
+                      and then Int64'Last - X >= abs (Y))
+                   and (if X < 0 and Y > 0 then Y < Int64'First - X),
+      Post     => X - Y = To_Int (To_Uns (X) - To_Uns (Y)),
+      Annotate => (GNATprove, False_Positive, "postcondition",
+                   "subtraction in 2 complement is associative");
+
    subtype Uns32 is Unsigned_32;
 
    -----------------------
@@ -155,7 +164,9 @@ is
 
    procedure Lemma_Identity (I : Int64; U : Uns64) is null;
 
-   procedure Lemma_Uns_Associativity (X, Y : Int64) is null;
+   procedure Lemma_Uns_Associativity_Add (X, Y : Int64) is null;
+
+   procedure Lemma_Uns_Associativity_Sub (X, Y : Int64) is null;
 
    --------------------------
    -- Add_With_Ovflo_Check --
@@ -165,7 +176,7 @@ is
       R : constant Int64 := To_Int (To_Uns (X) + To_Uns (Y));
 
    begin
-      Lemma_Uns_Associativity (X, Y);
+      Lemma_Uns_Associativity_Add (X, Y);
       if X >= 0 then
          if Y < 0 or else R >= 0 then
             return R;
@@ -620,6 +631,7 @@ is
       R : constant Int64 := To_Int (To_Uns (X) - To_Uns (Y));
 
    begin
+      Lemma_Uns_Associativity_Sub (X, Y);
       if X >= 0 then
          if Y > 0 or else R >= 0 then
             return R;
diff --git a/src/minimal/s-arit64.ads b/src/minimal/s-arit64.ads
index 226351a..387e584 100644
--- a/src/minimal/s-arit64.ads
+++ b/src/minimal/s-arit64.ads
@@ -54,7 +54,11 @@ is
    --  Raises Constraint_Error if sum of operands overflows 64 bits,
    --  otherwise returns the 64-bit signed integer sum.
 
-   function Subtract_With_Ovflo_Check (X, Y : Int64) return Int64;
+   function Subtract_With_Ovflo_Check (X, Y : Int64) return Int64 with
+      Pre  => (if X >= 0 and Y <= 0 then Y > Int64'First
+                  and then Int64'Last - X >= abs (Y))
+              and (if X < 0 and Y > 0 then Y < Int64'First - X),
+      Post => Subtract_With_Ovflo_Check'Result = X - Y;
    --  Raises Constraint_Error if difference of operands overflows 64
    --  bits, otherwise returns the 64-bit signed integer difference.