Support proving a frame condition when moving ownership of handles - #25
Merged
Conversation
The location of these annotations has changed for more recent versions of GNATprove. We keep the annotations in both locations to support a wider range of tool versions.
The Move procedure does not modify the stored primitive objects, and the postcondition of Move attempts to express this. However, since Request_Type and Confirm_Type are limited types, we cannot simply express that Request = Request'Old. Instead, we express that _properties_ on those primitives are preserved. This change adds some missing properties to the postcondition. This also required adding a Requires_Cleanup function for Service_Handles.
Moving ownership of a handle using `Move` does not modify the primitive, but this cannot be fully expressed in the postcondition of `Move` because the primitive types are limited types, so it is not possible to refer to the `'Old` value of the primitive in the postcondition. Instead, the postcondition of `Move` proves that certain properties are preserved during the move, such as Valid_Request. In some cases, however, it is useful to prove that the arbitrary properties on the primitives are also preserved during the move. For example, proving that the value of a primitive has not changed. This change adds new, generic variants of Move that can be instantiated with arbitrary, user-defined properties which are proven to be preserved during the move in the postcondition.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Moving ownership of a handle using
Movedoes not modify the primitive, but this cannot be fully expressed in the postcondition ofMovebecause the primitive types are limited types, so it is not possible to refer to the'Oldvalue of the primitive in the postcondition. Instead, the postcondition ofMoveproves that certain properties are preserved during the move, such as Valid_Request.In some cases, however, it is useful to prove that the arbitrary properties on the primitives are also preserved during the move. For example, proving that the value of a primitive has not changed.
This change adds new, generic variants of Move that can be instantiated with arbitrary, user-defined properties which are proven to be preserved during the move in the postcondition.
The postcondition of the exiting
Moveprocedures is also strengthened.