===================================================================
@@ -133,9 +133,44 @@
=================
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
* purity of units
@@ -571,7 +606,7 @@
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
@@ -860,7 +895,7 @@
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.
::
@@ -987,7 +1022,7 @@
* *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``,
@@ -1504,6 +1539,17 @@
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`
@@ -1558,7 +1604,7 @@
- *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`.
::
@@ -1612,8 +1658,8 @@
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
===================================================================
@@ -361,6 +361,13 @@
-- 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
@@ -6891,16 +6898,18 @@
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
@@ -7459,9 +7468,10 @@
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,
@@ -7469,7 +7479,8 @@
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
@@ -7869,7 +7880,10 @@
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
===================================================================
@@ -112,7 +112,7 @@
-- 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
@@ -600,6 +600,13 @@
-- 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.
===================================================================
@@ -21,7 +21,7 @@
@copying
@quotation
-GNAT User's Guide for Native Platforms , Oct 09, 2017
+GNAT User's Guide for Native Platforms , Oct 14, 2017
AdaCore
@@ -27187,13 +27187,67 @@
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 *
+
+@item
@emph{with}ed units
@item
@@ -27689,7 +27743,7 @@
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
@@ -28001,7 +28055,7 @@
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;
@@ -28146,7 +28200,7 @@
@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},
@@ -28711,6 +28765,22 @@
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)
@@ -28785,7 +28855,7 @@
@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);
@@ -28846,8 +28916,8 @@
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