gnatprove.gpr

with "gnatcoll_core";
with "gpr2";

project GNATprove is

   for Object_Dir use "obj";
   for Exec_Dir use "install/bin";

   for Languages use ("Ada", "C");

   type Build_Type is ("Debug", "Production", "Coverage");

   Build : Build_Type := External ("Build", "Debug");

   Tool := External ("GPR_TOOL", "");

   Target := project'Target;
   Sources := (".", "src/gnatprove", "src/common");

   case Tool is
      when "gnatsas" =>
         Sources := Sources & ("src/common/" & Tool);
      when others =>
         Sources := Sources & ("src/common/" & Target);
   end case;

   for Source_Dirs use Sources;

   for Main use ("gnatprove.adb",
                 "spark_report.adb",
                 "spark_memcached_wrapper.adb",
                 "spark_semaphore_wrapper.adb");

   Common_Switches := ("-gnatyg", "-g", "-gnat2022", "-gnatX");

   package Builder is
      for Executable ("gnatprove.adb") use "gnatprove";
      for Executable ("spark_report.adb") use "spark_report";
      for Executable ("spark_memcached_wrapper.adb") use "spark_memcached_wrapper";
      for Executable ("spark_semaphore_wrapper.adb") use "spark_semaphore_wrapper";

      case Build is
         when "Debug" =>
            for Global_Configuration_Pragmas use "gnatprove.adc";
         when "Production" =>
            null;
         when "Coverage" =>
            --  We don't do coverage of gnatprove yet, only gnat2why
            null;
      end case;

      case Tool is
         when "gnatsas" =>
            --  Use -gnateb to ensure that pragma configuration files checksums are
            --  correctly computed when running incremental analysis in CIs.
            for Global_Compilation_Switches ("Ada") use ("-gnateb");
         when Others =>
            null;
      end case;

   end Builder;

   package Compiler is
      case Build is
         when "Debug" =>
            for Default_Switches ("Ada") use
               Common_Switches & ("-O0", "-gnata", "-gnatwae", "-gnatVa");
         when "Production" =>
            for Default_Switches ("Ada") use
               Common_Switches & ("-O2", "-gnatn");
         when "Coverage" =>
            --  We don't do coverage of gnatprove yet, only gnat2why
            null;
      end case;
   end Compiler;

   package Linker is
      case Target is
         when "x86-linux" | "x86_64-linux" =>
            for Default_Switches ("Ada") use ("-pthread");
         when others =>
            null;
      end case;
   end Linker;

   package Analyzer is

      for Review_File use "analyzer/gnatprove.sar";

      --  Relocate outputs outside of object directory because that one is
      --  cached in CIs and we do not want to store baselines in the cache.
      for Output_Dir use "analyzer";

      --  Exclude source files leading to false positives
      for Excluded_Source_Files use
        ("assumptions.ads",
         "assumptions.adb",
         "print_table.adb",
         "configuration.adb",
         "report_database.ads"); --  spurious GNAT SAS violation U804-011

      for Switches ("analyze") use ("-j0", "--incrementality-method=minimal",
       "--no-gnatcheck");
      for Switches ("infer") use ("--disable-issue-type", "MEMORY_LEAK_ADA");
      for Switches ("inspector") use ("--legacy-level", "1", "-gnatws");

      for Switches ("report code-climate") use ("--long-desc");

   end Analyzer;

end GNATprove;