mirror of https://github.com/Componolit/jwx
110 lines
3.6 KiB
Plaintext
110 lines
3.6 KiB
Plaintext
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;
|