This patch fixes some problems involving the use of Type_Invariant'Class on
the ancestor of a derived type that also implements an interface.
The following command:
gnatmake -q -gnat12 -gnata test_invariant
test_invariant
must yield:
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE :
failed inherited invariant from invariants.ads:5
---
with Carrier.Next; use Carrier.Next;
procedure Test_Invariant is
THing : NT;
begin
HeHe (Thing);
end;
---
package Carrier is
type PT is tagged private;
function Invariant(X: PT) return Boolean;
procedure Do_AandB(X: out PT);
private
type PT is tagged record A,B: Integer; end record;
procedure Do_A(X: out PT; V: Integer);
procedure Do_B(X: out PT; V: Integer);
end Carrier;
---
Package body Carrier is
procedure Do_AandB(X: out PT) is
begin Do_A(X,42); Do_B(X,42); end Do_AandB;
function Invariant(X: PT) return Boolean is
begin return X.A=X.B; end Invariant;
procedure Do_A(X: out PT; V: Integer) is begin X.A := V; end Do_A;
procedure Do_B(X: out PT; V: Integer) is begin X.B := V; end do_B;
end Carrier;
---
with Carrier; use Carrier;
Package Invariants is
type T is new PT with private
with Type_Invariant'class => Invariant(PT(T));
-- type T introduced by my ignorance about visibility rules inside
-- of type invariants; maybe could be on Carrier.PT already, or
-- only on I below. The conclusion applies in all cases and
-- combinations.
private
type T is new PT with null record;
end Invariants;
---
package Interf is
type I is Interface
-- if you want:
with Type_Invariant'Class => Invariant(I);
-- maybe with the same "carrier detour" because of visibility?
function Invariant(X: I) return boolean is abstract;
procedure HeHe(X: out I) is abstract;
end Interf;
---
with Invariants; with Interf;
package Carrier.Next is
type NT is new Invariants.T and Interf.I with null record;
procedure HeHe(X: out NT); -- newly added op; definitely needs
-- to check the invariant, or else....
end Carrier.Next;
---
package body Carrier.Next is
procedure HeHe(X: out NT) is
begin
DO_A(PT(X),666); -- BREAKS THE INVARIANT
end Hehe; -- HeHe BETTER RAISE ASSERTION_ERROR
end Carrier.Next;
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-10-01 Ed Schonberg <schonb...@adacore.com>
* aspects.ads: Type_Invariant'class is a valid aspect.
* sem_ch6.adb (Is_Public_Subprogram_For): with the exception of
initialization procedures, subprograms that do not come from
source are not public for the purpose of invariant checking.
* sem_ch13.adb (Build_Invariant_Procedure): Handle properly the
case of a non-private type in a package without a private part,
when the type inherits invariants from its ancestor.
Index: aspects.ads
===================================================================
--- aspects.ads (revision 191888)
+++ aspects.ads (working copy)
@@ -191,11 +191,12 @@
-- The following array indicates aspects that accept 'Class
Class_Aspect_OK : constant array (Aspect_Id) of Boolean :=
- (Aspect_Invariant => True,
- Aspect_Pre => True,
- Aspect_Predicate => True,
- Aspect_Post => True,
- others => False);
+ (Aspect_Invariant => True,
+ Aspect_Pre => True,
+ Aspect_Predicate => True,
+ Aspect_Post => True,
+ Aspect_Type_Invariant => True,
+ others => False);
-- The following array indicates aspects that a subtype inherits from
-- its base type. True means that the subtype inherits the aspect from
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 191888)
+++ sem_ch6.adb (working copy)
@@ -11342,10 +11342,16 @@
-- 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.
+ -- Other internally generated subprograms are not public.
- if not Is_List_Member (DD) then
+ if not Is_List_Member (DD)
+ and then Is_Init_Proc (DD)
+ then
return True;
+ elsif not Comes_From_Source (DD) then
+ return False;
+
-- Otherwise we test whether the subprogram is declared in the
-- visible declarations of the package containing the type.
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 191900)
+++ sem_ch13.adb (working copy)
@@ -5188,9 +5188,6 @@
Statements => Stmts));
-- Insert procedure declaration and spec at the appropriate points.
- -- Skip this if there are no private declarations (that's an error
- -- that will be diagnosed elsewhere, and there is no point in having
- -- an invariant procedure set if the full declaration is missing).
if Present (Private_Decls) then
@@ -5214,6 +5211,19 @@
if In_Private_Part (Current_Scope) then
Analyze (PBody);
end if;
+
+ -- If there are no private declarations this may be an error that
+ -- will be diagnosed elsewhere. However, if this is a non-private
+ -- type that inherits invariants, it needs no completion and there
+ -- may be no private part. In this case insert invariant procedure
+ -- at end of current declarative list, and analyze at once, given
+ -- that the type is about to be frozen.
+
+ elsif not Is_Private_Type (Typ) then
+ Append_To (Visible_Decls, PDecl);
+ Append_To (Visible_Decls, PBody);
+ Analyze (PDecl);
+ Analyze (PBody);
end if;
end if;
end Build_Invariant_Procedure;
