[Ada] Handling of Invariant aspect on type completions
Arnaud Charlet
charlet@adacore.com
Fri Oct 5 14:32:00 GMT 2012
This patch fixes the handling of type invariants when they are specified on
the completion of a private type, and when public expression functions return
a type with invariants.
Running the following:
gnatmake -q -gnat12a main
main
must yield:
OK
---
with Ada.Assertions; use Ada.Assertions;
with Text_IO; use Text_IO;
with R; use R;
procedure Main is
X : T;
begin
X := Zero;
Put_Line ("Invariant violated");
exception
when Assertion_Error => Put_Line ("OK");
end Main;
---
package R is
type T is private;;
function Non_Null (X : T) return Boolean;
function Zero return T;
private
type T is new Integer with Type_Invariant => T /= 0;
function Non_Null (X : T) return Boolean is (X /= 0);
function Zero return T is (0);
end R;
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-10-05 Ed Schonberg <schonberg@adacore.com>
* einfo.adb (Set_Invariant_Procedure, Set_Predicate_Function):
chain properly subprograms on Subprograms_For_Type list.
* sem_ch13.ads; (Build_Invariant_Procedure_Declaration): new
procedure, to create declaration for invariant procedure
independently of the construction of the body, so that it can
be called within expression functions.
* sem_ch13.adb (Build_Invariant_Procedure): code cleanup. The
declaration may already have been generated at the point an
explicit invariant aspect is encountered.
* sem_prag.adb; (Analyze_Pragma, case Invariant): create declaration
for invariant procedure.
* sem_ch7.adb (Analyze_Package_Specification): clean up call to
build invariant procedure.
(Preserve_Full_Attributes): propagate information about invariants
if they appear on a completion,
-------------- next part --------------
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 192066)
+++ sem_ch7.adb (working copy)
@@ -28,6 +28,7 @@
-- handling of private and full declarations, and the construction of dispatch
-- tables for tagged types.
+with Aspects; use Aspects;
with Atree; use Atree;
with Debug; use Debug;
with Einfo; use Einfo;
@@ -1387,7 +1388,21 @@
and then Nkind (Parent (E)) = N_Full_Type_Declaration
and then Has_Aspects (Parent (E))
then
- Build_Invariant_Procedure (E, N);
+ declare
+ ASN : Node_Id;
+ begin
+ ASN := First (Aspect_Specifications (Parent (E)));
+ while Present (ASN) loop
+ if Chars (Identifier (ASN)) = Name_Invariant
+ or else Chars (Identifier (ASN)) = Name_Type_Invariant
+ then
+ Build_Invariant_Procedure (E, N);
+ exit;
+ end if;
+
+ Next (ASN);
+ end loop;
+ end;
end if;
Next_Entity (E);
@@ -2143,6 +2158,14 @@
Set_Freeze_Node (Priv, Freeze_Node (Full));
+ -- Propagate information of type invariants, which may be specified
+ -- for the full view.
+
+ if Has_Invariants (Full) and not Has_Invariants (Priv) then
+ Set_Has_Invariants (Priv);
+ Set_Subprograms_For_Type (Priv, Subprograms_For_Type (Full));
+ end if;
+
if Is_Tagged_Type (Priv)
and then Is_Tagged_Type (Full)
and then not Error_Posted (Full)
Index: einfo.adb
===================================================================
--- einfo.adb (revision 192066)
+++ einfo.adb (working copy)
@@ -7113,6 +7113,7 @@
S := Subprograms_For_Type (Id);
Set_Subprograms_For_Type (Id, V);
+ Set_Subprograms_For_Type (V, S);
while Present (S) loop
if Has_Invariants (S) then
@@ -7121,8 +7122,6 @@
S := Subprograms_For_Type (S);
end if;
end loop;
-
- Set_Subprograms_For_Type (Id, V);
end Set_Invariant_Procedure;
----------------------------
@@ -7137,6 +7136,7 @@
S := Subprograms_For_Type (Id);
Set_Subprograms_For_Type (Id, V);
+ Set_Subprograms_For_Type (V, S);
while Present (S) loop
if Has_Predicates (S) then
@@ -7145,8 +7145,6 @@
S := Subprograms_For_Type (S);
end if;
end loop;
-
- Set_Subprograms_For_Type (Id, V);
end Set_Predicate_Function;
-----------------
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 192124)
+++ sem_prag.adb (working copy)
@@ -10329,6 +10329,7 @@
when Pragma_Invariant => Invariant : declare
Type_Id : Node_Id;
Typ : Entity_Id;
+ PDecl : Node_Id;
Discard : Boolean;
pragma Unreferenced (Discard);
@@ -10380,8 +10381,13 @@
-- Note that the type has at least one invariant, and also that
-- it has inheritable invariants if we have Invariant'Class.
+ -- Build the corresponding invariant procedure declaration, so
+ -- that calls to it can be generated before the body is built
+ -- (for example wihin an expression function).
- Set_Has_Invariants (Typ);
+ PDecl := Build_Invariant_Procedure_Declaration (Typ);
+ Insert_After (N, PDecl);
+ Analyze (PDecl);
if Class_Present (N) then
Set_Has_Inheritable_Invariants (Typ);
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 192066)
+++ sem_ch13.adb (working copy)
@@ -4902,6 +4902,48 @@
end if;
end Analyze_Record_Representation_Clause;
+ -------------------------------------------
+ -- Build_Invariant_Procedure_Declaration --
+ -------------------------------------------
+
+ function Build_Invariant_Procedure_Declaration
+ (Typ : Entity_Id) return Node_Id
+ is
+ Loc : constant Source_Ptr := Sloc (Typ);
+ Object_Entity : constant Entity_Id :=
+ Make_Defining_Identifier (Loc, New_Internal_Name ('I'));
+ Spec : Node_Id;
+ SId : Entity_Id;
+
+ begin
+ Set_Etype (Object_Entity, Typ);
+
+ -- Check for duplicate definiations.
+
+ if Has_Invariants (Typ)
+ and then Present (Invariant_Procedure (Typ))
+ then
+ return Empty;
+ end if;
+
+ SId := Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Typ), "Invariant"));
+ Set_Has_Invariants (SId);
+ Set_Has_Invariants (Typ);
+ Set_Ekind (SId, E_Procedure);
+ Set_Invariant_Procedure (Typ, SId);
+
+ Spec :=
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => SId,
+ Parameter_Specifications => New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => Object_Entity,
+ Parameter_Type => New_Occurrence_Of (Typ, Loc))));
+
+ return Make_Subprogram_Declaration (Loc, Specification => Spec);
+ end Build_Invariant_Procedure_Declaration;
+
-------------------------------
-- Build_Invariant_Procedure --
-------------------------------
@@ -4936,12 +4978,11 @@
-- "inherited" to the exception message and generating an informational
-- message about the inheritance of an invariant.
- Object_Name : constant Name_Id := New_Internal_Name ('I');
+ Object_Name : Name_Id;
-- Name for argument of invariant procedure
- Object_Entity : constant Node_Id :=
- Make_Defining_Identifier (Loc, Object_Name);
- -- The procedure declaration entity for the argument
+ Object_Entity : Node_Id;
+ -- The entity of the formal for the procedure
--------------------
-- Add_Invariants --
@@ -5140,8 +5181,30 @@
Stmts := No_List;
PDecl := Empty;
PBody := Empty;
- Set_Etype (Object_Entity, Typ);
+ SId := Empty;
+ -- If the aspect specification exists for some view of the type, the
+ -- declaration for the procedure has been created.
+
+ if Has_Invariants (Typ) then
+ SId := Invariant_Procedure (Typ);
+ end if;
+
+ if Present (SId) then
+ PDecl := Unit_Declaration_Node (SId);
+
+ else
+ PDecl := Build_Invariant_Procedure_Declaration (Typ);
+ end if;
+
+ -- Recover formal of procedure, for use in the calls to invariant
+ -- functions (including inherited ones).
+
+ Object_Entity :=
+ Defining_Identifier
+ (First (Parameter_Specifications (Specification (PDecl))));
+ Object_Name := Chars (Object_Entity);
+
-- Add invariants for the current type
Add_Invariants (Typ, Inherit => False);
@@ -5174,39 +5237,8 @@
if Stmts /= No_List then
- -- Build procedure declaration
+ Spec := Copy_Separate_Tree (Specification (PDecl));
- SId :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Typ), "Invariant"));
- Set_Has_Invariants (SId);
- Set_Invariant_Procedure (Typ, SId);
-
- Spec :=
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => SId,
- Parameter_Specifications => New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier => Object_Entity,
- Parameter_Type => New_Occurrence_Of (Typ, Loc))));
-
- PDecl := Make_Subprogram_Declaration (Loc, Specification => Spec);
-
- -- Build procedure body
-
- SId :=
- Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Typ), "Invariant"));
-
- Spec :=
- Make_Procedure_Specification (Loc,
- Defining_Unit_Name => SId,
- Parameter_Specifications => New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier (Loc, Object_Name),
- Parameter_Type => New_Occurrence_Of (Typ, Loc))));
-
PBody :=
Make_Subprogram_Body (Loc,
Specification => Spec,
@@ -5216,14 +5248,18 @@
Statements => Stmts));
-- Insert procedure declaration and spec at the appropriate points.
+ -- If declaration is already analyzed, it was processed by the
+ -- generated pragma.
if Present (Private_Decls) then
-- The spec goes at the end of visible declarations, but they have
-- already been analyzed, so we need to explicitly do the analyze.
- Append_To (Visible_Decls, PDecl);
- Analyze (PDecl);
+ if not Analyzed (PDecl) then
+ Append_To (Visible_Decls, PDecl);
+ Analyze (PDecl);
+ end if;
-- The body goes at the end of the private declarations, which we
-- have not analyzed yet, so we do not need to perform an explicit
@@ -5523,6 +5559,7 @@
Make_Defining_Identifier (Loc,
Chars => New_External_Name (Chars (Typ), "Predicate"));
Set_Has_Predicates (SId);
+ Set_Ekind (SId, E_Function);
Set_Predicate_Function (Typ, SId);
-- The predicate function is shared between views of a type.
Index: sem_ch13.ads
===================================================================
--- sem_ch13.ads (revision 192066)
+++ sem_ch13.ads (working copy)
@@ -46,6 +46,14 @@
-- order is specified and there is at least one component clause. Adjusts
-- component positions according to either Ada 95 or Ada 2005 (AI-133).
+ function Build_Invariant_Procedure_Declaration
+ (Typ : Entity_Id) return Node_Id;
+ -- If a type declaration has a specified invariant aspect, build the
+ -- declaration for the procedure at once, so that calls to it can be
+ -- generated before the body of the invariant procedure is built. This
+ -- is needed in the presence of public expression functions that return
+ -- the type in question.
+
procedure Build_Invariant_Procedure (Typ : Entity_Id; N : Node_Id);
-- Typ is a private type with invariants (indicated by Has_Invariants being
-- set for Typ, indicating the presence of pragma Invariant entries on the
More information about the Gcc-patches
mailing list