- -- These modes are currently defined through debug flags
-
- Formal_Verification_Mode : Boolean := False;
- -- Set True if ALFA_Mode or SPARK_Mode
-
- ALFA_Mode : Boolean := False;
- -- Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode
-
- ALFA_Through_SPARK_Mode : Boolean := False;
- -- Specific compiling mode targeting formal verification through
- -- the generation of SPARK code for those parts of the input code that
- -- belong to the ALFA subset of Ada. Set by debug flag -gnatd.E.
-
- ALFA_Through_Why_Mode : Boolean := False;
- -- Specific compiling mode targeting formal verification through
- -- the generation of Why code for those parts of the input code that
- -- belong to the ALFA subset of Ada. Set by debuf flag -gnatd.F.
-
- SPARK_Mode : Boolean := False;
- -- Reject constructs not allowed by SPARK. Set by flag -gnatd.D or
- -- by pragma SPARK_95.
+ Alfa_Mode : Boolean := False;
+ -- Specific compiling mode targeting formal verification through the
+ -- generation of Why code for those parts of the input code that belong to
+ -- the Alfa subset of Ada. Set by debug flag -gnatd.F.
+
+ Strict_Alfa_Mode : Boolean := False;
+ -- Interpret compiler permissions as strictly as possible. E.g. base ranges
+ -- for integers are limited to the strict minimum with this option. Set by
+ -- debug flag -gnatd.D.
+
+ function Full_Expander_Active return Boolean;
+ pragma Inline (Full_Expander_Active);
+ -- Returns the value of (Expander_Active and not Alfa_Mode). This "flag"
+ -- indicates that expansion is fully active, that is, not in the reduced
+ -- mode for Alfa (True) or that expansion is either deactivated, or active
+ -- in the reduced mode for Alfa (False). For more information on full
+ -- expansion, see package Expander. For more information on reduced
+ -- Alfa expansion, see package Exp_Alfa.