Post-conditions in GPIO are wrong

[lambourg]

There's at least one post condition in the GPIO that is invalid:
overriding
procedure Set (This : in out GPIO_Point) with
Inline,
Post => Set (This);

Sometimes, setting a pin to a particular value will have no effect if the output is Open Drain, but is not erroneous either.

[pat-rogers]

OK, I can believe that. Any others?
The only ones that are significant are those for whether a pin configuration is locked, as there is no other check and so only via debug will a user know that an attempt to configure a pin(s) will have no effect.