Platinum_Reusable_Stack/stack_dev.gpr

project Stack_Dev is

   for Languages use ("Ada");
   for Exec_Dir use ".";

   package Compiler is
      for Default_Switches ("ada") use
        ("-gnatwa",    -- enable additional warnings
         "-g",         -- enable debugging info, in case
         "-gnato11",   -- enable overflow checks everywhere, which is also the default
         "-gnata");    -- enable assertions
   end Compiler;

   package Builder is
      for Switches ("ada") use ("-g");
   end Builder;

   type Adoption_Levels is ("Ada", "Stone", "Bronze", "Silver", "Gold", "Platinum");

   Adoption_Level : Adoption_Levels := external ("Adoption_Level", "Platinum");

   for Object_Dir use "objs/" & Adoption_Level;

   --  set main program
   case Adoption_Level is
      when "Ada" | "Stone" | "Bronze" | "Silver" =>
         for Main use ("demo_aorte.adb");

      when "Gold" | "Platinum" =>
         for Main use ("demo_gold.adb");
   end case;

   --  set source dirs
   case Adoption_Level is
      when "Ada" =>
         for Source_Dirs use ("source/mains", "source/Ada");
      when "Stone" =>
         for Source_Dirs use ("source/mains", "source/Stone");
      when "Bronze" =>
         for Source_Dirs use ("source/mains", "source/Bronze");
      when "Silver" =>
         for Source_Dirs use ("source/mains", "source/Silver");
      when "Gold" =>
         for Source_Dirs use ("source/mains", "source/Gold");
      when "Platinum" =>
         for Source_Dirs use ("source/mains", "source/Platinum");
   end case;

   --  set GNATprove mode switch
   Mode_Switch := "";
   case Adoption_Level is
      when "Ada" =>
         Mode_Switch := "--mode=check";

      when "Stone" =>
         Mode_Switch := "--mode=check_all";

      when "Bronze" =>
         Mode_Switch := "--mode=bronze";

      when "Silver" | "Gold" | "Platinum" =>
         Mode_Switch := "--mode=all";
   end case;

   --  set prover switches
   package Prove is
      for Proof_Switches ("Ada") use
        ("--level=4") & Mode_Switch;
   end Prove;

end Stack_Dev;