This patch utilizes compilation switch -gnatd.v to enforce the SPARK rules for
elaboration in SPARK code. The affected scenarios are calls and instantiations.
If the switch is active, the ABE mechanism will verify that the scenarios have
fulfilled their Elaborate[_All] requirements. Otherwise the static model of the
ABE mechanism will install implicit Elaborate[_All] pragmas to meet these
requirements.
------------
-- Source --
------------
-- server.ads
package Server with SPARK_Mode is
generic
procedure Gen_Proc;
generic
package Gen_Pack is
procedure Proc;
end Gen_Pack;
function Func return Boolean;
end Server;
-- server.adb
with Ada.Text_IO; use Ada.Text_IO;
package body Server with SPARK_Mode is
procedure Gen_Proc is
begin
Put_Line ("Gen_Proc");
end Gen_Proc;
package body Gen_Pack is
procedure Proc is
begin
Put_Line ("Proc");
end Proc;
end Gen_Pack;
function Func return Boolean is
begin
Put_Line ("Func");
return True;
end Func;
end Server;
-- client.ads
with Server;
package Client with SPARK_Mode is
procedure Inst_Proc is new Server.Gen_Proc;
package Inst_Pack is new Server.Gen_Pack;
Val : constant Boolean := Server.Func;
end Client;
----------------------------
-- Compilation and output --
----------------------------
$ echo "Ignore SPARK rules"
$ gcc -c client.ads
$ echo "Apply SPARK rules"
$ gcc -c client.ads -gnatd.v
Ignore SPARK rules
Apply SPARK rules
client.ads:4:04: instantiation of "Gen_Proc" during elaboration in SPARK
client.ads:4:04: unit "Client" requires pragma "Elaborate_All" for "Server"
client.ads:4:04: spec of unit "Client" elaborated
client.ads:4:04: procedure "Gen_Proc" instantiated as "Inst_Proc" at line 4
client.ads:5:04: instantiation of "Gen_Pack" during elaboration in SPARK
client.ads:5:04: unit "Client" requires pragma "Elaborate" for "Server"
client.ads:5:04: spec of unit "Client" elaborated
client.ads:5:04: package "Gen_Pack" instantiated as "Inst_Pack" at line 5
client.ads:7:36: call to "Func" during elaboration in SPARK
client.ads:7:36: unit "Client" requires pragma "Elaborate_All" for "Server"
client.ads:7:36: spec of unit "Client" elaborated
client.ads:7:36: function "Func" called at line 7
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-10-14 Hristian Kirtchev <kirtc...@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.
Index: doc/gnat_ugn/elaboration_order_handling_in_gnat.rst
===================================================================
--- doc/gnat_ugn/elaboration_order_handling_in_gnat.rst (revision 253753)
+++ doc/gnat_ugn/elaboration_order_handling_in_gnat.rst (working copy)
@@ -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
Index: sem_elab.adb
===================================================================
--- sem_elab.adb (revision 253756)
+++ sem_elab.adb (working copy)
@@ -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
Index: debug.adb
===================================================================
--- debug.adb (revision 253753)
+++ debug.adb (working copy)
@@ -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.
Index: gnat_ugn.texi
===================================================================
--- gnat_ugn.texi (revision 253753)
+++ gnat_ugn.texi (working copy)
@@ -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
