Set Externally_Built to prevent GNATprove from trying to analyse the runtime#26
Merged
Merged
Conversation
…runtime
This uses the GPR_TOOL external variable to detect when GNATprove is
running on the runtime_build.gpr and ravenscar_build.gpr files, in which
case Externally_Built is set to True to prevent GNATprove from analysing
the runtime sources.
This is necessary since some versions of GNATprove have problems processing
certain runtime units. For example, GNAT FSF 15 errors out on a-synbar.adb
due to the use of the 'Count attribute on an entry, which this version of
GNATprove erroneously thinks is not permitted when pure-barriers is in
effect. These problems are avoided by preventing GNATprove from trying to
analyse the runtime as a whole.
The reason why GNATprove tries to process the runtime sources is because
the expected usage of these runtime crates is to "with" runtime_build.gpr
and/or ravenscar_build.gpr in the user's GPR project, so the runtime
project files are automatically included as subprojects in the user's
project. By default, GNATprove tries to prove all subprojects, which would
include the runtime in this case.
Other GNAT runtimes do not have this problem because they are not "with"ed
as a subproject, and are instead selected using the --RTS switch or
`for Runtime ("Ada") use "<path>";`, so GNATprove does not see them as a
subproject. This would not work for community-bb-runtimes crates, however,
because this ensures the runtime is built properly as part of the project
build, and because some attributes of the runtime project files need to be
referenced in the user's project file (such as Target, Runtime, and sometimes
also Linker_Options).
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.
This uses the GPR_TOOL external variable to detect when GNATprove is running on the runtime_build.gpr and ravenscar_build.gpr files, in which case Externally_Built is set to True to prevent GNATprove from analysing the runtime sources.
This is necessary since some versions of GNATprove have problems processing certain runtime units. For example, GNAT FSF 15 errors out on a-synbar.adb due to the use of the 'Count attribute on an entry, which this version of GNATprove erroneously thinks is not permitted when pure-barriers is in effect. These problems are avoided by preventing GNATprove from trying to analyse the runtime as a whole.
The reason why GNATprove tries to process the runtime sources is because the expected usage of these runtime crates is to "with" runtime_build.gpr and/or ravenscar_build.gpr in the user's GPR project, so the runtime project files are automatically included as subprojects in the user's project. By default, GNATprove tries to prove all subprojects, which would include the runtime in this case.
Other GNAT runtimes do not have this problem because they are not "with"ed as a subproject, and are instead selected using the --RTS switch or
for Runtime ("Ada") use "<path>";, so GNATprove does not see them as a subproject. This would not work for community-bb-runtimes crates, however, because this ensures the runtime is built properly as part of the project build, and because some attributes of the runtime project files need to be referenced in the user's project file (such as Target, Runtime, and sometimes also Linker_Options).