Unable to run gnatprove on projects importing GNATCOLL

[docandrew]

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:

• https://forum.ada-lang.io/t/gnatprove-ignore-dependencies/1626
• https://www.reddit.com/r/ada/comments/1b1p9m6/how_to_setup_spark_mode_to_bypass_thirdparty/

[docandrew]

Also worth noting I've been able to reproduce this on both Windows and Linux.

[Nikokrock]

We have started separating gnatcoll-core in several projects, you should depends only on gnatcoll_core.gpr rather than gnatcoll.gpr and this will remove the need for project support and thus libgpr dep