This patch modifies the generation of the invariant procedure body as follows:
* The body of the "partial" invariant procedure is still generated at the
end of the visible declarations.
* The body of the "full" invariant procedure is generated when the related
type is frozen or at the end of the private declarations.
The last case ensures that the assertion expression will be resolved in the
proper context even when freezing does not take place before the end of the
private declarations has been reached. This scenario arises in two ways:
* A private type is declared within a nested package. Reaching the end of
the private declarations does not cause freezing because the package is not
library-level.
* The compilation is subject compilation switch -gnatd.F which enables SPARK
mode. This in turn suppresses freezing.
This patch also ensures that an invariant procedure is never treated as a
primitive of a tagged type.
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-01-19 Hristian Kirtchev <kirtc...@adacore.com>
* sem_ch3.adb Add with and use clauses for Exp_Ch7.
(Analyze_Declarations): Create the DIC and Invariant
procedure bodies s after all freezing has taken place.
(Build_Assertion_Bodies): New routine.
* sem_ch7.adb Remove the with and use clauses for Exp_Ch7
and Exp_Util.
(Analyze_Package_Specification): Remove the
generation of the DIC and Invariant procedure bodies. This is
now done by Analyze_Declarations.
* sem_disp.adb (Check_Dispatching_Operation): DIC and Invariant
procedures are never treated as primitives.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 244622)
+++ sem_ch3.adb (working copy)
@@ -33,6 +33,7 @@
with Errout; use Errout;
with Eval_Fat; use Eval_Fat;
with Exp_Ch3; use Exp_Ch3;
+with Exp_Ch7; use Exp_Ch7;
with Exp_Ch9; use Exp_Ch9;
with Exp_Disp; use Exp_Disp;
with Exp_Dist; use Exp_Dist;
@@ -2153,6 +2154,17 @@
-- (They have the sloc of the label as found in the source, and that
-- is ahead of the current declarative part).
+ procedure Build_Assertion_Bodies (Decls : List_Id; Context : Node_Id);
+ -- Create the subprogram bodies which verify the run-time semantics of
+ -- the pragmas listed below for each elibigle type found in declarative
+ -- list Decls. The pragmas are:
+ --
+ -- Default_Initial_Condition
+ -- Invariant
+ -- Type_Invariant
+ --
+ -- Context denotes the owner of the declarative list.
+
procedure Check_Entry_Contracts;
-- Perform a pre-analysis of the pre- and postconditions of an entry
-- declaration. This must be done before full resolution and creation
@@ -2195,6 +2207,85 @@
end loop;
end Adjust_Decl;
+ ----------------------------
+ -- Build_Assertion_Bodies --
+ ----------------------------
+
+ procedure Build_Assertion_Bodies (Decls : List_Id; Context : Node_Id) is
+ procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id);
+ -- Create the subprogram bodies which verify the run-time semantics
+ -- of the pragmas listed below for type Typ. The pragmas are:
+ --
+ -- Default_Initial_Condition
+ -- Invariant
+ -- Type_Invariant
+
+ -------------------------------------
+ -- Build_Assertion_Bodies_For_Type --
+ -------------------------------------
+
+ procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id) is
+ begin
+ -- Preanalyze and resolve the Default_Initial_Condition assertion
+ -- expression at the end of the declarations to catch any errors.
+
+ if Has_DIC (Typ) then
+ Build_DIC_Procedure_Body (Typ);
+ end if;
+
+ if Nkind (Context) = N_Package_Specification then
+
+ -- Preanalyze and resolve the invariants of a private type
+ -- at the end of the visible declarations to catch potential
+ -- errors. Inherited class-wide invariants are not included
+ -- because they have already been resolved.
+
+ if Decls = Visible_Declarations (Context)
+ and then Ekind_In (Typ, E_Limited_Private_Type,
+ E_Private_Type,
+ E_Record_Type_With_Private)
+ and then Has_Own_Invariants (Typ)
+ then
+ Build_Invariant_Procedure_Body
+ (Typ => Typ,
+ Partial_Invariant => True);
+
+ -- Preanalyze and resolve the invariants of a private type's
+ -- full view at the end of the private declarations to catch
+ -- potential errors.
+
+ elsif Decls = Private_Declarations (Context)
+ and then not Is_Private_Type (Typ)
+ and then Has_Private_Declaration (Typ)
+ and then Has_Invariants (Typ)
+ then
+ Build_Invariant_Procedure_Body (Typ);
+ end if;
+ end if;
+ end Build_Assertion_Bodies_For_Type;
+
+ -- Local variables
+
+ Decl : Node_Id;
+ Decl_Id : Entity_Id;
+
+ -- Start of processing for Build_Assertion_Bodies
+
+ begin
+ Decl := First (Decls);
+ while Present (Decl) loop
+ if Is_Declaration (Decl) then
+ Decl_Id := Defining_Entity (Decl);
+
+ if Is_Type (Decl_Id) then
+ Build_Assertion_Bodies_For_Type (Decl_Id);
+ end if;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end Build_Assertion_Bodies;
+
---------------------------
-- Check_Entry_Contracts --
---------------------------
@@ -2581,11 +2672,13 @@
Decl := Next_Decl;
end loop;
- -- Analyze the contracts of packages and their bodies
+ -- Post-freezing actions
if Present (L) then
Context := Parent (L);
+ -- Analyze the contracts of packages and their bodies
+
if Nkind (Context) = N_Package_Specification then
-- When a package has private declarations, its contract must be
@@ -2643,6 +2736,15 @@
-- protected, subprogram, or task body (SPARK RM 7.2.2(3)).
Check_State_Refinements (Context);
+
+ -- Create the subprogram bodies which verify the run-time semantics
+ -- of pragmas Default_Initial_Condition and [Type_]Invariant for all
+ -- types within the current declarative list. This ensures that all
+ -- assertion expressions are preanalyzed and resolved at the end of
+ -- the declarative part. Note that the resolution happens even when
+ -- freezing does not take place.
+
+ Build_Assertion_Bodies (L, Context);
end if;
end Analyze_Declarations;
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 244612)
+++ sem_ch7.adb (working copy)
@@ -35,11 +35,9 @@
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
-with Exp_Ch7; use Exp_Ch7;
with Exp_Disp; use Exp_Disp;
with Exp_Dist; use Exp_Dist;
with Exp_Dbug; use Exp_Dbug;
-with Exp_Util; use Exp_Util;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Lib; use Lib;
@@ -1432,30 +1430,6 @@
Error_Msg_N ("no declaration in visible part for incomplete}", E);
end if;
- if Is_Type (E) then
-
- -- Preanalyze and resolve the Default_Initial_Condition assertion
- -- expression at the end of the visible declarations to catch any
- -- errors.
-
- if Has_DIC (E) then
- Build_DIC_Procedure_Body (E);
- end if;
-
- -- Preanalyze and resolve the invariants of a private type at the
- -- end of the visible declarations to catch potential errors. Note
- -- that inherited class-wide invariants are not considered because
- -- they have already been resolved.
-
- if Ekind_In (E, E_Limited_Private_Type,
- E_Private_Type,
- E_Record_Type_With_Private)
- and then Has_Own_Invariants (E)
- then
- Build_Invariant_Procedure_Body (E, Partial_Invariant => True);
- end if;
- end if;
-
Next_Entity (E);
end loop;
@@ -1635,30 +1609,6 @@
("full view of & does not have preelaborable initialization", E);
end if;
- if Is_Type (E) and then Serious_Errors_Detected > 0 then
-
- -- Preanalyze and resolve the Default_Initial_Condition assertion
- -- expression at the end of the private declarations when freezing
- -- did not take place due to errors or because the context is a
- -- generic unit.
-
- if Has_DIC (E) then
- Build_DIC_Procedure_Body (E);
- end if;
-
- -- Preanalyze and resolve the invariants of a private type's full
- -- view at the end of the private declarations in case freezing
- -- did not take place either due to errors or because the context
- -- is a generic unit.
-
- if not Is_Private_Type (E)
- and then Has_Private_Declaration (E)
- and then Has_Invariants (E)
- then
- Build_Invariant_Procedure_Body (E);
- end if;
- end if;
-
Next_Entity (E);
end loop;
Index: sem_disp.adb
===================================================================
--- sem_disp.adb (revision 244612)
+++ sem_disp.adb (working copy)
@@ -932,14 +932,30 @@
---------------------------------
procedure Check_Dispatching_Operation (Subp, Old_Subp : Entity_Id) is
- Tagged_Type : Entity_Id;
+ Body_Is_Last_Primitive : Boolean := False;
Has_Dispatching_Parent : Boolean := False;
- Body_Is_Last_Primitive : Boolean := False;
Ovr_Subp : Entity_Id := Empty;
+ Tagged_Type : Entity_Id;
begin
- if not Ekind_In (Subp, E_Procedure, E_Function) then
+ if not Ekind_In (Subp, E_Function, E_Procedure) then
return;
+
+ -- The Default_Initial_Condition procedure is not a primitive subprogram
+ -- even if it relates to a tagged type. This routine is not meant to be
+ -- inherited or overridden.
+
+ elsif Is_DIC_Procedure (Subp) then
+ return;
+
+ -- The "partial" and "full" type invariant procedures are not primitive
+ -- subprograms even if they relate to a tagged type. These routines are
+ -- not meant to be inherited or overridden.
+
+ elsif Is_Invariant_Procedure (Subp)
+ or else Is_Partial_Invariant_Procedure (Subp)
+ then
+ return;
end if;
Set_Is_Dispatching_Operation (Subp, False);
