sparklib_common.gpr

abstract project SPARKlib_common is

   for Source_Files use ();

   --  Environment variable SPARKLIB_INSTALLED controls whether the
   --  project and its sources are being installed as part of SPARK install
   --  (value "True") or whether they are in source repository configuration
   --  (value "False"). Inside SPARK install, this project file is installed
   --  in <install>/lib/gnat and the sources in <install>/include/spark

   type SPARKlib_Installed_T is ("True", "False");
   SPARKlib_Installed : SPARKlib_Installed_T := External("SPARKLIB_INSTALLED", "True");

   --  Environment variable SPARKLIB_BODY_MODE controls whether the
   --  project is with'ed in client projects to use lemmas (value "Off"),
   --  or whether it is being itself formally verified (value "On").
   --  Users should not set the value of this variable to "On".

   type SPARK_Body_Mode_T is ("Off", "On");
   SPARK_Body_Mode : SPARK_Body_Mode_T := External ("SPARKLIB_BODY_MODE", "Off");

   Common_Default_Switches :=
     ("-gnat2022", "-gnatygo-u",
      "-gnatwI",  --  disable warnings about SPARKlib using GNAT internal units
      "-gnateDSPARK_BODY_MODE=" & SPARK_Body_Mode);

   package Compiler is
      --  Enforce GNAT style checks, except for multiple blank lines which does
      --  not work for preprocessed files, and alphabetical ordering of
      --  subprogram bodies (although not applicable to null subprograms).
      for Default_Switches ("Ada") use Common_Default_Switches;
   end Compiler;

   package Prove is
      for Proof_Dir use "proof";
   end Prove;

end SPARKlib_common;