Gnatprove: ignore dependencies

General
1

When doing alr gnatprove in a project that contains GNATColl dependency, I get the following error (many actually and similar):

gpr-err-scanner.adb:2569:15: error: "Name_Synchronized" is not a static constant (RM 4.9(5))
 2569 |         when Name_Synchronized =>

Is there any way to constrain gnatprove to only check the current project and ignore dependencies? Or is this error unrelated?

1 Like
2

Wondering about this myself. I tried this in the main project file:

   package Prove is
      for Excluded_Units use (
         "GNATCOLL",
         "GNATCOLL.SQL",
         "GNATCOLL.SQL.POSTGRESQL",
         "GPR"
      );
   end Prove;

But no dice. Did you ever figure this out?

3

You could annotate the source code to skip the proof… See Implementation Defined Annotations — SPARK User's Guide 26.0w

procedure P
  with Annotate => (GNATprove, Skip_Proof);

procedure P
  with Annotate => (GNATprove, Skip_Flow_And_Proof);

package Prove only supports Proof_Switches and Proof_Dir as per Project Attributes — SPARK User's Guide 26.0w

HOWEVER, using the documentation in the first link provided in this answer, we can use --mode=check-all for a specific set of files in the package Prove using Proof_Switches as that is documented to be equivalent to Skip_Flow_And_Proof.

I hope this help. Best,
Fer

2 Likes
4

I tried this:

   package Prove is
      for Proof_Switches ("gpr-err-scanner.adb") use ("--mode=check-all");
   end Prove;

But unfortunately gnatprove errors with unrecognized option '--mode=check-all'. I tried creating a separate project file without the imports to get gnatprove to run, but it can’t get far without the imports.

5

What version of GNATProve are you using? The documentation is about the latest available version, so an older version may not have this feature. I generally recommend people to always use the latest version of GNATProve as it comes with several enhancements.

Otherwise, you can always use with SPARK_Mode => Off wherever you are calling a function that uses that external file.

Best,
Fer

6

I appreciate the help on this - I tried upgrading to the latest available with Alire. Now it’s complaining that the file in question is not part of the project… In this case it’s not even a function I’m calling directly, this is a dependency further upstream so it’s difficult to isolate.

7

Mmmm… I found someone having that exact same issue in Reddit see https://www.reddit.com/r/ada/comments/1b1p9m6/how_to_setup_spark_mode_to_bypass_thirdparty/

So it seems to be an easy to reproduce bug… What version of GNATColl are you using? If it is not the latest, could you try updating it to see if it has been fixed?

Best regards,
Fer

8

Look like the latest release: Release v25.0.0 · AdaCore/gnatcoll-core · GitHub

my alire.toml:

[[depends-on]]
gnatcoll_postgres = "^25.0.0"

[[depends-on]]
gnatcoll = "^25.0.0"
9

Yup… Then I would recommend opening an issue in the GNATColl repo documenting this issue if you do not mind.

Best,
Fer

1 Like
10
1 Like