[Ada] Fix a bug in the contract of formal ordered sets

There are 2 main issues in the postcondition of the function Replace
of the formal ordered sets, in the sub package Generic_Keys. One is
related to the fact that when the element is changed, the key is
also changed. The second one is due to the fact that the arrival of
the new element might modify the ordering of the set and thus
the Positions might be modified.
As a consequence, the postcondition might be false and thus fail
at runtime.

gcc/ada/

	* libgnat/a-cforse.ads (Replace): Fix the postcondition.

diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads
index ff96d8e7547b84b0dbdef1f71a110b49ed7afba0..f6cca0fe05282e3fc73dc31e314af173911fe16e 100644 (file)
--- a/gcc/ada/libgnat/a-cforse.ads
+++ b/gcc/ada/libgnat/a-cforse.ads
@@ -1598,7 +1598,7 @@ is
 
              --  Key now maps to New_Item
 
-             and Element (Container, Key) = New_Item
+             and Element (Container, Find (Container, Key)'Old) = New_Item
 
              --  New_Item is contained in Container
 
@@ -1622,8 +1622,9 @@ is
                     E_Right  => Elements (Container),
                     P_Left   => Positions (Container)'Old,
                     P_Right  => Positions (Container),
-                    Position => Find (Container, Key))
-             and Positions (Container) = Positions (Container)'Old;
+                    Position => Find (Container, Key)'Old)
+             and P.Keys_Included (Positions (Container),
+                                  Positions (Container)'Old);
 
       procedure Exclude (Container : in out Set; Key : Key_Type) with
         Global         => null,