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

[hw762]

I get a similar problem:

$ alr gnatprove
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...

gnatcoll-os-temp.adb:33:09: error: "Generator" is not allowed in SPARK (due to entity declared with SPARK_Mode Off)
   33 |   type Generator_Access is access Ada_Rand.Generator;
      |        ^~~~~~~~~~~~~~~~

It makes my project completely unable to use Spark.

[kanigsson]

Can you try --no-subprojects for gnatprove invocation? In theory it should skip analysing this GNATCOLL file.

[hw762]

No, it gives this:

fatal error: file project_config.ali is incorrectly formatted
make sure you are using consistent versions of gcc/gnatbind

I can't find this file anywhere.

[kanigsson]

We will look into this when we have the time.

[kanigsson]

The original issue seems to be limited to SPARK FSF 14.x, it doesn't appear anymore with SPARK FSF 15.x. I was able to circumvent the newer issue by adding --no-subprojects to the gnatprove commandline. I couldn't reproduce the issue with "file project_config.ali is incorrectly formatted". I would suggest trying to find the file with find -L . -name "project_config.ali, or cleaning temp files with alr gnatprove --clean.