+2011-08-30 Robert Dewar <dewar@adacore.com>
+
+ * opt.ads, s-soflin.adb, exp_ch9.adb, sem_res.adb: Update comment.
+ Minor code reorg/reformatting.
+
2011-08-30 Yannick Moy <moy@adacore.com>
* opt.adb, opt.ads (Full_Expander_Active): New function defines a
begin
if Full_Expander_Active then
+
-- If we have no handled statement sequence, we may need to build
-- a dummy sequence consisting of a null statement. This can be
-- skipped if the trivial accept optimization is permitted.
return;
elsif Full_Expander_Active then
+
-- Associate discriminals with the first subprogram or entry body to
-- be expanded.
-- behavior can be disabled using switch -gnatd.t which will set this flag
-- to False and revert to the previous dynamic behavior.
- function Full_Expander_Active return Boolean;
- -- 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.
-
-----------------------
-- Tree I/O Routines --
-----------------------
-- Used to store the ASIS version number read from a tree file to check if
-- it is the same as stored in the ASIS version number in Tree_IO.
- ----------------------------------
- -- Mode for Formal Verification --
- ----------------------------------
-
- -- This mode is currently defined through a debug flag
+ -----------------------------------
+ -- Modes for Formal Verification --
+ -----------------------------------
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.
+ 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.
+
private
-- The following type is used to save and restore settings of switches in