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;