* [Ada] Fix a bug in the contract of formal ordered sets
@ 2022-09-06 7:15 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2022-09-06 7:15 UTC (permalink / raw)
To: gcc-patches; +Cc: Julien Bortolussi
[-- Attachment #1: Type: text/plain, Size: 561 bytes --]
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.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-cforse.ads (Replace): Fix the postcondition.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1012 bytes --]
diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads
--- 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,
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-09-06 7:15 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-09-06 7:15 [Ada] Fix a bug in the contract of formal ordered sets Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).