2009-11-30 Thomas Quinot <quinot@adacore.com>

	* g-sechas.adb: Minor reformatting

2009-11-30  Matthew Heaney  <heaney@adacore.com>

	* a-crbtgo.adb (Delete_Fixup): Add comments explaining why predicates
	were removed.
	* a-cdlili.adb (Vet): Remove always-true predicates.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@154823 138bc75d-0d04-0410-961f-82ee72b054a4

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 4c3e007..3a3bad1 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,15 @@
 2009-11-30  Thomas Quinot  <quinot@adacore.com>
 
+       * g-sechas.adb: Minor reformatting
+
+2009-11-30  Matthew Heaney  <heaney@adacore.com>
+
+       * a-crbtgo.adb (Delete_Fixup): Add comments explaining why predicates
+       were removed.
+       * a-cdlili.adb (Vet): Remove always-true predicates.
+
+2009-11-30  Thomas Quinot  <quinot@adacore.com>
+
        * s-sechas.adb, s-sechas.ads, s-shshco.adb, s-shshco.ads, s-shsh64.adb,
        s-shsh64.ads, s-sehamd.adb, s-sehamd.ads, s-shsh32.adb, s-shsh32.ads,
        s-sehash.adb, s-sehash.ads, g-sechas.adb, g-sechas.ads, g-shshco.adb,

diff --git a/gcc/ada/a-cdlili.adb b/gcc/ada/a-cdlili.adb
index f9d7db8..c2e0d9d 100644 (file)
--- a/gcc/ada/a-cdlili.adb
+++ b/gcc/ada/a-cdlili.adb
@@ -1711,12 +1711,18 @@ package body Ada.Containers.Doubly_Linked_Lists is
             return False;
          end if;
 
+         --  If we get here, we know that this disjunction is true:
+         --  Position.Node.Prev /= null or else Position.Node = L.First
+
          if Position.Node.Next = null
            and then Position.Node /= L.Last
          then
             return False;
          end if;
 
+         --  If we get here, we know that this disjunction is true:
+         --  Position.Node.Next /= null or else Position.Node = L.Last
+
          if L.Length = 1 then
             return L.First = L.Last;
          end if;
@@ -1761,21 +1767,21 @@ package body Ada.Containers.Doubly_Linked_Lists is
             return False;
          end if;
 
-         if Position.Node = L.First then
+         if Position.Node = L.First then  -- eliminates ealier disjunct
             return True;
          end if;
 
-         if Position.Node = L.Last then
-            return True;
-         end if;
+         --  If we get here, we know, per disjunctive syllogism (modus
+         --  tollendo ponens), that this predicate is true:
+         --  Position.Node.Prev /= null
 
-         if Position.Node.Next = null then
-            return False;
+         if Position.Node = L.Last then  -- eliminates earlier disjunct
+            return True;
          end if;
 
-         if Position.Node.Prev = null then
-            return False;
-         end if;
+         --  If we get here, we know, per disjunctive syllogism (modus
+         --  tollendo ponens), that this predicate is true:
+         --  Position.Node.Next /= null
 
          if Position.Node.Next.Prev /= Position.Node then
             return False;

diff --git a/gcc/ada/a-crbtgo.adb b/gcc/ada/a-crbtgo.adb
index cd14b90..c8ddcff 100644 (file)
--- a/gcc/ada/a-crbtgo.adb
+++ b/gcc/ada/a-crbtgo.adb
@@ -49,6 +49,8 @@ package body Ada.Containers.Red_Black_Trees.Generic_Operations is
    procedure Left_Rotate  (Tree : in out Tree_Type; X : Node_Access);
    procedure Right_Rotate (Tree : in out Tree_Type; Y : Node_Access);
 
+--  Why is all the following code commented out ???
+
 --     ---------------------
 --     -- Check_Invariant --
 --     ---------------------
@@ -171,8 +173,15 @@ package body Ada.Containers.Red_Black_Trees.Generic_Operations is
                if Right (W) = null
                  or else Color (Right (W)) = Black
                then
+                  --  As a condition for setting the color of the left child to
+                  --  black, the left child access value must be non-null. A
+                  --  truth table analysis shows that if we arrive here, that
+                  --  condition holds, so there's no need for an explicit test.
+                  --  The assertion is here to document what we know is true.
+
                   pragma Assert (Left (W) /= null);
                   Set_Color (Left (W), Black);
+
                   Set_Color (W, Red);
                   Right_Rotate (Tree, W);
                   W := Right (Parent (X));
@@ -206,8 +215,16 @@ package body Ada.Containers.Red_Black_Trees.Generic_Operations is
 
             else
                if Left (W) = null or else Color (Left (W)) = Black then
+
+                  --  As a condition for setting the color of the right child
+                  --  to black, the right child access value must be non-null.
+                  --  A truth table analysis shows that if we arrive here, that
+                  --  condition holds, so there's no need for an explicit test.
+                  --  The assertion is here to document what we know is true.
+
                   pragma Assert (Right (W) /= null);
                   Set_Color (Right (W), Black);
+
                   Set_Color (W, Red);
                   Left_Rotate (Tree, W);
                   W := Left (Parent (X));
@@ -246,6 +263,8 @@ package body Ada.Containers.Red_Black_Trees.Generic_Operations is
            "attempt to tamper with cursors (container is busy)";
       end if;
 
+      --  Why are these all commented out ???
+
 --    pragma Assert (Tree.Length > 0);
 --    pragma Assert (Tree.Root /= null);
 --    pragma Assert (Tree.First /= null);

diff --git a/gcc/ada/g-sechas.adb b/gcc/ada/g-sechas.adb
index 1c57548..78eddc3 100644 (file)
--- a/gcc/ada/g-sechas.adb
+++ b/gcc/ada/g-sechas.adb
@@ -37,8 +37,7 @@ package body GNAT.Secure_Hashes is
    use Ada.Streams;
 
    Hex_Digit : constant array (Stream_Element range 0 .. 15) of Character :=
-                 ('0', '1', '2', '3', '4', '5', '6', '7',
-                  '8', '9', 'a', 'b', 'c', 'd', 'e', 'f');
+                 "0123456789abcdef";
 
    type Fill_Buffer_Access is
      access procedure