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,
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;
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;
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 --
-- ---------------------
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));
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));
"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);
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