spark_rfsb509exp.gpr

with "config/spark_rfsb509exp_config.gpr";
project Spark_Rfsb509Exp is

   for Library_Name use "SPARK_RFSB509Exp";
   for Library_Version use
     Project'Library_Name &
     ".so." &
     Spark_Rfsb509Exp_Config.Crate_Version;

   for Source_Dirs use ("src/", "config/");
   for Object_Dir use "obj/" & Spark_Rfsb509Exp_Config.Build_Profile;
   for Create_Missing_Dirs use "True";
   for Library_Dir use "lib";

   type Library_Type_Type is ("relocatable", "static", "static-pic");
   Library_Type : Library_Type_Type :=
     external ("SPARK_RFSB509Exp_LIBRARY_TYPE",
       external ("LIBRARY_TYPE", "static"));
   for Library_Kind use Library_Type;

   type Enabled_Kind is ("enabled", "disabled");
   Compile_Checks   : Enabled_Kind :=
     External ("SPARKExp_COMPILE_CHECKS", "enabled");
   Runtime_Checks   : Enabled_Kind :=
     External ("SPARKExp_RUNTIME_CHECKS", "disabled");
   Style_Checks     : Enabled_Kind :=
     External ("SPARKExp_STYLE_CHECKS", "enabled");
   Contracts_Checks : Enabled_Kind :=
     External ("SPARK_RFSB509Exp_CONTRACTS", "disabled");

   type Build_Kind is ("debug", "O1", "O2", "O3", "Os", "Og");
   Build_Mode : Build_Kind := External ("SPARKNACL_BUILD_MODE", "O2");

   Compile_Checks_Switches := ();
   case Compile_Checks is
      when "enabled" =>
         Compile_Checks_Switches :=
           ("-gnatwaC",  -- All warnings except redundant checks
            "-gnatwe"); -- Warnings as errors
      when others => null;
   end case;

   Runtime_Checks_Switches := ();
   case Runtime_Checks is
      when "enabled" => null;
      when others =>
         Runtime_Checks_Switches :=
           ("-gnatp"); -- Supress checks
   end case;

   Style_Checks_Switches := ();
   case Style_Checks is
      when "enabled" => null;
         Style_Checks_Switches :=
           ("-gnaty");    -- style checks on
      when others => null;
   end case;

   Contracts_Switches := ();
   case Contracts_Checks is
      when "enabled" =>
         Contracts_Switches :=
           ("-gnata"); --  Enable assertions and contracts
      when "disabled" =>
         null;
   end case;

   Build_Switches := ();
   case Build_Mode is
      when "debug" =>
         Build_Switches := ("-g",   -- Debug info
                            "-O0"); -- No optimization
      when "O1" =>
         Build_Switches := ("-O1",     -- Optimization
                            "-gnatn"); -- Enable inlining
      when "O2" =>
         Build_Switches := ("-O2",     -- Optimization
                            "-gnatn"); -- Enable inlining
      when "O3" =>
         Build_Switches := ("-O3",     -- Optimization
                            "-gnatn"); -- Enable inlining
      when "Os" =>
         Build_Switches := ("-Os");     -- Optimize for small code size, no inlining
      when "Og" =>
         Build_Switches := ("-g",
                            "-Og");
   end case;

   package Compiler is
      for Default_Switches ("Ada") use
        Compile_Checks_Switches &
        Build_Switches &
        Runtime_Checks_Switches &
        Style_Checks_Switches &
        Contracts_Switches &
        ("-ffunction-sections") & -- Create a linker section for each function
        ("-fdata-sections") &    -- Create a linker section for each data area
        ("-gnatw.X") & -- Disable warnings for No_Exception_Propagation
        ("-gnatQ");    -- Don't quit. Generate ALI and tree files even if illegalities
   end Compiler;

   package Binder is
      for Switches ("Ada") use ("-Es"); --  Symbolic traceback
   end Binder;

   package Prove is
      for Proof_Switches ("Ada") use ("--proof=per_path",
                                      "-j4",
                                      "--no-global-generation",
                                      "--no-inlining",
                                      "--no-loop-unrolling",
                                      "--level=1",
                                      "--counterexamples=on",
                                      "--prover=z3,cvc4,altergo",
                                      "--timeout=60",
                                      "--memlimit=0",
                                      "--steps=200000",
                                      "--report=statistics");
   end Prove;

   package Install is
      for Artifacts (".") use ("share");
   end Install;

end Spark_Rfsb509Exp;