JWX.gpr

with "obj/lsc/libsparkcrypto";

project JWX is

   type Callgraph_Type is ("none", "su", "su_da");
   Callgraph : Callgraph_Type := external ("callgraph", "none");

   Callgraph_Switches := ();
   case Callgraph is
      when "none" =>
         Callgraph_Switches := ();

      when "su" =>
         Callgraph_Switches := ("-fcallgraph-info=su");

      when "su_da" =>
         Callgraph_Switches := ("-fcallgraph-info=su,da");
   end case;

   Ada_Switches :=
   (
      "-gnatA"	 -- Avoid processing gnat.adc, if present file will be ignored
     ,"-gnata"  -- Enable pragma Assert/Debug

     ,"-gnatA"  -- Aliasing checks on subprogram parameters
     ,"-gnatef" -- Full source path in brief error messages
     ,"-gnateV" -- Validity checks on subprogram parameters
     ,"-gnatf"  -- Full errors. Verbose details, all undefined references
     ,"-gnatU"  -- Enable unique tag for error messages

     -- Validity checks
     ,"-gnatVa" -- turn on all validity checking options

     -- Warnings
     ,"-gnatwa" -- turn on all info/warnings marked with + in gnatmake help
     ,"-gnatwe" -- treat all warnings (but not info) as errors
     ,"-gnatwd" -- turn on warnings for implicit dereference
     ,"-gnatwh" -- turn on warnings for hiding declarations
     ,"-gnatwk" -- turn on warnings for standard redefinition
     ,"-gnatwt" -- turn on warnings for tracking deleted code
     ,"-gnatwu" -- turn on warnings for unordered enumeration

     -- Style checks
     ,"-gnaty3"    -- Check indentation (3 spaces)
     ,"-gnatya"    -- check attribute casing
     ,"-gnatyA"    -- check array attribute indexes
     ,"-gnatyb"    -- check no blanks at end of lines
     ,"-gnatyc"    -- check comment format (two spaces)
     ,"-gnatyd"    -- check no DOS line terminators
     ,"-gnatye"    -- check end/exit labels present
     ,"-gnatyf"    -- check no form feeds/vertical tabs in source
     ,"-gnatyh"    -- check no horizontal tabs in source
     ,"-gnatyi"    -- check if-then layout
     ,"-gnatyI"    -- check mode in
     ,"-gnatyk"    -- check casing rules for keywords
     ,"-gnatyl"    -- check reference manual layout
     ,"-gnatyL8"   -- check max nest level < nn
     ,"-gnatyM120" -- check line length <= nn characters
     ,"-gnatyn"    -- check casing of package Standard identifiers
     ,"-gnatyO"    -- check overriding indicators
     ,"-gnatyp"    -- check pragma casing
     ,"-gnatyr"    -- check casing for identifier references
     ,"-gnatys"    -- check separate subprogram specs present
     ,"-gnatyS"    -- check separate lines after THEN or ELSE
     ,"-gnatyt"    -- check token separation rules
     ,"-gnatyu"    -- check no unnecessary blank lines
     ,"-gnatyx"    -- check extra parentheses around conditionals

     ,"-fstack-check"          -- dynamic stack checking
   );

   for Source_Dirs use ("src");
   for Object_Dir use "obj";

   package Gnattest
   is
      for Tests_Dir use "../tests";
   end Gnattest;

   package Documentation is
      for Documentation_Dir use "doc/api";
   end Documentation;

   package Builder is
      for Global_Configuration_Pragmas use "spark.adc";
   end Builder;

   package Compiler is
      for Default_Switches ("Ada") use Ada_Switches & Callgraph_Switches;
   end Compiler;

   package Stack is
      for Switches use ("-Wa", "-a", "-p");
   end Stack;

   package Prove is
      for Proof_Switches ("Ada") use
      (
         "-j0",
         "--prover=z3,cvc4,altergo",
         "--steps=1000",
         "--timeout=60",
         "--memlimit=1000",
         "--checks-as-errors",
         "--warnings=error"
      );
   end Prove;

end JWX;