+2012-12-05 Yannick Moy <moy@adacore.com>
+
+ * gnat1drv.adb (Adjust_Global_Switches): Move setting of flags for
+ Alfa mode before general treatment of flags, so that overflow checks
+ settings are set appropriately in Alfa mode. Also set the mode to
+ STRICT in Alfa mode if not already set by the user.
+
+2012-12-05 Robert Dewar <dewar@adacore.com>
+
+ * sem_ch3.adb: Minor reformatting.
+
+2012-12-05 Steve Baird <baird@adacore.com>
+
+ * sinfo.ads: Improve comments about SCIL-related node kinds and selector
+ functions.
+
+2012-12-05 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch10.adb (Build_Limited_Views): Even though the unit is
+ not analyzed, place its entity on the name in the with clause,
+ so that warnings on unused with-clause are properly supported
+ for limited withs.
+
+2012-12-05 Robert Dewar <dewar@adacore.com>
+
+ * gnat_ugn.texi: Update overflow description. Pragma
+ Overflow_Checks changed to Overflow_Mode.
+
2012-12-05 Ed Schonberg <schonberg@adacore.com>
* sem_ch3.adb (Build_Derived_Private_Type): Handle properly a
Dynamic_Elaboration_Checks := False;
- -- Set STRICT mode for overflow checks if not set explicitly
+ -- Set STRICT mode for overflow checks if not set explicitly. This
+ -- prevents suppressing of overflow checks by default, in code down
+ -- below.
if Suppress_Options.Overflow_Checks_General = Not_Set then
Suppress_Options.Overflow_Checks_General := Strict;
Try_Semantics := True;
end if;
+ -- Set switches for formal verification mode
+
+ if Debug_Flag_Dot_VV then
+ Formal_Extensions := True;
+ end if;
+
+ if Debug_Flag_Dot_FF then
+ Alfa_Mode := True;
+
+ -- Set strict standard interpretation of compiler permissions
+
+ if Debug_Flag_Dot_DD then
+ Strict_Alfa_Mode := True;
+ end if;
+
+ -- Turn off inlining, which would confuse formal verification output
+ -- and gain nothing.
+
+ Front_End_Inlining := False;
+ Inline_Active := False;
+
+ -- Disable front-end optimizations, to keep the tree as close to the
+ -- source code as possible, and also to avoid inconsistencies between
+ -- trees when using different optimization switches.
+
+ Optimization_Level := 0;
+
+ -- Enable some restrictions systematically to simplify the generated
+ -- code (and ease analysis). Note that restriction checks are also
+ -- disabled in Alfa mode, see Restrict.Check_Restriction, and user
+ -- specified Restrictions pragmas are ignored, see
+ -- Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
+
+ Restrict.Restrictions.Set (No_Initialize_Scalars) := True;
+
+ -- Note: at this point we used to suppress various checks, but that
+ -- is not what we want. We need the semantic processing for these
+ -- checks (which will set flags like Do_Overflow_Check, showing the
+ -- points at which potential checks are required semantically). We
+ -- don't want the expansion associated with these checks, but that
+ -- happens anyway because this expansion is simply not done in the
+ -- Alfa version of the expander.
+
+ -- Turn off dynamic elaboration checks: generates inconsistencies in
+ -- trees between specs compiled as part of a main unit or as part of
+ -- a with-clause.
+
+ Dynamic_Elaboration_Checks := False;
+
+ -- Set STRICT mode for overflow checks if not set explicitly. This
+ -- prevents suppressing of overflow checks by default, in code down
+ -- below.
+
+ if Suppress_Options.Overflow_Checks_General = Not_Set then
+ Suppress_Options.Overflow_Checks_General := Strict;
+ Suppress_Options.Overflow_Checks_Assertions := Strict;
+ end if;
+
+ -- Kill debug of generated code, since it messes up sloc values
+
+ Debug_Generated_Code := False;
+
+ -- Turn cross-referencing on in case it was disabled (e.g. by -gnatD)
+ -- as it is needed for computing effects of subprograms in the formal
+ -- verification backend.
+
+ Xref_Active := True;
+
+ -- Polling mode forced off, since it generates confusing junk
+
+ Polling_Required := False;
+
+ -- Set operating mode to Generate_Code, but full front-end expansion
+ -- is not desirable in Alfa mode, so a light expansion is performed
+ -- instead.
+
+ Operating_Mode := Generate_Code;
+
+ -- Skip call to gigi
+
+ Debug_Flag_HH := True;
+
+ -- Disable Expressions_With_Actions nodes
+
+ -- The gnat2why backend does not deal with Expressions_With_Actions
+ -- in all places (in particular assertions). It is difficult to
+ -- determine in the frontend which cases are allowed, so we disable
+ -- Expressions_With_Actions entirely. Even in the cases where
+ -- gnat2why deals with Expressions_With_Actions, it is easier to
+ -- deal with the original constructs (quantified, conditional and
+ -- case expressions) instead of the rewritten ones.
+
+ Use_Expression_With_Actions := False;
+
+ -- Enable assertions and debug pragmas, since they give valuable
+ -- extra information for formal verification.
+
+ Assertions_Enabled := True;
+ Debug_Pragmas_Enabled := True;
+
+ -- Turn off style check options since we are not interested in any
+ -- front-end warnings when we are getting Alfa output.
+
+ Reset_Style_Check_Options;
+
+ -- Suppress compiler warnings, since what we are interested in here
+ -- is what formal verification can find out.
+
+ Warning_Mode := Suppress;
+
+ -- Suppress the generation of name tables for enumerations, which are
+ -- not needed for formal verification, and fall outside the Alfa
+ -- subset (use of pointers).
+
+ Global_Discard_Names := True;
+
+ -- Suppress the expansion of tagged types and dispatching calls,
+ -- which lead to the generation of non-Alfa code (use of pointers),
+ -- which is more complex to formally verify than the original source.
+
+ Tagged_Type_Expansion := False;
+ end if;
+
-- Set Configurable_Run_Time mode if system.ads flag set
if Targparm.Configurable_Run_Time_On_Target or Debug_Flag_YY then
-- Set proper status for overflow check mechanism
- -- If already set (by -gnato or above in CodePeer mode) then we have
- -- nothing to do.
+ -- If already set (by -gnato or above in Alfa or CodePeer mode) then we
+ -- have nothing to do.
if Opt.Suppress_Options.Overflow_Checks_General /= Not_Set then
null;
Back_End_Handles_Limited_Types := False;
end if;
- -- Set switches for formal verification mode
-
- if Debug_Flag_Dot_VV then
- Formal_Extensions := True;
- end if;
-
- if Debug_Flag_Dot_FF then
- Alfa_Mode := True;
-
- -- Set strict standard interpretation of compiler permissions
-
- if Debug_Flag_Dot_DD then
- Strict_Alfa_Mode := True;
- end if;
-
- -- Turn off inlining, which would confuse formal verification output
- -- and gain nothing.
-
- Front_End_Inlining := False;
- Inline_Active := False;
-
- -- Disable front-end optimizations, to keep the tree as close to the
- -- source code as possible, and also to avoid inconsistencies between
- -- trees when using different optimization switches.
-
- Optimization_Level := 0;
-
- -- Enable some restrictions systematically to simplify the generated
- -- code (and ease analysis). Note that restriction checks are also
- -- disabled in Alfa mode, see Restrict.Check_Restriction, and user
- -- specified Restrictions pragmas are ignored, see
- -- Sem_Prag.Process_Restrictions_Or_Restriction_Warnings.
-
- Restrict.Restrictions.Set (No_Initialize_Scalars) := True;
-
- -- Note: at this point we used to suppress various checks, but that
- -- is not what we want. We need the semantic processing for these
- -- checks (which will set flags like Do_Overflow_Check, showing the
- -- points at which potential checks are required semantically). We
- -- don't want the expansion associated with these checks, but that
- -- happens anyway because this expansion is simply not done in the
- -- Alfa version of the expander.
-
- -- Kill debug of generated code, since it messes up sloc values
-
- Debug_Generated_Code := False;
-
- -- Turn cross-referencing on in case it was disabled (e.g. by -gnatD)
- -- as it is needed for computing effects of subprograms in the formal
- -- verification backend.
-
- Xref_Active := True;
-
- -- Polling mode forced off, since it generates confusing junk
-
- Polling_Required := False;
-
- -- Set operating mode to Generate_Code, but full front-end expansion
- -- is not desirable in Alfa mode, so a light expansion is performed
- -- instead.
-
- Operating_Mode := Generate_Code;
-
- -- Skip call to gigi
-
- Debug_Flag_HH := True;
-
- -- Disable Expressions_With_Actions nodes
-
- -- The gnat2why backend does not deal with Expressions_With_Actions
- -- in all places (in particular assertions). It is difficult to
- -- determine in the frontend which cases are allowed, so we disable
- -- Expressions_With_Actions entirely. Even in the cases where
- -- gnat2why deals with Expressions_With_Actions, it is easier to
- -- deal with the original constructs (quantified, conditional and
- -- case expressions) instead of the rewritten ones.
-
- Use_Expression_With_Actions := False;
-
- -- Enable assertions and debug pragmas, since they give valuable
- -- extra information for formal verification.
-
- Assertions_Enabled := True;
- Debug_Pragmas_Enabled := True;
-
- -- Turn off style check options since we are not interested in any
- -- front-end warnings when we are getting Alfa output.
-
- Reset_Style_Check_Options;
-
- -- Suppress compiler warnings, since what we are interested in here
- -- is what formal verification can find out.
-
- Warning_Mode := Suppress;
-
- -- Suppress the generation of name tables for enumerations, which are
- -- not needed for formal verification, and fall outside the Alfa
- -- subset (use of pointers).
-
- Global_Discard_Names := True;
-
- -- Suppress the expansion of tagged types and dispatching calls,
- -- which lead to the generation of non-Alfa code (use of pointers),
- -- which is more complex to formally verify than the original source.
-
- Tagged_Type_Expansion := False;
- end if;
-
-- If the inlining level has not been set by the user, compute it from
-- the optimization level: 1 at -O1/-O2 (and -Os), 2 at -O3 and above.
causing all intermediate overflows to be handled in strict mode.
This switch also causes arithmetic overflow checking to be performed
-(as though pragma @code{Unsuppress (Overflow_Check)} has been specified.
+(as though pragma @code{Unsuppress (Overflow_Mode)} has been specified.
The default if no option @option{-gnato} is given is that overflow handling
is in @code{STRICT} mode (computations done using the base type), and that
-overflow is not enabled.
+overflow checking is suppressed.
Note that division by zero is a separate check that is not
controlled by this switch (division by zero checking is on by default).
@item -gnato??
@cindex @option{-gnato??} (@command{gcc})
@cindex Overflow checks
+@cindex Overflow mode
@cindex Check, overflow
-In @code{CHECKED} and @code{MINIMIZED} modes (@option{-gnato1} and
-@option{-gnato2}), it enables overflow checking for integer operations.
-In @code{ELIMINATED} mode (@option{-gnato3}), it enables arbitrary
-precision arithmetic for integer operations. In all these modes, this
-causes @value{EDITION} to generate slower and larger executable programs
-by adding code to either check for overflow (resulting in raising
-@code{Constraint_Error} as required by standard Ada semantics) or avoid
-overflows. In mode @code{CHECKED}, overflow checks correspond to
-situations in which the true value of the result of an operation may be
-outside the base range of the result type. In mode @code{MINIMIZED},
-overflow checks correspond to situations in which the true value of the
-result of an operation may be outside the largest available machine
-integer type (@code{Long_Long_Integer}). The following example shows the
-distinction:
+This switch controls the mode used for computing intermediate
+arithmetic integer operations, and also enables overflow checking.
+For a full description of overflow mode and checking control, see
+the ``Overflow Check Handling in GNAT'' appendix in this
+User's Guide.
-@smallexample @c ada
-procedure Add_And_Subtract (X : in out Integer; Y, Z : in Integer) is
-begin
- X := X + Y - Z;
-end Add_And_Subtract;
-
-X1 : Integer := Integer'Last;
-X2 : Integer range 1 .. 5 := 5;
-
-Add_And_Subtract (X1, 1, 0); -- first addition and subtraction
-Add_And_Subtract (X1, 1, 1); -- second addition and subtraction
-Add_And_Subtract (X2, 1, 0); -- third addition and subtraction
-Add_And_Subtract (X2, 1, 1); -- fourth addition and subtraction
-@end smallexample
-
-@noindent
-Note that if explicit values are assigned at compile time, the compiler
-may be able to detect overflow at compile time, in which case no actual
-run-time checking code is required, and @code{Constraint_Error} will be
-raised unconditionally, with or without @option{-gnato}.
-
-The first addition results in a value that is outside the base range of
-@code{Integer}. In mode @code{CHECKED}, this raises
-@code{Constraint_Error} at run time. In mode @code{MINIMIZED}, the
-addition and subtraction are performed in type @code{Long_Long_Integer},
-which is 64 bits for most machines. The compiler detects that no
-overflow check is needed on these operations. The program still raises
-@code{Constraint_Error} at run time because the resulting value is too
-large to be assigned to @code{X}. The assignment results in a violation
-of the explicit range constraint; such range checks are performed by
-default, and are unaffected by @option{-gnato??}. In mode
-@code{ELIMINATED}, the compiler uses type @code{Long_Long_Integer} for
-intermediate computations, as this type is sufficient here to avoid all
-overflows. When it is not sufficient, the compiler uses instead a
-library for multiple-precision arithmetic, which may cause a significant
-run-time overhead. The program still raises @code{Constraint_Error} at
-run time when assigning to @code{X}.
-
-The second addition results in a value that is outside the base range of
-@code{Integer}. In mode @code{CHECKED}, this raises
-@code{Constraint_Error} at run time, like in the previous case. In mode
-@code{MINIMIZED}, the addition and subtraction are performed in type
-@code{Long_Long_Integer}, resulting in a final value that fits in an
-@code{Integer}. Thus, no @code{Constraint_Error} is raised. In mode
-@code{ELIMINATED}, the compiler generates the same code as in mode
-@code{MINIMIZED}, which avoids all overflows.
-
-The third addition and subtraction result in an intermediate value and a
-result well in the base range of @code{Integer}, so no
-@code{Constraint_Error} exception is raised at run time in any
-mode. However, the copy to @code{X2} when returning from the call to
-@code{Add_And_Subtract} fails the range check for the type of
-@code{X2}. Hence, a @code{Constraint_Error} exception is raised at run
-time in all modes.
-
-The fourth addition and subtraction result in an intermediate value and
-a result well in the base range of @code{Integer}, and in a final value
-that fits in the type of @code{X2}. Hence, no exception is raised at run
-time in any mode.
-
-Basically the rule is that in the default mode (@option{-gnato??} not
-used), the generated code assures that all integer variables stay within
-their declared ranges, or within the base range if there is no declared
-range. This prevents any serious problems like indexes out of range for
-array operations.
-
-What is not checked in default mode is an overflow that results in an
-in-range, but incorrect value. In the above example, the first
-assignment to @code{X1} gives a result that is within the range of the
-target variable, but the result is wrong in the sense that it is too
-large to be represented correctly. Typically the assignment to @code{X1}
-will result in wrap around to the largest negative number.
+Overflow checks are always enabled by this switch. The argument
+controls the mode, using the codes
+
+@itemize
+@item 1 = STRICT
+In STRICT mode, intermediate operations are always done using the
+base type, and overflow checking ensures that the result is within
+the base type range.
+
+@item 2 = MINIMIZED
+In MINIMIZED mode, overflows in intermediate operations are avoided
+where possible by using a larger integer type for the computation
+(typically @code{Long_Long_Integer). Overflow checking ensures that
+the result fits in this larger integer type.
+
+@item 3 = ELIMINATED
+In ELIMINATED mode, overflows in intermediate operations are avoided
+by using multi-precision arithmetic. In this case, overflow checking
+has no effect on intermediate operations (since overflow is impossible).
+@end itemize
+
+If two digits are present after @option{-gnato} then the first digit
+sets the mode for expressions outside assertions, and the second digit
+sets the mode for expressions within assertions. Here assertions is used
+in the technical sense (which includes for example precondition and
+postcondition expressions).
+
+If one digit is present, the corresponding mode is applicable to both
+expressions within and outside assertion expressions.
+
+If no digits are present, the default is to enable overflow checks
+and set STRICT mode for both kinds of expressions. This is compatible
+with the use of @option{-gnato} in previous versions of GNAT.
@findex Machine_Overflows
Note that the @option{-gnato??} switch does not affect the code generated
The three modes are:
@itemize @bullet
-@item @i{All intermediate overflows checked} (@code{STRICT})
+@item @i{Use base type for intermediate operations} (@code{STRICT})
In this mode, all intermediate results for predefined arithmetic
- operators must be in range of the base type. If this is not the
+ operators are computed using the base type, and the result must
+ be in range of the base type. If this is not the
case then either an exception is raised (if overflow checks are
enabled) or the execution is erroneous (if overflow checks are suppressed).
This is the normal default mode.
@item @i{Most intermediate overflows avoided} (@code{MINIMIZED})
In this mode, the compiler attempts to avoid intermediate overflows by
- using @code{Long_Long_Integer} as the type in which arithmetic is
- performed for predefined arithmetic operators. This is slightly more
+ using a larger integer type, typically @code{Long_Long_Integer},
+ as the type in which arithmetic is
+ performed for predefined arithmetic operators. This may be slightly more
expensive at
run time (compared to suppressing intermediate overflow checks), though
the cost is negligible on modern 64-bit machines. For the examples given
earlier, no intermediate overflows would have resulted in exceptions,
since the intermediate results are all in the range of
@code{Long_Long_Integer} (typically 64-bits on nearly all implementations
- of GNAT).
+ of GNAT). In addition, if checks are enabled, this reduces the number of
+ checks that must be made, so this choice may actually result in an
+ improvement in space and time behavior.
However, there are cases where @code{Long_Long_Integer} is not large
enough, consider the following example:
@noindent
The desired mode of for handling intermediate overflow can be specified using
-either the @code{Overflow_Checks} pragma or an equivalent compiler switch.
+either the @code{Overflow_Mode} pragma or an equivalent compiler switch.
The pragma has the form
-@cindex pragma @code{Overflow_Checks}
+@cindex pragma @code{Overflow_Mode}
@smallexample @c ada
- pragma Overflow_Checks ([General =>] MODE [, [Assertions =>] MODE]);
+ pragma Overflow_Mode ([General =>] MODE [, [Assertions =>] MODE]);
@end smallexample
@noindent
and @code{Assertions} applies to expressions within assertions. For example:
@smallexample @c ada
- pragma Overflow_Checks
+ pragma Overflow_Mode
(General => Minimized, Assertions => Eliminated);
@end smallexample
the behavior at run time matches the expected mathematical
behavior.
-The @code{Overflow_Checks} pragma has the same scoping and placement
+The @code{Overflow_Mode} pragma has the same scoping and placement
rules as pragma @code{Suppress}, so it can occur either as a
configuration pragma, specifying a default for the whole
program, or in a declarative scope, where it applies to the
remaining declarations and statements in that scope.
-Note that pragma @code{Overflow_Checks} does not affect whether
+Note that pragma @code{Overflow_Mode} does not affect whether
overflow checks are enabled or suppressed. It only controls the
method used to compute intermediate values. To control whether
overflow checking is enabled or suppressed, use pragma @code{Suppress}
@itemize @bullet
@item @code{1}:
-all intermediate overflows checked (@code{CHECKED})
+use base type for intermediate operations (@code{STRICT})
@item @code{2}:
minimize intermediate overflows (@code{MINIMIZED})
@item @code{3}:
If no digits follow the @option{-gnato}, then it is equivalent to
@option{-gnato11},
-causing all intermediate overflows to be checked.
+causing all intermediate operations to be computed using the base
+type (@code{STRICT} mode).
In addition to setting the mode used for computation of intermediate
results, the @code{-gnato} switch also enables overflow checking (which
is suppressed by default). It thus combines the effect of using
-a pragma @code{Overflow_Checks} and pragma @code{Unsuppress}.
+a pragma @code{Overflow_Mode} and pragma @code{Unsuppress}.
@c -------------------------
raise Program_Error;
end case;
+ -- The limited unit is not analyzed but the with clause must be
+ -- minimally decorated so that checks on unused with clause also work
+ -- with limited with clauses.
+
+ if Is_Entity_Name (Name (N)) then
+ Set_Entity (Name (N), P);
+
+ elsif Nkind (Name (N)) = N_Selected_Component then
+ Set_Entity (Selector_Name (Name (N)), P);
+ end if;
+
-- Check if the chain is already built
Spec := Specification (Unit (Library_Unit (N)));
then
Append_Elmt (Derived_Type, Private_Dependents (Parent_Type));
+ -- Check for unusual case where a type completed by a private
+ -- derivation occurs within a package nested in a child unit, and
+ -- the parent is declared in an ancestor.
+
if Is_Child_Unit (Scope (Current_Scope))
and then Is_Completion
and then In_Private_Part (Current_Scope)
and then Scope (Parent_Type) /= Current_Scope
+
+ -- Note that if the parent has a completion in the private part,
+ -- (which is itself a derivation from some other private type)
+ -- it is that completion that is visible, there is no full view
+ -- available, and no special processing is needed.
+
and then Present (Full_View (Parent_Type))
then
- -- This is the unusual case where a type completed by a private
- -- derivation occurs within a package nested in a child unit, and
- -- the parent is declared in an ancestor. In this case, the full
- -- view of the parent type will become visible in the body of
- -- the enclosing child, and only then will the current type be
- -- possibly non-private. We build a underlying full view that
- -- will be installed when the enclosing child body is compiled.
- -- Note that if the parent has a completion in the private part,
- -- (which is itself a derivation from some other private type)
- -- it is that completion that is visible, there is no full view
- -- view available, and no special processing is needed.
+ -- In this case, the full view of the parent type will become
+ -- visible in the body of the enclosing child, and only then will
+ -- the current type be possibly non-private. We build an
+ -- underlying full view that will be installed when the enclosing
+ -- child body is compiled.
Full_Der :=
Make_Defining_Identifier
-- SCIL nodes are special nodes added to the tree when the CodePeer
-- mode is active. They help the CodePeer backend to locate nodes that
- -- require special processing.
-
- -- Major documentation on the general design of the SCIL interface, and
- -- in particular detailed description of these nodes is missing and is
- -- to be supplied in the future, when the design has finalized ???
-
- -- Meanwhile these nodes should be considered in experimental form, and
- -- should be ignored by all code generating back ends. ???
+ -- require special processing. They are only generated if SCIL
+ -- generation is enabled. A standard tree-walk will not encounter
+ -- these nodes even if they are present; these nodes are only
+ -- accessible via the function SCIL_LL.Get_SCIL_Node.
-- N_SCIL_Dispatch_Table_Tag_Init
-- Sloc references a node for a tag initialization
-- SCIL_Entity (Node4-Sem)
+ --
+ -- An N_SCIL_Dispatch_Table_Tag_Init node may be associated (via
+ -- Get_SCIL_Node) with the N_Object_Declaration node corresponding to
+ -- the declaration of the dispatch table for a tagged type.
-- N_SCIL_Dispatching_Call
-- Sloc references the node of a dispatching call
-- SCIL_Target_Prim (Node2-Sem)
-- SCIL_Entity (Node4-Sem)
-- SCIL_Controlling_Tag (Node5-Sem)
+ --
+ -- An N_Scil_Dispatching call node may be associated (via Get_SCIL_Node)
+ -- with the N_Procedure_Call or N_Function_Call node (or a rewriting
+ -- thereof) corresponding to a dispatching call.
-- N_SCIL_Membership_Test
-- Sloc references the node of a membership test
-- SCIL_Tag_Value (Node5-Sem)
-- SCIL_Entity (Node4-Sem)
+ --
+ -- An N_Scil_Membership_Test node may be associated (via Get_SCIL_Node)
+ -- with the N_In node (or a rewriting thereof) corresponding to a
+ -- classwide membership test.
---------------------
-- Subprogram_Info --
projects / platform / upstream / linaro-gcc.git / commitdiff