===================================================================
@@ -62,6 +62,7 @@ with Sem_Dist; use Sem_Dist;
with Sem_Elim; use Sem_Elim;
with Sem_Eval; use Sem_Eval;
with Sem_Mech; use Sem_Mech;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Smem; use Sem_Smem;
with Sem_Type; use Sem_Type;
@@ -2069,6 +2070,35 @@ package body Sem_Ch3 is
D := Next_Node;
end loop;
+
+ -- One more thing to do, we need to scan the declarations to check
+ -- for any precondition/postcondition pragmas (Pre/Post aspects have
+ -- by this stage been converted into corresponding pragmas). It is
+ -- at this point that we analyze the expressions in such pragmas,
+ -- to implement the delayed visibility requirement.
+
+ declare
+ Decl : Node_Id;
+ Spec : Node_Id;
+ Sent : Entity_Id;
+ Prag : Node_Id;
+
+ begin
+ Decl := First (L);
+ while Present (Decl) loop
+ if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
+ Spec := Specification (Original_Node (Decl));
+ Sent := Defining_Unit_Name (Spec);
+ Prag := Spec_PPC_List (Sent);
+ while Present (Prag) loop
+ Analyze_PPC_In_Decl_Part (Prag, Sent);
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end;
end Analyze_Declarations;
-----------------------------------
===================================================================
@@ -55,7 +55,6 @@ with Sem_Ch12; use Sem_Ch12;
with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
with Sem_Eval; use Sem_Eval;
-with Sem_Prag; use Sem_Prag;
with Sem_Util; use Sem_Util;
with Sem_Warn; use Sem_Warn;
with Snames; use Snames;
@@ -872,12 +871,6 @@ package body Sem_Ch7 is
-- private_with_clauses, and remove them at the end of the nested
-- package.
- procedure Analyze_PPCs (Decls : List_Id);
- -- Given a list of declarations, go through looking for subprogram
- -- specs, and for each one found, analyze any pre/postconditions that
- -- are chained to the spec. This is the implementation of the late
- -- visibility analysis for preconditions and postconditions in specs.
-
procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
-- Clears constant indications (Never_Set_In_Source, Constant_Value, and
-- Is_True_Constant) on all variables that are entities of Id, and on
@@ -906,33 +899,6 @@ package body Sem_Ch7 is
-- private part rather than being done in Sem_Ch12.Install_Parent
-- (which is where the parents' visible declarations are installed).
- ------------------
- -- Analyze_PPCs --
- ------------------
-
- procedure Analyze_PPCs (Decls : List_Id) is
- Decl : Node_Id;
- Spec : Node_Id;
- Sent : Entity_Id;
- Prag : Node_Id;
-
- begin
- Decl := First (Decls);
- while Present (Decl) loop
- if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
- Spec := Specification (Original_Node (Decl));
- Sent := Defining_Unit_Name (Spec);
- Prag := Spec_PPC_List (Sent);
- while Present (Prag) loop
- Analyze_PPC_In_Decl_Part (Prag, Sent);
- Prag := Next_Pragma (Prag);
- end loop;
- end if;
-
- Next (Decl);
- end loop;
- end Analyze_PPCs;
-
---------------------
-- Clear_Constants --
---------------------
@@ -1161,7 +1127,6 @@ package body Sem_Ch7 is
begin
if Present (Vis_Decls) then
Analyze_Declarations (Vis_Decls);
- Analyze_PPCs (Vis_Decls);
end if;
-- Verify that incomplete types have received full declarations
@@ -1296,7 +1261,6 @@ package body Sem_Ch7 is
end if;
Analyze_Declarations (Priv_Decls);
- Analyze_PPCs (Priv_Decls);
-- Check the private declarations for incomplete deferred constants
===================================================================
@@ -2581,7 +2581,10 @@ package body Einfo is
function Spec_PPC_List (Id : E) return N is
begin
- pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+ pragma Assert
+ (Ekind (Id) = E_Entry
+ or else Is_Subprogram (Id)
+ or else Is_Generic_Subprogram (Id));
return Node24 (Id);
end Spec_PPC_List;
@@ -5046,7 +5049,10 @@ package body Einfo is
procedure Set_Spec_PPC_List (Id : E; V : N) is
begin
- pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+ pragma Assert
+ (Ekind_In (Id, E_Entry, E_Void)
+ or else Is_Subprogram (Id)
+ or else Is_Generic_Subprogram (Id));
Set_Node24 (Id, V);
end Set_Spec_PPC_List;
===================================================================
@@ -3532,11 +3532,12 @@ package Einfo is
-- the corresponding parameter entities in the spec.
-- Spec_PPC_List (Node24)
+-- Present in entries, and in subprogram and generic subprogram entities.
+-- Points to a list of Precondition and Postcondition pragma nodes for
+-- preconditions and postconditions declared in the spec. The last pragma
+-- encountered is at the head of this list, so it is in reverse order of
+-- textual appearance. Note that this includes precondition/postcondition
+-- pragmas generated to correspond to Pre/Post aspects.
-- Storage_Size_Variable (Node15) [implementation base type only]
-- Present in access types and task type entities. This flag is set
@@ -4951,6 +4952,7 @@ package Einfo is
-- Accept_Address (Elist21)
-- Scope_Depth_Value (Uint22)
-- Protection_Object (Node23) (protected kind)
+ -- Spec_PPC_List (Node24) (for entry only)
-- Default_Expressions_Processed (Flag108)
-- Entry_Accepted (Flag152)
-- Is_AST_Entry (Flag132) (for entry only)
===================================================================
@@ -240,9 +240,7 @@ package body Sem_Prag is
------------------------------
procedure Analyze_PPC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
- Arg1 : constant Node_Id :=
- First (Pragma_Argument_Associations (N));
- Arg2 : constant Node_Id := Next (Arg1);
+ Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N));
begin
-- Install formals and push subprogram spec onto scope stack so that we
@@ -257,13 +255,6 @@ package body Sem_Prag is
Preanalyze_Spec_Expression
(Get_Pragma_Arg (Arg1), Standard_Boolean);
- -- If there is a message argument, analyze it the same way
-
- if Present (Arg2) then
- Preanalyze_Spec_Expression
- (Get_Pragma_Arg (Arg2), Standard_String);
- end if;
-
-- Remove the subprogram from the scope stack now that the pre-analysis
-- of the precondition/postcondition is done.
@@ -1511,8 +1502,7 @@ package body Sem_Prag is
("pragma% cannot be applied to abstract subprogram");
elsif Class_Present (N) then
- Error_Pragma
- ("aspect `%''Class` not implemented yet");
+ null;
else
Error_Pragma
@@ -1520,14 +1510,19 @@ package body Sem_Prag is
end if;
elsif not Nkind_In (PO, N_Subprogram_Declaration,
- N_Generic_Subprogram_Declaration)
+ N_Generic_Subprogram_Declaration,
+ N_Entry_Declaration)
then
Pragma_Misplaced;
end if;
- -- Here if we have subprogram or generic subprogram declaration
+ -- Here if we have [generic] subprogram or entry declaration
- S := Defining_Unit_Name (Specification (PO));
+ if Nkind (PO) = N_Entry_Declaration then
+ S := Defining_Entity (PO);
+ else
+ S := Defining_Unit_Name (Specification (PO));
+ end if;
-- Make sure we do not have the case of a precondition pragma when
-- the Pre'Class aspect is present.
@@ -1583,14 +1578,11 @@ package body Sem_Prag is
end;
end if;
- -- Analyze the pragma unless it appears within a package spec,
- -- which is the case where we delay the analysis of the PPC until
- -- the end of the package declarations (for details, see
- -- Analyze_Package_Specification.Analyze_PPCs).
-
- if not Is_Package_Or_Generic_Package (Scope (S)) then
- Analyze_PPC_In_Decl_Part (N, S);
- end if;
+ -- Note: we do not analye the pragma at this point. Instead we
+ -- delay this analysis until the end of the declarative part in
+ -- which the pragma appears. This implements the required delay
+ -- in this analysis, allowing forward references. The analysis
+ -- happens at the end of Analyze_Declarations.
-- Chain spec PPC pragma to list for subprogram
@@ -1610,6 +1602,15 @@ package body Sem_Prag is
Pragma_Misplaced;
end if;
+ -- Preanalyze message argument if present. Visibility in this
+ -- argument is established at the point of pragma occurrence.
+
+ if Arg_Count = 2 then
+ Check_Optional_Identifier (Arg2, Name_Message);
+ Preanalyze_Spec_Expression
+ (Get_Pragma_Arg (Arg2), Standard_String);
+ end if;
+
-- Record if pragma is enabled
if Check_Enabled (Pname) then
@@ -10823,7 +10824,6 @@ package body Sem_Prag is
Check_At_Least_N_Arguments (1);
Check_At_Most_N_Arguments (2);
Check_Optional_Identifier (Arg1, Name_Check);
-
Check_Precondition_Postcondition (In_Body);
-- If in spec, nothing more to do. If in body, then we convert the
@@ -10833,11 +10833,6 @@ package body Sem_Prag is
-- analyze the condition itself in the proper context.
if In_Body then
- if Arg_Count = 2 then
- Check_Optional_Identifier (Arg3, Name_Message);
- Analyze_And_Resolve (Get_Pragma_Arg (Arg2), Standard_String);
- end if;
-
Rewrite (N,
Make_Pragma (Loc,
Chars => Name_Check,
===================================================================
@@ -8699,18 +8699,22 @@ package body Sem_Ch6 is
-- do this fiddling, for the spec cases, the already preanalyzed
-- parameters are not affected.
+ Set_Analyzed (CP, False);
+
+ -- We also make sure Comes_From_Source is False for the copy
+
+ Set_Comes_From_Source (CP, False);
+
-- For a postcondition pragma within a generic, preserve the pragma
-- for later expansion.
- Set_Analyzed (CP, False);
-
if Nam = Name_Postcondition
and then not Expander_Active
then
return CP;
end if;
- -- Change pragma into corresponding pragma Check
+ -- Change copy of pragma into corresponding pragma Check
Prepend_To (Pragma_Argument_Associations (CP),
Make_Pragma_Argument_Association (Sloc (Prag),
@@ -8761,9 +8765,8 @@ package body Sem_Ch6 is
Prag := Spec_PPC_List (Spec_Id);
while Present (Prag) loop
- if Pragma_Name (Prag) = Name_Precondition
- and then Pragma_Enabled (Prag)
- then
+ if Pragma_Name (Prag) = Name_Precondition then
+
-- For Pre (or Precondition pragma), we simply prepend the
-- pragma to the list of declarations right away so that it
-- will be executed at the start of the procedure. Note that
@@ -8969,7 +8972,6 @@ package body Sem_Ch6 is
Prag := Spec_PPC_List (Spec);
loop
if Pragma_Name (Prag) = Name_Postcondition
- and then Pragma_Enabled (Prag)
and then (not Class or else Class_Present (Prag))
then
if Plist = No_List then
===================================================================
@@ -1742,8 +1742,29 @@ package body Sem_Disp is
Parent_Op : Entity_Id;
-- Traverses the Overridden_Operation chain
+ procedure Store_IS (E : Entity_Id);
+ -- Stores E in Result if not already stored
+
+ --------------
+ -- Store_IS --
+ --------------
+
+ procedure Store_IS (E : Entity_Id) is
+ begin
+ for J in 1 .. N loop
+ if E = Result (J) then
+ return;
+ end if;
+ end loop;
+
+ N := N + 1;
+ Result (N) := E;
+ end Store_IS;
+
+ -- Start of processing for Inherited_Subprograms
+
begin
- if Present (S) then
+ if Present (S) and then Is_Dispatching_Operation (S) then
-- Deal with direct inheritance
@@ -1755,13 +1776,56 @@ package body Sem_Disp is
if Is_Subprogram (Parent_Op)
or else Is_Generic_Subprogram (Parent_Op)
then
- N := N + 1;
- Result (N) := Parent_Op;
+ Store_IS (Parent_Op);
end if;
end loop;
- -- For now don't bother with interfaces, TBD ???
+ -- Now deal with interfaces
+
+ declare
+ Tag_Typ : Entity_Id;
+ Prim : Entity_Id;
+ Elmt : Elmt_Id;
+
+ begin
+ Tag_Typ := Find_Dispatching_Type (S);
+
+ if Is_Concurrent_Type (Tag_Typ) then
+ Tag_Typ := Corresponding_Record_Type (Tag_Typ);
+ end if;
+ -- Search primitive operations of dispatching type
+
+ if Present (Tag_Typ)
+ and then Present (Primitive_Operations (Tag_Typ))
+ then
+ Elmt := First_Elmt (Primitive_Operations (Tag_Typ));
+ while Present (Elmt) loop
+ Prim := Node (Elmt);
+
+ -- The following test eliminates some odd cases in which
+ -- Ekind (Prim) is Void, to be investigated further ???
+
+ if not (Is_Subprogram (Prim)
+ or else
+ Is_Generic_Subprogram (Prim))
+ then
+ null;
+
+ -- For [generic] subprogram, look at interface alias
+
+ elsif Present (Interface_Alias (Prim))
+ and then Alias (Prim) = S
+ then
+ -- We have found a primitive covered by S
+
+ Store_IS (Interface_Alias (Prim));
+ end if;
+
+ Next_Elmt (Elmt);
+ end loop;
+ end if;
+ end;
end if;
return Result (1 .. N);
This patch completes two of the remaining issues in processing the Pre/Post attributes. First inheritance of Pre'Class is properly handled. Second, delay of visibility analysis of Pre/Post aspects is done right for all declarative parts, not just packages. The following test of Pre'Class inheritance is compiled with -gnatld7 -gnatj60 -gnata12: Compiling: test_prepost_ifaces.adb 1. with Prepost_Ifaces.P123; 2. use Prepost_Ifaces; 3. use Prepost_Ifaces.P123; 4. with Prepost_Ifaces.P1; use Prepost_Ifaces.P1; 5. with Prepost_Ifaces.P2; use Prepost_Ifaces.P2; 6. with Prepost_Ifaces.P3; use Prepost_Ifaces.P3; 7. procedure Test_Prepost_Ifaces is 8. X123 : T123 := (null record); 9. X23 : T23 := (null record); 10. begin 11. P1.Dispatch (X123); 12. P2.Dispatch (X123); 13. P3.Dispatch (X123); 14. 15. P2.Dispatch (X23); 16. P3.Dispatch (X23); 17. end Test_Prepost_Ifaces; 17 lines: No errors Compiling: prepost_ifaces.adb 1. package body Prepost_Ifaces is 2. 3. function Faux return Boolean is 4. begin 5. return False; 6. end Faux; 7. 8. function Vrai return Boolean is 9. begin 10. return True; 11. end Vrai; 12. 13. end Prepost_Ifaces; Compiling: prepost_ifaces.ads 1. with Ada.Text_IO; use Ada.Text_IO; 2. with Ada.Assertions; use Ada.Assertions; 3. package Prepost_Ifaces is 4. 5. function Faux return Boolean; 6. function Vrai return Boolean; 7. 8. end Prepost_Ifaces; 13 lines: No errors Compiling: prepost_ifaces-p1.adb 1. with Ada.Exceptions; use Ada.Exceptions; 2. package body Prepost_Ifaces.P1 is 3. 4. procedure Dispatch (X : T1'Class) is 5. begin 6. OK_Pre (X); 7. OK_Post (X); 8. 9. begin 10. Bad_Pre (X); 11. Put_Line ("P1: Bad_Pre: No exception"); 12. exception 13. when E : Assertion_Error => 14. Put_Line ("P1: Bad_Pre: Assertion_Error"); 15. Put_Line (" " & Exception_Message (E)); 16. end; 17. 18. begin 19. Bad_Post (X); 20. Put_Line 21. ("P1: Bad_Post: No exception"); 22. exception 23. when E : Assertion_Error => 24. Put_Line ("P1: Bad_Post: Assertion_Error"); 25. Put_Line (" " & Exception_Message (E)); 26. end; 27. end Dispatch; 28. 29. end Prepost_Ifaces.P1; Compiling: prepost_ifaces-p1.ads 1. package Prepost_Ifaces.P1 is 2. type T1 is abstract tagged null record; 3. procedure OK_Pre (X : T1) is abstract with 4. Pre'Class => Faux; 5. procedure Bad_Pre (X : T1) is abstract with 6. Pre'Class => Faux; 7. procedure OK_Post (X : T1) is abstract with 8. Post'Class => Vrai; 9. procedure Bad_Post (X : T1) is abstract with 10. Post'Class => Vrai; 11. 12. procedure Dispatch (X : T1'Class); 13. end Prepost_Ifaces.P1; 29 lines: No errors Compiling: prepost_ifaces-p123.adb 1. package body Prepost_Ifaces.P123 is 2. 3. overriding procedure OK_Pre (X : T123) is 4. begin 5. null; 6. end OK_Pre; 7. 8. overriding procedure Bad_Pre (X : T123) is 9. begin 10. null; 11. end Bad_Pre; 12. 13. overriding procedure OK_Post (X : T123) is 14. begin 15. null; 16. end OK_Post; 17. 18. overriding procedure Bad_Post (X : T123) is 19. begin 20. null; 21. end Bad_Post; 22. 23. overriding procedure OK_Pre (X : T23) is 24. begin 25. null; 26. end OK_Pre; 27. 28. overriding procedure Bad_Pre (X : T23) is 29. begin 30. null; 31. end Bad_Pre; 32. 33. overriding procedure OK_Post (X : T23) is 34. begin 35. null; 36. end OK_Post; 37. 38. overriding procedure Bad_Post (X : T23) is 39. begin 40. null; 41. end Bad_Post; 42. 43. end Prepost_Ifaces.P123; Compiling: prepost_ifaces-p123.ads 1. with Prepost_Ifaces.P1; use Prepost_Ifaces.P1; 2. with Prepost_Ifaces.P2; use Prepost_Ifaces.P2; 3. with Prepost_Ifaces.P3; use Prepost_Ifaces.P3; 4. package Prepost_Ifaces.P123 is 5. type T123 is new T1 and T2 and T3 6. with null record; 7. 8. overriding procedure OK_Pre (X : T123); | >>> info: "OK_Pre" inherits "Pre'Class" aspect from prepost_ifaces-p1.ads:4 9. -- Inherits Pre => False or False or True 10. 11. overriding procedure Bad_Pre (X : T123); | >>> info: "Bad_Pre" inherits "Pre'Class" aspect from prepost_ifaces-p1.ads:6 12. -- Inherits Pre => False or False or False 13. 14. overriding procedure OK_Post (X : T123); | >>> info: "OK_Post" inherits "Post'Class" aspect from prepost_ifaces-p1.ads:8 15. -- Inherits Post => True and True and True 16. 17. overriding procedure Bad_Post (X : T123); | >>> info: "Bad_Post" inherits "Post'Class" aspect from prepost_ifaces-p1.ads:10 18. -- Inherits Post => True and True and False 19. 20. type T23 is new T2 and T3 with null record; 21. 22. overriding procedure OK_Pre (X : T23); | >>> info: "OK_Pre" inherits "Pre'Class" aspect from prepost_ifaces-p2.ads:4 23. -- Inherits Pre => False or True 24. 25. overriding procedure Bad_Pre (X : T23); | >>> info: "Bad_Pre" inherits "Pre'Class" aspect from prepost_ifaces-p2.ads:6 26. -- Inherits Pre => False or False 27. 28. overriding procedure OK_Post (X : T23); | >>> info: "OK_Post" inherits "Post'Class" aspect from prepost_ifaces-p2.ads:8 29. -- Inherits Post => True and True 30. 31. overriding procedure Bad_Post (X : T23); | >>> info: "Bad_Post" inherits "Post'Class" aspect from prepost_ifaces-p2.ads:10 32. -- Inherits Post => True and False 33. 34. end Prepost_Ifaces.P123; Compiling: prepost_ifaces-p2.adb 1. with Ada.Exceptions; use Ada.Exceptions; 2. package body Prepost_Ifaces.P2 is 3. 4. procedure Dispatch (X : T2'Class) is 5. begin 6. OK_Pre (X); 7. OK_Post (X); 8. 9. begin 10. Bad_Pre (X); 11. Put_Line ("P2: Bad_Pre: No exception"); 12. exception 13. when E : Assertion_Error => 14. Put_Line ("P2: Bad_Pre: Assertion_Error: "); 15. Put_Line (" " & Exception_Message (E)); 16. end; 17. 18. begin 19. Bad_Post (X); 20. Put_Line ("P2: Bad_Post: No exception"); 21. exception 22. when E : Assertion_Error => 23. Put_Line ("P2: Bad_Post: Assertion_Error"); 24. Put_Line (" " & Exception_Message (E)); 25. end; 26. end Dispatch; 27. 28. end Prepost_Ifaces.P2; Compiling: prepost_ifaces-p2.ads 1. package Prepost_Ifaces.P2 is 2. type T2 is interface; 3. procedure OK_Pre (X : T2) is abstract with 4. Pre'Class => Faux; 5. procedure Bad_Pre (X : T2) is abstract with 6. Pre'Class => Faux; 7. procedure OK_Post (X : T2) is abstract with 8. Post'Class => Vrai; 9. procedure Bad_Post (X : T2) is abstract with 10. Post'Class => Vrai; 11. 12. procedure Dispatch (X : T2'Class); 13. end Prepost_Ifaces.P2; 28 lines: No errors Compiling: prepost_ifaces-p3.adb 1. with Ada.Exceptions; use Ada.Exceptions; 2. package body Prepost_Ifaces.P3 is 3. 4. procedure Dispatch (X : T3'Class) is 5. begin 6. OK_Pre (X); 7. OK_Post (X); 8. 9. begin 10. Bad_Pre (X); 11. Put_Line 12. ("P3: Bad_Pre: No exception"); 13. exception 14. when E : Assertion_Error => 15. Put_Line ("P3: Bad_Pre: Assertion_Error"); 16. Put_Line (" " & Exception_Message (E)); 17. end; 18. 19. begin 20. Bad_Post (X); 21. Put_Line 22. ("P3: Bad_Post: No exception"); 23. exception 24. when E : Assertion_Error => 25. Put_Line ("P3: Bad_Post: Assertion_Error"); 26. Put_Line (" " & Exception_Message (E)); 27. end; 28. end Dispatch; 29. 30. end Prepost_Ifaces.P3; Compiling: prepost_ifaces-p3.ads 1. package Prepost_Ifaces.P3 is 2. type T3 is interface; 3. procedure OK_Pre (X : T3) is null with 4. Pre'Class => Vrai; 5. procedure Bad_Pre (X : T3) is null with 6. Pre'Class => Faux; 7. procedure OK_Post (X : T3) is null with 8. Post'Class => Vrai; 9. procedure Bad_Post (X : T3) is null with 10. Post'Class => Faux; 11. 12. procedure Dispatch (X : T3'Class); 13. end Prepost_Ifaces.P3; 30 lines: No errors The output when this program is run is: P1: Bad_Pre: Assertion_Error failed inherited precondition from prepost_ifaces-p1.ads:6 also failed inherited precondition from prepost_ifaces-p2.ads:6 also failed inherited precondition from prepost_ifaces-p3.ads:6 P1: Bad_Post: Assertion_Error failed inherited postcondition from prepost_ifaces-p3.ads:10 P2: Bad_Pre: Assertion_Error: failed inherited precondition from prepost_ifaces-p1.ads:6 also failed inherited precondition from prepost_ifaces-p2.ads:6 also failed inherited precondition from prepost_ifaces-p3.ads:6 P2: Bad_Post: Assertion_Error failed inherited postcondition from prepost_ifaces-p3.ads:10 P3: Bad_Pre: Assertion_Error failed inherited precondition from prepost_ifaces-p1.ads:6 also failed inherited precondition from prepost_ifaces-p2.ads:6 also failed inherited precondition from prepost_ifaces-p3.ads:6 P3: Bad_Post: Assertion_Error failed inherited postcondition from prepost_ifaces-p3.ads:10 P2: Bad_Pre: Assertion_Error: failed inherited precondition from prepost_ifaces-p2.ads:6 also failed inherited precondition from prepost_ifaces-p3.ads:6 P2: Bad_Post: Assertion_Error failed inherited postcondition from prepost_ifaces-p3.ads:10 P3: Bad_Pre: Assertion_Error failed inherited precondition from prepost_ifaces-p2.ads:6 also failed inherited precondition from prepost_ifaces-p3.ads:6 P3: Bad_Post: Assertion_Error failed inherited postcondition from prepost_ifaces-p3.ads:10 the following test shows proper delay of Pre/Post visibility in a declarative part of a subprogram. Compiled with -gnata12 -gnatld7: 1. with Text_IO; use Text_IO; 2. with Ada.Exceptions; 3. use Ada.Exceptions; 4. procedure Prepostdelay is 5. procedure p1 (X : Integer) with 6. Pre => ident (X) = 13; 7. 8. function ident (X : Integer) return Integer; 9. 10. procedure p1 (X : Integer) is 11. begin null; end; 12. 13. function ident (X : Integer) return Integer 14. is begin return X; end; 15. 16. begin 17. p1 (13); 18. Put_Line ("no exception for p1 (13)"); 19. begin 20. p1 (12); 21. exception 22. when E : others => 23. Put_Line ("exception for p1 (12)"); 24. Put_Line (" " & Exception_Message (E)); 25. end; 26. end Prepostdelay; The output is: no exception for p1 (13) exception for p1 (12) failed precondition from prepostdelay.adb:6 The following test shows that the visibilty does not extend into the private part, compiled again with -gnata12 -gnatld7 1. package Prepostdelay2 is 2. procedure p1 (X : Integer) with 3. Pre => ident (X) = 13; 4. 5. function ident (X : Integer) return Integer; 6. 7. procedure p2 (X : Integer) with 8. Pre => ident2 (X); | >>> "ident2" is undefined >>> possible misspelling of "ident" 9. 10. private 11. function ident2 (X : Integer) return Integer; 12. end; Tested on x86_64-pc-linux-gnu, committed on trunk 2010-10-18 Robert Dewar <dewar@adacore.com> * einfo.ads, einfo.adb (Spec_PPC_List): Is now present in Entries * sem_ch3.adb (Analyze_Declarations): Add processing for delaying visibility analysis of precondition and postcondition pragmas (and Pre/Post aspects). * sem_ch6.adb (Process_PPCs): Add handling of inherited Pre'Class aspects. * sem_ch7.adb (Analyze_Package_Specification): Remove special handling of pre/post conditions (no longer needed). * sem_disp.adb (Inherit_Subprograms): Deal with interface case. * sem_prag.adb (Analyze_PPC_In_Decl_Part): Remove analysis of message argument, since this is now done in the main processing for pre/postcondition pragmas when they are first seen. (Chain_PPC): Pre'Class and Post'Class now handled properly (Chain_PPC): Handle Pre/Post aspects for entries (Check_Precondition_Postcondition): Handle entry declaration case (Check_Precondition_Postcondition): Handle delay of visibility analysis (Check_Precondition_Postcondition): Preanalyze message argument if present.