===================================================================
@@ -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;
===================================================================
@@ -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;
===================================================================
@@ -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);