+2017-10-14 Eric Botcazou <ebotcazou@adacore.com>
+
+ * layout.ads (Set_Elem_Alignment): Add Align parameter defaulted to 0.
+ * layout.adb (Set_Elem_Alignment): Likewise. Use M name as maximum
+ alignment for consistency. If Align is non-zero, use the minimum of
+ Align and M for the alignment.
+ * cstand.adb (Build_Float_Type): Use Set_Elem_Alignment instead of
+ setting the alignment directly.
+
+2017-10-14 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_prag.adb (Analyze_Pragma, case Check): Defer evaluation of the
+ optional string in an Assert pragma until the expansion of the pragma
+ has rewritten it as a conditional statement, so that the string
+ argument is only evaluaed if the assertion fails. This is mandated by
+ RM 11.4.2.
+
+2017-10-14 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * debug.adb: Switch -gnatd.v and associated flag are now used to
+ enforce the SPARK rules for elaboration in SPARK code.
+ * sem_elab.adb: Describe switch -gnatd.v.
+ (Process_Call): Verify the SPARK rules only when -gnatd.v is in effect.
+ (Process_Instantiation): Verify the SPARK rules only when -gnatd.v is
+ in effect.
+ (Process_Variable_Assignment): Clarify why variable assignments are
+ processed reglardless of whether -gnatd.v is in effect.
+ * doc/gnat_ugn/elaboration_order_handling_in_gnat.rst: Update the
+ sections on elaboration code and compilation switches.
+ * gnat_ugn.texi: Regenerate.
+
+2017-10-14 Gary Dismukes <dismukes@adacore.com>
+
+ * exp_util.adb, freeze.adb, sem_aggr.adb, sem_util.ads, sem_util.adb,
+ sem_warn.adb: Minor reformattings.
+
2017-10-14 Ed Schonberg <schonberg@adacore.com>
* doc/gnat_rm/implementation_defined_aspects.rst: Add documentation
Init_Digits_Value (E, Digs);
Set_Float_Rep (E, Rep);
Init_Size (E, Siz);
- Set_Alignment (E, UI_From_Int (Align));
+ Set_Elem_Alignment (E, Align);
Set_Float_Bounds (E);
Set_Is_Frozen (E);
Set_Is_Public (E);
-- d.s Strict secondary stack management
-- d.t Disable static allocation of library level dispatch tables
-- d.u Enable Modify_Tree_For_C (update tree for c)
- -- d.v
+ -- d.v Enforce SPARK elaboration rules in SPARK code
-- d.w Do not check for infinite loops
-- d.x No exception handlers
-- d.y Disable implicit pragma Elaborate_All on task bodies
-- d.u Sets Modify_Tree_For_C mode in which tree is modified to make it
-- easier to generate code using a C compiler.
+ -- d.v This flag enforces the elaboration rules defined in the SPARK
+ -- Reference Manual, chapter 7.7, to all SPARK code within a unit. As
+ -- a result, constructs which violate the rules in chapter 7.7 are no
+ -- longer accepted, even if the implementation is able to statically
+ -- ensure that accepting these constructs does not introduce the
+ -- possibility of failing an elaboration check.
+
-- d.w This flag turns off the scanning of loops to detect possible
-- infinite loops.
=================
The sequence by which the elaboration code of all units within a partition is
-executed is referred to as **elaboration order**. The elaboration order depends
-on the following factors:
+executed is referred to as **elaboration order**.
+
+Within a single unit, elaboration code is executed in sequential order.
+
+::
+
+ package body Client is
+ Result : ... := Server.Func;
+
+ procedure Proc is
+ package Inst is new Server.Gen;
+ begin
+ Inst.Eval (Result);
+ end Proc;
+ begin
+ Proc;
+ end Client;
+
+In the example above, the elaboration order within package body ``Client`` is
+as follows:
+
+1. The object declaration of ``Result`` is elaborated.
+
+ * Function ``Server.Func`` is invoked.
+
+2. The subprogram body of ``Proc`` is elaborated.
+
+3. Procedure ``Proc`` is invoked.
+
+ * Generic unit ``Server.Gen`` is instantiated as ``Inst``.
+
+ * Instance ``Inst`` is elaborated.
+
+ * Procedure ``Inst.Eval`` is invoked.
+
+The elaboration order of all units within a partition depends on the following
+factors:
* |withed| units
a partition is elaboration code. GNAT performs very few diagnostics and
generates run-time checks to verify the elaboration order of a program. This
behavior is identical to that specified by the Ada Reference Manual. The
- dynamic model is enabled with compilation switch :switch:`-gnatE`.
+ dynamic model is enabled with compiler switch :switch:`-gnatE`.
.. index:: Static elaboration model
The SPARK model is identical to the static model in its handling of internal
targets. The SPARK model, however, requires explicit ``Elaborate`` or
``Elaborate_All`` pragmas to be present in the program when a target is
-external, and emits hard errors instead of warnings:
+external, and compiler switch :switch:`-gnatd.v` is in effect.
::
* *Switch to more permissive elaboration model*
If the compilation was performed using the static model, enable the dynamic
- model with compilation switch :switch:`-gnatE`. GNAT will no longer generate
+ model with compiler switch :switch:`-gnatE`. GNAT will no longer generate
implicit ``Elaborate`` and ``Elaborate_All`` pragmas, resulting in a behavior
identical to that specified by the Ada Reference Manual. The binder will
generate an executable program that may or may not raise ``Program_Error``,
When this switch is in effect, GNAT will ignore ``'Access`` of an entry,
operator, or subprogram when the static model is in effect.
+.. index:: -gnatd.v (gnat)
+
+:switch:`-gnatd.v`
+ Enforce SPARK elaboration rules in SPARK code
+
+ When this switch is in effect, GNAT will enforce the SPARK rules of
+ elaboration as defined in the SPARK Reference Manual, section 7.7. As a
+ result, constructs which violate the SPARK elaboration rules are no longer
+ accepted, even if GNAT is able to statically ensure that these constructs
+ will not lead to ABE problems.
+
.. index:: -gnatd.y (gnat)
:switch:`-gnatd.y`
- *SPARK model*
GNAT will indicate how an elaboration requirement is met by the context of
- a unit.
+ a unit. This diagnostic requires compiler switch :switch:`-gnatd.v`.
::
elaboration order, then apart from possible cases involing dispatching calls
and access-to-subprogram types, the program is free of elaboration errors.
If it is important for the program to be portable to compilers other than GNAT,
-then the programmer should use compilation switch :switch:`-gnatel` and
-consider the messages about missing or implicitly created ``Elaborate`` and
+then the programmer should use compiler switch :switch:`-gnatel` and consider
+the messages about missing or implicitly created ``Elaborate`` and
``Elaborate_All`` pragmas.
If the binder reports an elaboration circularity, the programmer has several
-- Exp_Ch2.Expand_Renaming). Otherwise the temporary must be
-- elaborated by gigi, and is of course not to be replaced in-line
-- by the expression it renames, which would defeat the purpose of
- -- removing the side-effect.
+ -- removing the side effect.
if Nkind_In (Exp, N_Selected_Component, N_Indexed_Component)
and then Has_Non_Standard_Rep (Etype (Prefix (Exp)))
and then Variable_Ref
then
-- Exception is a prefix that is the result of a previous removal
- -- of side-effects.
+ -- of side effects.
return Is_Entity_Name (Prefix (N))
and then not Comes_From_Source (Prefix (N))
-- The analysis of the expression may generate insert actions,
-- which of course must not be executed. We wrap those actions
-- in a procedure that is not called, and later on eliminated.
- -- The following cases have no side-effects, and are analyzed
+ -- The following cases have no side effects, and are analyzed
-- directly.
if Nkind (Dcopy) = N_Identifier
@copying
@quotation
-GNAT User's Guide for Native Platforms , Oct 09, 2017
+GNAT User's Guide for Native Platforms , Oct 14, 2017
AdaCore
The sequence by which the elaboration code of all units within a partition is
-executed is referred to as @strong{elaboration order}. The elaboration order depends
-on the following factors:
+executed is referred to as @strong{elaboration order}.
+
+Within a single unit, elaboration code is executed in sequential order.
+
+@example
+package body Client is
+ Result : ... := Server.Func;
+
+ procedure Proc is
+ package Inst is new Server.Gen;
+ begin
+ Inst.Eval (Result);
+ end Proc;
+begin
+ Proc;
+end Client;
+@end example
+
+In the example above, the elaboration order within package body @code{Client} is
+as follows:
+
+
+@enumerate
+
+@item
+The object declaration of @code{Result} is elaborated.
+
+
+@itemize *
+
+@item
+Function @code{Server.Func} is invoked.
+@end itemize
+
+@item
+The subprogram body of @code{Proc} is elaborated.
+
+@item
+Procedure @code{Proc} is invoked.
+
+
+@itemize *
+
+@item
+Generic unit @code{Server.Gen} is instantiated as @code{Inst}.
+
+@item
+Instance @code{Inst} is elaborated.
+
+@item
+Procedure @code{Inst.Eval} is invoked.
+@end itemize
+@end enumerate
+
+The elaboration order of all units within a partition depends on the following
+factors:
@itemize *
a partition is elaboration code. GNAT performs very few diagnostics and
generates run-time checks to verify the elaboration order of a program. This
behavior is identical to that specified by the Ada Reference Manual. The
-dynamic model is enabled with compilation switch @code{-gnatE}.
+dynamic model is enabled with compiler switch @code{-gnatE}.
@end itemize
@geindex Static elaboration model
The SPARK model is identical to the static model in its handling of internal
targets. The SPARK model, however, requires explicit @code{Elaborate} or
@code{Elaborate_All} pragmas to be present in the program when a target is
-external, and emits hard errors instead of warnings:
+external, and compiler switch @code{-gnatd.v} is in effect.
@example
1. with Server;
@emph{Switch to more permissive elaboration model}
If the compilation was performed using the static model, enable the dynamic
-model with compilation switch @code{-gnatE}. GNAT will no longer generate
+model with compiler switch @code{-gnatE}. GNAT will no longer generate
implicit @code{Elaborate} and @code{Elaborate_All} pragmas, resulting in a behavior
identical to that specified by the Ada Reference Manual. The binder will
generate an executable program that may or may not raise @code{Program_Error},
operator, or subprogram when the static model is in effect.
@end table
+@geindex -gnatd.v (gnat)
+
+
+@table @asis
+
+@item @code{-gnatd.v}
+
+Enforce SPARK elaboration rules in SPARK code
+
+When this switch is in effect, GNAT will enforce the SPARK rules of
+elaboration as defined in the SPARK Reference Manual, section 7.7. As a
+result, constructs which violate the SPARK elaboration rules are no longer
+accepted, even if GNAT is able to statically ensure that these constructs
+will not lead to ABE problems.
+@end table
+
@geindex -gnatd.y (gnat)
@emph{SPARK model}
GNAT will indicate how an elaboration requirement is met by the context of
-a unit.
+a unit. This diagnostic requires compiler switch @code{-gnatd.v}.
@example
1. with Server; pragma Elaborate_All (Server);
elaboration order, then apart from possible cases involing dispatching calls
and access-to-subprogram types, the program is free of elaboration errors.
If it is important for the program to be portable to compilers other than GNAT,
-then the programmer should use compilation switch @code{-gnatel} and
-consider the messages about missing or implicitly created @code{Elaborate} and
+then the programmer should use compiler switch @code{-gnatel} and consider
+the messages about missing or implicitly created @code{Elaborate} and
@code{Elaborate_All} pragmas.
If the binder reports an elaboration circularity, the programmer has several
-- Set_Elem_Alignment --
------------------------
- procedure Set_Elem_Alignment (E : Entity_Id) is
+ procedure Set_Elem_Alignment (E : Entity_Id; Align : Nat := 0) is
begin
-- Do not set alignment for packed array types, this is handled in the
-- backend.
return;
end if;
- -- Here we calculate the alignment as the largest power of two multiple
- -- of System.Storage_Unit that does not exceed either the object size of
- -- the type, or the maximum allowed alignment.
+ -- We attempt to set the alignment in all the other cases
declare
S : Int;
A : Nat;
-
- Max_Alignment : Nat;
+ M : Nat;
begin
-- The given Esize may be larger that int'last because of a previous
and then S = 8
and then Is_Floating_Point_Type (E)
then
- Max_Alignment := Ttypes.Target_Double_Float_Alignment;
+ M := Ttypes.Target_Double_Float_Alignment;
-- If the default alignment of "double" or larger scalar types is
-- specifically capped, enforce the cap.
and then S >= 8
and then Is_Scalar_Type (E)
then
- Max_Alignment := Ttypes.Target_Double_Scalar_Alignment;
+ M := Ttypes.Target_Double_Scalar_Alignment;
-- Otherwise enforce the overall alignment cap
else
- Max_Alignment := Ttypes.Maximum_Alignment;
+ M := Ttypes.Maximum_Alignment;
end if;
- A := 1;
- while 2 * A <= Max_Alignment and then 2 * A <= S loop
- A := 2 * A;
- end loop;
+ -- We calculate the alignment as the largest power-of-two multiple
+ -- of System.Storage_Unit that does not exceed the object size of
+ -- the type and the maximum allowed alignment, if none was specified.
+ -- Otherwise we only cap it to the maximum allowed alignment.
+
+ if Align = 0 then
+ A := 1;
+ while 2 * A <= S and then 2 * A <= M loop
+ A := 2 * A;
+ end loop;
+ else
+ A := Nat'Min (Align, M);
+ end if;
-- If alignment is currently not set, then we can safely set it to
-- this new calculated value.
-- types, the RM_Size is simply set to zero. This routine also sets
-- the Is_Constrained flag in Def_Id.
- procedure Set_Elem_Alignment (E : Entity_Id);
+ procedure Set_Elem_Alignment (E : Entity_Id; Align : Nat := 0);
-- The front end always sets alignments for elementary types by calling
-- this procedure. Note that we have to do this for discrete types (since
-- the Alignment attribute is static), so we might as well do it for all
- -- elementary types, since the processing is the same.
+ -- elementary types, as the processing is the same. If Align is nonzero,
+ -- it is an external alignment setting that we must respect.
end Layout;
-- unless the expression covers a single component, or the
-- expander is inactive.
- -- In SPARK mode, expressions that can perform side-effects will
+ -- In SPARK mode, expressions that can perform side effects will
-- be recognized by the gnat2why back-end, and the whole
-- subprogram will be ignored. So semantic analysis can be
-- performed safely.
-- This is redundant if the others_choice covers only
-- one component (small optimization possible???), but
-- indispensable otherwise, because each one must be
- -- expanded individually to preserve side-effects.
+ -- expanded individually to preserve side effects.
-- Ada 2005 (AI-287): In case of default initialization
-- of components, we duplicate the corresponding default
-- expansion is delayed until the enclosing aggregate is expanded
-- into assignments. In that case, do not generate checks on the
-- expression, because they will be generated later, and will other-
- -- wise force a copy (to remove side-effects) that would leave a
+ -- wise force a copy (to remove side effects) that would leave a
-- dynamic-sized aggregate in the code, something that gigi cannot
-- handle.
-- entries, operators, and subprograms. As a result, the scenarios
-- are not recorder or processed.
--
+ -- -gnatd.v enforce SPARK elaboration rules in SPARK code
+ --
+ -- The ABE mechanism applies some of the SPARK elaboration rules
+ -- defined in the SPARK reference manual, chapter 7.7. Note that
+ -- certain rules are always enforced, regardless of whether the
+ -- switch is active.
+ --
-- -gnatd.y disable implicit pragma Elaborate_All on task bodies
--
-- The ABE mechanism does not generate implicit Elaborate_All when
elsif Is_Up_Level_Target (Target_Attrs.Spec_Decl) then
return;
- -- The SPARK rules are in effect
+ -- The SPARK rules are verified only when -gnatd.v (enforce SPARK
+ -- elaboration rules in SPARK code) is in effect.
- elsif SPARK_Rules_On then
+ elsif SPARK_Rules_On and Debug_Flag_Dot_V then
Process_Call_SPARK
(Call => Call,
Call_Attrs => Call_Attrs,
Target_Id => Target_Id,
Target_Attrs => Target_Attrs);
- -- Otherwise the Ada rules are in effect
+ -- Otherwise the Ada rules are in effect, or SPARK code is allowed to
+ -- violate the SPARK rules.
else
Process_Call_Ada
elsif Is_Up_Level_Target (Gen_Attrs.Spec_Decl) then
return;
- -- The SPARK rules are in effect
+ -- The SPARK rules are verified only when -gnatd.v (enforce SPARK
+ -- elaboration rules in SPARK code) is in effect.
- elsif SPARK_Rules_On then
+ elsif SPARK_Rules_On and Debug_Flag_Dot_V then
Process_Instantiation_SPARK
(Exp_Inst => Exp_Inst,
Inst => Inst,
Gen_Id => Gen_Id,
Gen_Attrs => Gen_Attrs);
- -- Otherwise the Ada rules are in effect
+ -- Otherwise the Ada rules are in effect, or SPARK code is allowed to
+ -- violate the SPARK rules.
else
Process_Instantiation_Ada
In_SPARK => SPARK_Rules_On);
end if;
- -- The SPARK rules are in effect
+ -- The SPARK rules are in effect. These rules are applied regardless of
+ -- whether -gnatd.v (enforce SPARK elaboration rules in SPARK code) is
+ -- in effect because the static model cannot ensure safe assignment of
+ -- variables.
if SPARK_Rules_On then
Process_Variable_Assignment_SPARK
-- If checks are not on we don't want any expansion (since
-- such expansion would not get properly deleted) but
-- we do want to analyze (to get proper references).
- -- The Preanalyze_And_Resolve routine does just what we want
+ -- The Preanalyze_And_Resolve routine does just what we want.
+ -- Ditto if pragma is active, because it will be rewritten
+ -- as an if-statement whose analysis will complete analysis
+ -- and expansion of the string message. This makes a
+ -- difference in the unusual case where the expression for
+ -- the string may have a side effect, such as raising an
+ -- exception. This is mandated by RM 11.4.2, which specifies
+ -- that the string expression is only evaluated if the
+ -- check fails and Assertion_Error is to be raised.
+
+ Preanalyze_And_Resolve (Str, Standard_String);
- if Is_Ignored (N) then
- Preanalyze_And_Resolve (Str, Standard_String);
-
- -- Otherwise we need a proper analysis and expansion
-
- else
- Analyze_And_Resolve (Str, Standard_String);
- end if;
end if;
-- Now you might think we could just do the same with the Boolean
end if;
-- A discriminant check on a selected component may be expanded
- -- into a dereference when removing side-effects. Recover the
+ -- into a dereference when removing side effects. Recover the
-- original node and its type, which may be unconstrained.
elsif Nkind (P) = N_Explicit_Dereference
-- This construct appears in the context of dispatching calls.
function Reference_To (Obj : Node_Id) return Node_Id;
- -- An explicit dereference is created when removing side-effects from
+ -- An explicit dereference is created when removing side effects from
-- expressions for constraint checking purposes. In this case a local
-- access type is created for it. The correct access level is that of
-- the original source node. We detect this case by noting that the
-- type of the other operand is a descendant of System.Address.
function Number_Of_Elements_In_Array (T : Entity_Id) return Int;
- -- Returns the number elements in the array T if the index bounds of T is
- -- known at compile time. If the bounds are not known at compile time, the
- -- function returns the value zero.
+ -- Returns the number of elements in the array T if the index bounds of T
+ -- is known at compile time. If the bounds are not known at compile time,
+ -- the function returns the value zero.
function Object_Access_Level (Obj : Node_Id) return Uint;
-- Return the accessibility level of the view of the object Obj. For
end if;
-- If the condition contains a function call, we consider it may
- -- be modified by side-effects from a procedure call. Otherwise,
+ -- be modified by side effects from a procedure call. Otherwise,
-- we consider the condition may not be modified, although that
-- might happen if Variable is itself a by-reference parameter,
-- and the procedure called modifies the global object referred to
projects / gcc.git / commitdiff