Fix resource leak detection - #29
Merged
Merged
Conversation
It turns out that transaction handle resource leaks were not being detected
by GNATprove due to the use of general access types ("access all" type)
internally to point to transaction data objects. Only pool-specific access
types have resource leak detection in SPARK.
GNATprove was warning about possible resource leaks at the point where the
pool-specific access was converted to a general access, but this was incorrectly
believed to be safe, so the warning was suppressed. It turns out this was not
safe and broke leak detection, so the use of general access types has now
been removed in favour of pool-specific access types only to ensure resource
leak detection works correctly on all handle types again.
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.
It turns out that transaction handle resource leaks were not being detected by GNATprove due to the use of general access types ("access all" type) internally to point to transaction data objects. Only pool-specific access types have resource leak detection in SPARK.
GNATprove was warning about possible resource leaks at the point where the pool-specific access was converted to a general access, but this was incorrectly believed to be safe, so the warning was suppressed. It turns out this was not safe and broke leak detection, so the use of general access types has now been removed in favour of pool-specific access types only to ensure resource leak detection works correctly on all handle types again.