This implements two new pragmas, whose names, syntax, and semantics
match the corresponding aspects Type_Invariant and Type_Invariant'Class
as closely as possible. For Type_Invariant'Class the pragma is named
Type_Invariant_Class, since the attribute form of the name is not legal
for a pragma name.
The following test
1. with Ada.Text_IO; use Ada.Text_IO;
2. with Ada.Assertions; use Ada.Assertions;
3. with Ada.Exceptions; use Ada.Exceptions;
4. procedure PSimpleinv is
5. package X is
6. type R is private;
7. pragma Type_Invariant (R, Testr (R));
8. function Testr (X : R) return Boolean;
9. function Gen (X : Integer) return R;
10. procedure Make (X : out R);
11.
12. type T1 is tagged private;
13. pragma Type_Invariant (T1, Testt1 (T1));
14. type T2 is new T1 with private;
15. function Testt1 (X : T1) return Boolean;
16. function Maket2 return T2;
17.
18. private
19. type R is record
20. Field : Integer := 4;
21. end record;
22.
23. type T1 is tagged record
24. Field : Integer := 4;
25. end record;
26.
27. type T2 is new T1 with record
28. Field2 : Integer := 4;
29. end record;
30. end X;
31.
32. package body X is
33. function Testr (X : R) return Boolean is
34. begin
35. return X.Field mod 2 = 1;
36. end Testr;
37.
38. function Gen (X : Integer) return R is
39. begin
40. return (Field => X);
41. end Gen;
42.
43. procedure Make (X : out R) is
44. begin
45. X := (Field => 4);
46. end Make;
47.
48. function Testt1 (X : T1) return Boolean is
49. begin
50. return X.Field mod 2 = 1;
51. end Testt1;
52.
53. function Maket2 return T2 is
54. begin
55. return (Field => 4, Field2 => 3);
56. end Maket2;
57.
58. -- No exception, private initialization
59.
60. VPrivate : R := (Field => 6);
61. end X;
62.
63. begin
64. -- No exception, OK initialization
65.
66. begin
67. declare
68. V1 : X.R := X.Gen (5);
69. begin
70. null;
71. end;
72. Put_Line ("V1: no exception");
73. end;
74.
75. -- Bad result from public function
76.
77. begin
78. declare
79. V2 : X.R := X.Gen (4);
80. begin
81. null;
82. end;
83. Put_Line ("V2: no exception");
84. exception
85. when E : Assertion_Error =>
86. Put_Line ("V2: " & Exception_Message (E));
87. end;
88.
89. -- Bad default initialization
90.
91. begin
92. declare
93. V3 : X.R;
94. begin
95. null;
96. end;
97. Put_Line ("V3: no exception");
98. exception
99. when E : Assertion_Error =>
100. Put_Line ("V3: " & Exception_Message (E));
101. end;
102.
103. -- Bad OUT parameter
104.
105. begin
106. declare
107. V4 : X.R := X.Gen (5);
108. begin
109. X.Make (V4);
110. end;
111. Put_Line ("V4: no exception");
112. exception
113. when E : Assertion_Error =>
114. Put_Line ("V4: " & Exception_Message (E));
115. end;
116.
117. -- Bad conversion
118.
119. begin
120. declare
121. TT : X.T2 := X.Maket2;
122. V5 : X.T1 := X.T1 (TT);
123. begin
124. null;
125. end;
126. Put_Line ("V5: no exception");
127. exception
128. when E : Assertion_Error =>
129. Put_Line ("V5: " & Exception_Message (E));
130. end;
131. end PSimpleinv;
compiled with -gnata12 -gnatw.l, outputs:
V1: no exception
V2: failed invariant from psimpleinv.adb:7
V3: failed invariant from psimpleinv.adb:7
V4: failed invariant from psimpleinv.adb:7
V5: failed invariant from psimpleinv.adb:13
The following test:
1. with Ada.Text_IO; use Ada.Text_IO;
2. with Ada.Assertions; use Ada.Assertions;
3. with Ada.Exceptions; use Ada.Exceptions;
4. procedure PInheritinv is
5. package X is
6.
7. type T1 is tagged private;
8. pragma Type_Invariant_Class (T1, Testt1 (T1));
9.
10. function Testt1 (X : T1) return Boolean;
11. function Maket1 return T1;
12.
13. type T2 is new T1 with private;
|
>>> info: "T2" inherits "Invariant'Class" aspect from line 8
14.
15. function Maket2 return T2;
16. function Testt1 (X : T2) return Boolean;
17. function Maket1 return T2;
18.
19. private
20. type T1 is tagged record
21. Field1 : Integer := 4;
22. end record;
23.
24. type T2 is new T1 with record
25. Field2 : Integer := 4;
26. end record;
27. end X;
28.
29. package body X is
30.
31. function Testt1 (X : T1) return Boolean is
32. begin
33. return X.Field1 mod 2 = 1;
34. end Testt1;
35.
36. function Testt1 (X : T2) return Boolean is
37. begin
38. return X.Field1 mod 2 = 0;
39. end Testt1;
40.
41. function Maket1 return T1 is
42. begin
43. return (Field1 => 4);
44. end Maket1;
45.
46. function Maket1 return T2 is
47. begin
48. return (Field1 => 4, Field2 => 3);
49. end Maket1;
50.
51. function Maket2 return T2 is
52. begin
53. return (Field1 => 5, Field2 => 3);
54. end Maket2;
55. end X;
56.
57. begin
58. -- Bad value from Maket1
59.
60. begin
61. declare
62. V1 : X.T1 := X.Maket1;
63. begin
64. null;
65. end;
66. Put_Line ("V1: no exception");
67. exception
68. when E : Assertion_Error =>
69. Put_Line ("V1: " & Exception_Message (E));
70. end;
71.
72. -- Bad value from Maket2
73. -- (tested with overridden testt1)
74.
75. begin
76. declare
77. V2 : X.T2 := X.Maket2;
78. begin
79. null;
80. end;
81. Put_Line ("V2: no exception");
82. exception
83. when E : Assertion_Error =>
84. Put_Line ("V2: " & Exception_Message (E));
85. end;
86.
87. -- OK value from overridden Maket1
88. -- (tested with overridden testt1)
89.
90. begin
91. declare
92. V3 : X.T2 := X.Maket1;
93. begin
94. null;
95. end;
96. Put_Line ("V3: no exception");
97. exception
98. when E : Assertion_Error =>
99. Put_Line ("V3: " & Exception_Message (E));
100. end;
101.
102. end PInheritinv;
compiled with -gnata12 -gnatw.l, outputs:
V1: failed invariant from pinheritinv.adb:8
V2: failed invariant from pinheritinv.adb:8
V3: no exception
Tested on x86_64-pc-linux-gnu, committed on trunk
2013-10-14 Robert Dewar <de...@adacore.com>
* exp_prag.adb (Expand_Pragma_Check): Generate proper string
for invariant
* gnat_rm.texi: Add documentation for pragmas
Type_Invariant[_Class]
* par-prag.adb: Add entries for pragmas Type_Invariant[_Class]
* sem_ch13.adb: Minor reformatting
* sem_prag.adb: Implement pragmas Type_Invariant[_Class]
* snames.ads-tmpl: Add entries for pragmas Type_Invariant[_Class]
Index: exp_prag.adb
===================================================================
--- exp_prag.adb (revision 203521)
+++ exp_prag.adb (working copy)
@@ -311,6 +311,10 @@
-- at" is omitted for name = Assertion, since it is redundant, given
-- that the name of the exception is Assert_Failure.)
+ -- Also, instead of "XXX failed at", we generate slightly
+ -- different messages for some of the contract assertions (see
+ -- code below for details).
+
-- An alternative expansion is used when the No_Exception_Propagation
-- restriction is active and there is a local Assert_Failure handler.
-- This is not a common combination of circumstances, but it occurs in
@@ -400,6 +404,15 @@
Insert_Str_In_Name_Buffer ("failed ", 1);
Add_Str_To_Name_Buffer (" from ");
+ -- For special case of Invariant, the string is "failed
+ -- invariant from yy", to be consistent with the string that is
+ -- generated for the aspect case (the code later on checks for
+ -- this specific string to modify it in some cases, so this is
+ -- functionally important).
+
+ elsif Nam = Name_Invariant then
+ Add_Str_To_Name_Buffer ("failed invariant from ");
+
-- For all other checks, the string is "xxx failed at yyy"
-- where xxx is the check name with current source file casing.
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi (revision 203521)
+++ gnat_rm.texi (working copy)
@@ -253,6 +253,8 @@
* Pragma Thread_Local_Storage::
* Pragma Time_Slice::
* Pragma Title::
+* Pragma Type_Invariant::
+* Pragma Type_Invariant_Class::
* Pragma Unchecked_Union::
* Pragma Unimplemented_Unit::
* Pragma Universal_Aliasing ::
@@ -1073,6 +1075,8 @@
* Pragma Thread_Local_Storage::
* Pragma Time_Slice::
* Pragma Title::
+* Pragma Type_Invariant::
+* Pragma Type_Invariant_Class::
* Pragma Unchecked_Union::
* Pragma Unimplemented_Unit::
* Pragma Universal_Aliasing ::
@@ -5367,6 +5371,21 @@
Dynamic_Predicate => F(Q) or G(Q);
@end smallexample
+Note that there is are no pragmas @code{Dynamic_Predicate}
+or @code{Static_Predicate}. That is
+because these pragmas would affect legality and semantics of
+the program and thus do not have a neutral effect if ignored.
+The motivation behind providing pragmas equivalent to
+corresponding aspects is to allow a program to be written
+using the pragmas, and then compiled with a compiler that
+will ignore the pragmas. That doesn't work in the case of
+static and dynamic predicates, since if the corresponding
+pragmas are ignored, then the behavior of the program is
+fundamentally changed (for example a membership test
+@code{A in B} would not take into account a predicate
+defined for subtype B). When following this approach, the
+use of predicates should be avoided.
+
@node Pragma Preelaborable_Initialization
@unnumberedsec Pragma Preelaborable_Initialization
@findex Preelaborable_Initialization
@@ -6786,6 +6805,56 @@
notation is used, and named and positional notation can be mixed
following the normal rules for procedure calls in Ada.
+@node Pragma Type_Invariant
+@unnumberedsec Pragma Type_Invariant
+@findex Invariant
+@findex Type_Invariant pragma
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Type_Invariant
+ ([Entity =>] type_LOCAL_NAME,
+ [Check =>] EXPRESSION);
+@end smallexample
+
+@noindent
+The @code{Type_Invariant} pragma is intended to be an exact
+replacement for the language-defined @code{Type_Invariant}
+aspect, and shares its restrictions and semantics. It differs
+from the language defined @code{Invariant} pragma in that it
+does not permit a string parameter, and it is
+controlled by the assertion identifier @code{Type_Invariant}
+rather than @code{Invariant}.
+
+@node Pragma Type_Invariant_Class
+@unnumberedsec Pragma Type_Invariant_Class
+@findex Invariant
+@findex Type_Invariant_Class pragma
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma Type_Invariant_Class
+ ([Entity =>] type_LOCAL_NAME,
+ [Check =>] EXPRESSION);
+@end smallexample
+
+@noindent
+The @code{Type_Invariant_Class} pragma is intended to be an exact
+replacement for the language-defined @code{Type_Invariant'Class}
+aspect, and shares its restrictions and semantics.
+
+Note: This pragma is called @code{Type_Invariant_Class} rather than
+@code{Type_Invariant'Class} because the latter would not be strictly
+conforming to the allowed syntax for pragmas. The motivation
+for providing pragmas equivalent to the aspects is to allow a program
+to be written using the pragmas, and then compiled if necessary
+using an Ada compiler that does not recognize the pragmas or
+aspects, but is prepared to ignore the pragmas. The assertion
+policy that controls this pragma is @code{Type_Invariant'Class},
+not @code{Type_Invariant_Class}.
+
@node Pragma Unchecked_Union
@unnumberedsec Pragma Unchecked_Union
@cindex Unions in C
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 203523)
+++ sem_prag.adb (working copy)
@@ -846,7 +846,7 @@
if Is_Input then
if (Ekind (Item_Id) = E_Out_Parameter
- and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
+ and then not Is_Unconstrained_Or_Tagged_Item (Item_Id))
or else
(Global_Seen and then not Appears_In (Subp_Inputs, Item_Id))
then
@@ -11772,7 +11772,6 @@
Name_Link_Name));
Check_At_Least_N_Arguments (2);
-
Check_At_Most_N_Arguments (4);
Process_Convention (C, Def_Id);
@@ -13716,7 +13715,7 @@
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (2);
- Check_At_Most_N_Arguments (3);
+ Check_At_Most_N_Arguments (3);
Check_Optional_Identifier (Arg1, Name_Entity);
Check_Optional_Identifier (Arg2, Name_Check);
@@ -15316,7 +15315,7 @@
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (2);
+ Check_At_Most_N_Arguments (2);
-- Process first argument
@@ -15700,11 +15699,13 @@
begin
GNAT_Pragma;
- Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (1);
+ Check_Arg_Count (1);
Check_No_Identifiers;
Check_Pre_Post;
+ -- Rewrite Post[_Class] pragma as Precondition pragma setting the
+ -- flag Class_Present to True for the Post_Class case.
+
Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
PC_Pragma := New_Copy (N);
Set_Pragma_Identifier
@@ -15760,11 +15761,13 @@
begin
GNAT_Pragma;
- Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (1);
+ Check_Arg_Count (1);
Check_No_Identifiers;
Check_Pre_Post;
+ -- Rewrite Pre[_Class] pragma as Precondition pragma setting the
+ -- flag Class_Present to True for the Pre_Class case.
+
Set_Class_Present (N, Prag_Id = Pragma_Pre_Class);
PC_Pragma := New_Copy (N);
Set_Pragma_Identifier
@@ -15787,7 +15790,7 @@
begin
GNAT_Pragma;
Check_At_Least_N_Arguments (1);
- Check_At_Most_N_Arguments (2);
+ Check_At_Most_N_Arguments (2);
Check_Optional_Identifier (Arg1, Name_Check);
Check_Precondition_Postcondition (In_Body);
@@ -18317,6 +18320,34 @@
end loop;
end Title;
+ ----------------------------
+ -- Type_Invariant[_Class] --
+ ----------------------------
+
+ -- pragma Type_Invariant[_Class]
+ -- ([Entity =>] type_LOCAL_NAME,
+ -- [Check =>] EXPRESSION);
+
+ when Pragma_Type_Invariant |
+ Pragma_Type_Invariant_Class =>
+ Type_Invariant : declare
+ I_Pragma : Node_Id;
+
+ begin
+ Check_Arg_Count (2);
+
+ -- Rewrite Type_Invariant[_Class] pragma as an Invariant pragma,
+ -- setting Class_Present for the Type_Invariant_Class case.
+
+ Set_Class_Present (N, Prag_Id = Pragma_Type_Invariant_Class);
+ I_Pragma := New_Copy (N);
+ Set_Pragma_Identifier
+ (I_Pragma, Make_Identifier (Loc, Name_Invariant));
+ Rewrite (N, I_Pragma);
+ Set_Analyzed (N, False);
+ Analyze (N);
+ end Type_Invariant;
+
---------------------
-- Unchecked_Union --
---------------------
@@ -21493,6 +21524,8 @@
Pragma_Thread_Local_Storage => 0,
Pragma_Time_Slice => -1,
Pragma_Title => -1,
+ Pragma_Type_Invariant => -1,
+ Pragma_Type_Invariant_Class => -1,
Pragma_Unchecked_Union => 0,
Pragma_Unimplemented_Unit => -1,
Pragma_Universal_Aliasing => -1,
Index: par-prag.adb
===================================================================
--- par-prag.adb (revision 203522)
+++ par-prag.adb (working copy)
@@ -1293,6 +1293,8 @@
Pragma_Thread_Local_Storage |
Pragma_Time_Slice |
Pragma_Title |
+ Pragma_Type_Invariant |
+ Pragma_Type_Invariant_Class |
Pragma_Unchecked_Union |
Pragma_Unimplemented_Unit |
Pragma_Universal_Aliasing |
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb (revision 203522)
+++ sem_ch13.adb (working copy)
@@ -5961,7 +5961,6 @@
if Present (SId) then
PDecl := Unit_Declaration_Node (SId);
-
else
PDecl := Build_Invariant_Procedure_Declaration (Typ);
end if;
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl (revision 203522)
+++ snames.ads-tmpl (working copy)
@@ -144,8 +144,6 @@
Name_Dynamic_Predicate : constant Name_Id := N + $;
Name_Static_Predicate : constant Name_Id := N + $;
Name_Synchronization : constant Name_Id := N + $;
- Name_Type_Invariant : constant Name_Id := N + $;
- Name_Type_Invariant_Class : constant Name_Id := N + $;
-- Some special names used by the expander. Note that the lower case u's
-- at the start of these names get translated to extra underscores. These
@@ -448,7 +446,7 @@
Name_Wide_Character_Encoding : constant Name_Id := N + $; -- GNAT
Last_Configuration_Pragma_Name : constant Name_Id := N + $;
- -- Remaining pragma names
+ -- Remaining pragma names (non-configuration pragmas)
Name_Abort_Defer : constant Name_Id := N + $; -- GNAT
Name_Abstract_State : constant Name_Id := N + $; -- GNAT
@@ -621,6 +619,8 @@
Name_Thread_Local_Storage : constant Name_Id := N + $; -- GNAT
Name_Time_Slice : constant Name_Id := N + $; -- GNAT
Name_Title : constant Name_Id := N + $; -- GNAT
+ Name_Type_Invariant : constant Name_Id := N + $; -- GNAT
+ Name_Type_Invariant_Class : constant Name_Id := N + $; -- GNAT
Name_Unchecked_Union : constant Name_Id := N + $; -- Ada 05
Name_Unimplemented_Unit : constant Name_Id := N + $; -- GNAT
Name_Universal_Aliasing : constant Name_Id := N + $; -- GNAT
@@ -1905,6 +1905,8 @@
Pragma_Thread_Local_Storage,
Pragma_Time_Slice,
Pragma_Title,
+ Pragma_Type_Invariant,
+ Pragma_Type_Invariant_Class,
Pragma_Unchecked_Union,
Pragma_Unimplemented_Unit,
Pragma_Universal_Aliasing,
