Previously, invariants were applied for IN OUT parameters and return
values on all subprograms. This is wrong, they should only be applied
for private subprograms. In the following test program, only the
exception marked OK should be raised, not the other two (before all
three exceptions were raised).
1. with PrivInv; use PrivInv;
2. with Text_IO; use Text_IO;
3. procedure PrivInvM is
4. X : T := Create;
5. begin
6. Pub (X);
7. exception
8. when others =>
9. Put_Line ("OK, exception raised for call to Pub");
10. end;
1. package PrivInv is
2. type T is private with Invariant => Valid (T);
3. function Valid (X : T) return Boolean;
4. procedure Pub (X : in out T);
5. function Create return T;
6. private
7. type T is record
8. B : Boolean;
9. end record;
10. function Valid (X : T) return Boolean is (X.B);
11. procedure Priv (X : in out T);
12. function Create return T is (T'(B => True));
13. end PrivInv;
1. with Text_IO; use Text_IO;
2. package body PrivInv is
3. procedure Bod (X : in out T);
4. procedure Bod (X : in out T) is
5. begin
6. X.B := False;
7. end;
8.
9. procedure Pub (X : in out T) is
10. begin
11. begin
12. Bod (X);
13. exception
14. when others =>
15. Put_Line ("ERROR: Exception raised for call to Bod");
16. end;
17.
18. begin
19. Priv (X);
20. exception
21. when others =>
22. Put_Line ("ERROR: Exception raised for call to Priv");
23. end;
24.
25. X.B := False;
26. end;
27.
28. procedure Priv (X : in out T) is
29. begin
30. X.B := False;
31. end;
32. end PrivInv;
The new correct output is the single line:
OK, exception raised for call to Pub
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-11-21 Robert Dewar <de...@adacore.com>
* sem_ch6.adb (Is_Public_Subprogram_For): New procedure
(Process_PPCs): Invariants only apply to public subprograms.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 181556)
+++ sem_ch6.adb (working copy)
@@ -8536,19 +8536,19 @@
and then In_Private_Part (Current_Scope)
then
Priv_Decls :=
- Private_Declarations (
- Specification (Unit_Declaration_Node (Current_Scope)));
+ Private_Declarations
+ (Specification (Unit_Declaration_Node (Current_Scope)));
return In_Package_Body (Current_Scope)
or else
(Is_List_Member (Decl)
- and then List_Containing (Decl) = Priv_Decls)
+ and then List_Containing (Decl) = Priv_Decls)
or else (Nkind (Parent (Decl)) = N_Package_Specification
- and then not
- Is_Compilation_Unit
- (Defining_Entity (Parent (Decl)))
- and then List_Containing (Parent (Parent (Decl)))
- = Priv_Decls);
+ and then not
+ Is_Compilation_Unit
+ (Defining_Entity (Parent (Decl)))
+ and then List_Containing (Parent (Parent (Decl))) =
+ Priv_Decls);
else
return False;
end if;
@@ -9562,6 +9562,15 @@
-- or IN OUT parameters of the subprogram, or (for a function) if the
-- return value has an invariant.
+ function Is_Public_Subprogram_For (T : Entity_Id) return Boolean;
+ -- T is the entity for a private type for which invariants are defined.
+ -- This function returns True if the procedure corresponding to the
+ -- value of Designator is a public procedure from the point of view of
+ -- this type (i.e. its spec is in the visible part of the package that
+ -- contains the declaration of the private type). A True value means
+ -- that an invariant check is required (for an IN OUT parameter, or
+ -- the returned value of a function.
+
--------------
-- Grab_PPC --
--------------
@@ -9689,6 +9698,45 @@
return False;
end Invariants_Or_Predicates_Present;
+ ------------------------------
+ -- Is_Public_Subprogram_For --
+ ------------------------------
+
+ -- The type T is a private type, its declaration is therefore in
+ -- the list of public declarations of some package. The test for a
+ -- public subprogram is that its declaration is in this same list
+ -- of declarations for the same package (note that all the public
+ -- declarations are in one list, and all the private declarations
+ -- in another, so this deals with the public/private distinction).
+
+ function Is_Public_Subprogram_For (T : Entity_Id) return Boolean is
+ DD : constant Node_Id := Unit_Declaration_Node (Designator);
+ -- The subprogram declaration for the subprogram in question
+
+ TL : constant List_Id :=
+ Visible_Declarations
+ (Specification (Unit_Declaration_Node (Scope (T))));
+ -- The list of declarations containing the private declaration of
+ -- the type. We know it is a private type, so we know its scope is
+ -- the package in question, and we know it must be in the visible
+ -- declarations of this package.
+
+ begin
+ -- If the subprogram declaration is not a list member, it must be
+ -- an Init_Proc, in which case we want to consider it to be a
+ -- public subprogram, since we do get initializations to deal with.
+
+ if not Is_List_Member (DD) then
+ return True;
+
+ -- Otherwise we test whether the subprogram is declared in the
+ -- visible declarations of the package containing the type.
+
+ else
+ return TL = List_Containing (DD);
+ end if;
+ end Is_Public_Subprogram_For;
+
-- Start of processing for Process_PPCs
begin
@@ -9985,10 +10033,13 @@
Parameter_Type => New_Occurrence_Of (Ftyp, Loc),
Defining_Identifier => Rent));
- -- Add invariant call if returning type with invariants
+ -- Add invariant call if returning type with invariants and
+ -- this is a public function, i.e. a function declared in the
+ -- visible part of the package defining the private type.
if Has_Invariants (Etype (Rent))
and then Present (Invariant_Procedure (Etype (Rent)))
+ and then Is_Public_Subprogram_For (Etype (Rent))
then
Append_To (Plist,
Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
@@ -10017,6 +10068,7 @@
if Has_Invariants (Ftype)
and then Present (Invariant_Procedure (Ftype))
+ and then Is_Public_Subprogram_For (Ftype)
then
Append_To (Plist,
Make_Invariant_Call
