AdaCore / AdaCore/gnatcoll-core
Unable to run gnatprove on projects importing GNATCOLL
Open
@Nikokrock is already working on this.
Since Jan 9, 2025.
- Dominant language
- Ada
- Stars
- 55
- Forks
- 36
- PR merge metrics
- No merged PRs in 30d
Description
I'm using Alire to import the GNATCOLL database libraries, which depend on GNATCOLL Core. However, the GNATCOLL crate has a dependency on libgpr which appears to prevent gnatprove from working.
This can be reproduced with:
alr init --bin testcase
alr with gnatcoll
alr with gnatprove
# edit main subprogram to add "with SPARK_Mode"
alr build
alr gnatprove
Phase 1 of 3: generation of data representation information ...
generation of data representation information failed
continuing analysis with partial data representation
for details, see log file gnatprove/data_representation_generation.log
Phase 2 of 3: generation of Global contracts ...
gpr-err-scanner.adb:2421:15: error: choice given in case statement is not static
2421 | when Name_Abort =>
| ^~~~~~~~~~
gpr-err-scanner.adb:2421:15: error: "Name_Abort" is not a static constant (RM 4.9(5))
2421 | when Name_Abort =>
| ^~~~~~~~~~
gpr-err-scanner.adb:2423:15: error: choice given in case statement is not static
2423 | when Name_Abs =>
| ^~~~~~~~
...
<many more lines>
One solution may be to disable SPARK_Mode on libgpr, alternatively a solution to either skip imported project or exclude specific project files when calling gnatprove might be useful.
Relevant forum threads:
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.