defaults.gpr

abstract project Defaults is

   type Build_Mode is ("strict", "asserts_enabled", "optimized");
   Mode : Build_Mode := external ("mode", "asserts_enabled");
   Cache := external ("GNATPROVE_CACHE", "");
   Procs := external ("GNATPROVE_PROCS", "");

   Compiler_Variant := external ("gnat", "");

   GNATVI := "-gnatVi";
   GNATVO := "-gnatVo";
   GNATEV := "-gnateV";
   GNATA  := "-gnata";

   case Compiler_Variant is
      when "community2020" =>
         GNATVI := "";  -- Eng/RecordFlux/Workarounds#43
         GNATA  := "";  -- Eng/RecordFlux/Workarounds#49
      when "community2021" =>
         GNATA  := "";  -- Eng/RecordFlux/Workarounds#49
      when "pro20.2" =>
         GNATVI := "";  -- Eng/RecordFlux/Workarounds#43
         GNATVO := "";  -- Eng/RecordFlux/Workarounds#23
         GNATEV := "";  -- Eng/RecordFlux/Workarounds#22
         GNATA  := "";  -- Eng/RecordFlux/Workarounds#49
      when "pro21.2" | "pro22.2" =>
         GNATA  := "";  -- Eng/RecordFlux/Workarounds#49
      when "fsf11.2.4" | "fsf12.2.1" =>
         GNATA  := "";  -- Eng/RecordFlux/Workarounds#49
      when "fsf13.2.1" =>
         GNATVO := "";  -- Eng/RecordFlux/Workarounds#51
         GNATA  := "";  -- Eng/RecordFlux/Workarounds#52
      when "fsf14.1.3" =>
         GNATVO := "";  -- Eng/RecordFlux/Workarounds#53
      when others =>
   end case;

   case Mode is
      when "strict" | "optimized" =>
         GNATA  := "";
      when "asserts_enabled" =>
   end case;

   Global_Configuration_Pragmas := "defaults_backward_compatible.adc";

   case Compiler_Variant is
      when "pro23.0w-20220508" | "pro23.0" | "pro23.1" | "pro23.2" =>
         Global_Configuration_Pragmas := "defaults.adc";
      when others =>
   end case;

   Cache_Switch := "";
   case Cache is
      when "" =>
         null;
      when others =>
         Cache_Switch := "--memcached-server=" & Cache;
   end case;

   Procs_Switch := "";
   case Procs is
      when "" =>
         Procs_Switch := "-j 0";
      when others =>
         Procs_Switch := "-j " & Procs;
   end case;

   Proof_Switches :=
   (
      "--prover=z3,cvc5,altergo",
      "--steps=0",
      "--timeout=60",
      "--memlimit=1500",
      "--checks-as-errors=on",
      "--warnings=error",
      -- Eng/RecordFlux/RecordFlux#670
      -- "--proof-warnings",
      "--function-sandboxing=off",
      "--counterexamples=off",
      Procs_Switch,
      Cache_Switch
   );

   Builder_Switches :=
   (
      "-j0"
   );

   Compiler_Switches :=
   (
      "-gnatA",    -- Avoid processing gnat.adc. If a gnat.adc file is present, it will be ignored.
      "-gnatf",    -- Full errors. Multiple errors per line, all undefined references, do not attempt to suppress cascaded errors.
      "-gnatU",    -- Tag all error messages with the unique string ‘error:’.

      -- Validity Checks
      "-gnatVc",  -- Validity checks for copies.
      "-gnatVd",  -- Default (RM) validity checks.
      "-gnatVe",  -- Validity checks for elementary components.
      "-gnatVf",  -- Validity checks for floating-point values.
      GNATVI,     -- Validity checks for ``in`` mode parameters.
      "-gnatVm",  -- Validity checks for ``in out`` mode parameters.
      GNATVO,     -- Validity checks for operator and attribute operands.
      "-gnatVp",  -- Validity checks for parameters.
      "-gnatVr",  -- Validity checks for function returns.
      "-gnatVs",  -- Validity checks for subscripts.
      "-gnatVt",  -- Validity checks for tests.
      GNATEV,     -- Check that all actual parameters of a subprogram call are valid according to the rules of validity checking (Validity Checking).

      -- Debugging
      "-fstack-check",  -- Activate stack checking.
      "-g",             -- Enable generation of debugging information.
      GNATA,            -- Enable assertions.

      -- Warnings
      "-gnatwa",   -- Activate most optional warnings.
      "-gnatw.d",  -- Activate tagging of warning and info messages.
      "-gnatwe",   -- Treat all run-time exception warnings as errors.
      "-gnatwd",   -- Activate warnings on implicit dereferencing.
      -- Eng/RecordFlux/Workarounds#27
      -- "-gnatwh",   -- Activate warnings on hiding.
      "-gnatwt",   -- Activate warnings for tracking of deleted conditional code.
      "-gnatwQ",   -- Suppress warnings on questionable missing parentheses.

      -- Style Checks
      "-gnaty3",    -- Specify indentation level.
      "-gnatya",    -- Check attribute casing.
      "-gnatyA",    -- Use of array index numbers in array attributes.
      "-gnatyb",    -- Blanks not allowed at statement end.
      "-gnatyC",    -- Check comments, single space.
      "-gnatyd",    -- Check no DOS line terminators present.
      "-gnatye",    -- Check end/exit labels.
      "-gnatyf",    -- No form feeds or vertical tabs.
      "-gnatyh",    -- No horizontal tabs.
      "-gnatyi",    -- Check if-then layout.
      "-gnatyI",    -- Check mode IN keywords.
      "-gnatyk",    -- Check keyword casing.
      "-gnatyl",    -- Check layout.
      "-gnatyL9",   -- Set maximum nesting level.
      "-gnatyM120", -- Set maximum line length.
      "-gnatyn",    -- Check casing of entities in Standard.
      "-gnatyO",    -- Check that overriding subprograms are explicitly marked as such.
      "-gnatyp",    -- Check pragma casing.
      "-gnatyr",    -- Check references.
      "-gnatyS",    -- Check no statements after then/else.
      "-gnatyt",    -- Check token spacing.
      "-gnatyu",    -- Check unnecessary blank lines.
      "-gnatyx",    -- Check extra parentheses.

      ""
   );

   Binder_Switches :=
   (
      "-Es"
   );

end Defaults;