This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
| Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
|---|---|---|
| Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
| Other format: | [Raw text] | |
This patch completes the implementation of predicates as described in
AI05-0153-1/06. There are two more aspects to be taken care of. First
we will likely decide that 'First/'Last should not be allowed if a
predicate is present, second we want to introduce the notion of a
static predicate usable in case statements.
The following two tests are compiled with -gnata12 -gnatj60 -gnatld7
and they both execute silently showing that all tests have passed.
Compiling: test_predicates.ads
1. with Ada.Assertions; use Ada.Assertions;
2. package Test_Predicates is
3.
4. type Even is range 0 .. Integer'Last with
5. Predicate => (Even mod 2) = 0;
6.
7. type Color is
8. (Red, Orange, Yellow, Green, Blue, Indigo, Violet);
9. subtype RGB is Color with
10. Predicate => RGB = Red or RGB in Green .. Blue;
11. subtype Other_Color is Color with
12. Predicate => Other_Color not in RGB;
13.
14. subtype Another_Color is Other_Color;
|
>>> info: "Another_Color" inherits predicate from
"Other_Color" at line 11
15. function Not_Another_One return Color;
16. -- Returns a value that violates
17. -- Another_Color's predicate
18.
19. type No_Defaults is private;
20. subtype No_Defaults_P is No_Defaults with
21. Predicate => Is_Good (No_Defaults_P);
22.
23. function Is_Good (X : No_Defaults) return Boolean;
24. function Good return No_Defaults;
25. function Bad return No_Defaults;
26. -- Is_Good(Good) is True; Is_Good(Bad) is False.
27.
28. type Defaults is private;
29. subtype Defaults_P is Defaults with
30. Predicate => Is_Good (Defaults_P);
31.
32. function Is_Good (X : Defaults) return Boolean;
33. function Good return Defaults;
34. function Bad return Defaults;
35.
36. type String_Ref is access all String;
37.
38. private
39.
40. type No_Defaults is
41. record
42. Comp : Integer;
43. Acc : String_Ref;
44. -- Default 'null' default doesn't count!
45. end record;
46.
47. type Defaults is
48. record
49. Comp : Integer := 0;
50. Acc : String_Ref := null;
51. end record;
52.
53. end Test_Predicates;
Compiling: test_predicates.adb
1.
2. package body Test_Predicates is
3.
4. function Not_Another_One return Color is
5. begin
6. return Result : constant Color := Red do
7. pragma Assert (Result in RGB);
8. pragma Assert
9. (Result not in Another_Color);
10. end return;
11. end Not_Another_One;
12.
13. function Is_Good
14. (X : No_Defaults) return Boolean is
15. begin
16. return X.Acc /= null;
17. end Is_Good;
18.
19. function Good return No_Defaults is
20. begin
21. return Result : constant No_Defaults
22. := (Comp => 0, Acc => new String'("xxx"))
23. do
24. pragma Assert (Result in No_Defaults_P);
25. pragma Assert (Is_Good (Result));
26. end return;
27. end Good;
28.
29. function Bad return No_Defaults is
30. begin
31. return Result : constant No_Defaults
32. := (Comp => 0, Acc => null)
33. do
34. pragma Assert (Result not in No_Defaults_P);
35. pragma Assert (not Is_Good (Result));
36. end return;
37. end Bad;
38.
39. function Is_Good (X : Defaults) return Boolean is
40. begin
41. return X.Acc /= null;
42. end Is_Good;
43.
44. function Good return Defaults is
45. begin
46. return Result : constant Defaults
47. := (Comp => 0, Acc => new String'("xxx"))
48. do
49. pragma Assert (Is_Good (Result));
50. pragma Assert (Result in Defaults_P);
51. end return;
52. end Good;
53.
54. function Bad return Defaults is
55. begin
56. return Result : constant Defaults
57. := (Comp => 0, Acc => null)
58. do
59. pragma Assert (not Is_Good (Result));
60. pragma Assert (Result not in Defaults_P);
61. end return;
62. end Bad;
63.
64. end Test_Predicates;
Compiling: test_predicates-acc.ads
1. package Test_Predicates.Acc is
2.
3. type Node (Discrim : Color) is
4. record
5. case Discrim is
6. when Red =>
7. Red_Comp : Integer;
8. when others =>
9. Others_Color_Comp : Integer;
10. end case;
11. end record;
12.
13. type Ref is access all Node;
14. subtype RGB_Ref is Ref with
15. Predicate => RGB_Ref.all.Discrim in RGB;
16. subtype Another_Color_Ref is Ref with
17. Predicate =>
18. Another_Color_Ref.all.Discrim
19. in Another_Color;
20.
21. end Test_Predicates.Acc;
Compiling: test_predicates-main.adb
1. with Test_Predicates.Acc;
2. use Test_Predicates.Acc;
3. procedure Test_Predicates.Main is
4. -- This test should run silently
5.
6. pragma Assert (RGB'First in RGB);
7. pragma Assert
8. (Another_Color'First not in Another_Color);
9.
10. pragma Assert (RGB'Last not in RGB);
11. pragma Assert
12. (Another_Color'Last in Another_Color);
13.
14. X1 : RGB;
15. -- OK; predicate not checked
16.
17. X2 : Another_Color;
18. -- OK; predicate not checked
19.
20. X3 : No_Defaults;
21. -- OK; no predicate
22.
23. X4 : No_Defaults_P;
24. -- OK; predicate not checked
25.
26. X5 : Defaults;
27. -- OK; no predicate
28.
29. X6 : RGB := Not_Another_One;
30. -- OK; predicate is True
31.
32. X7 : No_Defaults := Bad;
33. -- OK; no predicate
34.
35. X8 : No_Defaults_P := Good;
36. -- OK; predicate is True
37.
38. X9 : Defaults := Bad;
39. -- OK; no predicate
40.
41. X10 : Defaults_P := Good;
42. -- OK; predicate is True
43.
44. Even_Var_1 : Even;
45. -- OK; predicate not checked
46.
47. Even_Var_2 : Even := 100;
48. -- OK; predicate is True
49.
50. begin
51.
52. begin
53. Even_Var_1 := 1;
54. raise Program_Error;
55. -- Predicate should have failed
56. exception
57. when Assertion_Error =>
58. null; -- OK
59. end;
60.
61. Even_Var_1 := 0; -- OK; predicate is True
62.
63. begin
64. declare
65. Even_Var_3 : Even := Even_Var_2 + 1;
66. begin
67. raise Program_Error;
68. -- Predicate should have failed
69. end;
70. exception
71. when Assertion_Error =>
72. null; -- OK
73. end;
74.
75. ----------------
76.
77. begin
78. declare
79. Var : Another_Color := Not_Another_One;
80. begin
81. raise Program_Error;
82. -- Predicate should have failed
83. end;
84. exception
85. when Assertion_Error =>
86. null; -- OK
87. end;
88.
89. begin
90. declare
91. Var : Defaults_P := Bad;
92. begin
93. raise Program_Error;
94. -- Predicate should have failed
95. end;
96. exception
97. when Assertion_Error =>
98. null; -- OK
99. end;
100.
101. begin
102. declare
103. Var : No_Defaults_P := Bad;
104. begin
105. raise Program_Error;
106. -- Predicate should have failed
107. end;
108. exception
109. when Assertion_Error =>
110. null; -- OK
111. end;
112.
113. begin
114. declare
115. Var : Defaults_P;
116. -- Default init violates predicate
117. begin
118. raise Program_Error;
119. -- Predicate should have failed
120. end;
121. exception
122. when Assertion_Error =>
123. null; -- OK
124. end;
125.
126. X1 := Not_Another_One; -- OK; predicate is True
127.
128. begin
129. X2 := Not_Another_One;
130. raise Program_Error; -- Predicate should have failed
131. exception
132. when Assertion_Error =>
133. null; -- OK
134. end;
135.
136. X3 := Bad; -- OK; no predicate
137.
138. X4 := Good;
139. begin
140. X4 := Bad;
141. raise Program_Error;
142. -- Predicate should have failed
143. exception
144. when Assertion_Error =>
145. null; -- OK
146. end;
147.
148. X5 := Bad; -- OK; no predicate
149.
150. X6 := Not_Another_One;
151. -- OK; predicate is True
152.
153. X7 := Bad; -- OK; no predicate
154.
155. X8 := Good; -- OK; predicate is True
156. begin
157. X8 := Bad;
158. raise Program_Error;
159. -- Predicate should have failed
160. exception
161. when Assertion_Error =>
162. null; -- OK
163. end;
164.
165. X9 := Bad; -- OK; no predicate
166.
167. X10 := Good; -- OK; predicate is True
168. begin
169. X10 := Bad;
170. raise Program_Error;
171. -- Predicate should have failed
172. exception
173. when Assertion_Error =>
174. null; -- OK
175. end;
176.
177. ----------------
178.
179. declare
180. procedure P (X : Another_Color_Ref) is
181. begin
182. null;
183. end P;
184.
185. Var : Ref := new Node(Red);
186. begin
187. P (Var); -- Violate predicate of 'in' param
188. raise Program_Error;
189. exception
190. when Assertion_Error =>
191. null; -- OK
192. end;
193.
194. declare
195. procedure P (X : out Another_Color_Ref) is
196. begin
197. null;
198. -- Predicate of 'out' param
199. -- raises Constraint_Error
200. end P;
201.
202. Var : Ref;
203. begin
204. P (Var);
205. raise Program_Error;
206. exception
207. when Constraint_Error =>
208. null; -- OK
209. end;
210.
211. declare
212. procedure P (X : out Another_Color_Ref) is
213. begin
214. X := new Node(Orange);
215. end P;
216.
217. Var : Ref;
218. begin
219. P (Var);
220. -- OK; don't check predicate on the way 'in'
221. end;
222.
223. declare
224. procedure P (X : in out Another_Color_Ref) is
225. begin
226. X := new Node(Orange); -- Can't get here
227. end P;
228.
229. Var : Ref;
230. begin
231. P (Var);
232. -- Predicate of 'in out' param
233. -- raises Constraint_Error
234. raise Program_Error;
235. exception
236. when Constraint_Error =>
237. null; -- OK
238. end;
239.
240. end Test_Predicates.Main;
Compiling: test_predicates_lim.ads
1.
2. with Ada.Assertions; use Ada.Assertions;
3. package Test_Predicates_Lim is
4.
5. type No_Defaults is limited private;
6. subtype No_Defaults_P is No_Defaults with
7. Predicate => Is_Good (No_Defaults_P);
8.
9. function Is_Good (X : No_Defaults)
10. return Boolean;
11. function Good return No_Defaults;
12. function Bad return No_Defaults;
13. procedure Set_To_Bad (X : out No_Defaults);
14. procedure Set_To_Good (X : out No_Defaults);
15.
16. type Defaults is limited private;
17. subtype Defaults_P is Defaults with
18. Predicate => Is_Good (Defaults_P);
19.
20. function Is_Good (X : Defaults)
21. return Boolean;
22. function Good return Defaults;
23. function Bad return Defaults;
24. procedure Set_To_Bad (X : out Defaults);
25. procedure Set_To_Good (X : out Defaults);
26.
27. type String_Ref is access all String;
28.
29. private
30.
31. type No_Defaults is limited
32. record
33. Comp : Integer;
34. Acc : String_Ref;
35. -- Default 'null' default doesn't count!
36. end record;
37.
38. type Defaults is limited
39. record
40. Comp : Integer := 0;
41. Acc : String_Ref := null;
42. end record;
43.
44. end Test_Predicates_Lim;
Compiling: test_predicates_lim.adb
1. package body Test_Predicates_Lim is
2.
3. function Is_Good (X : No_Defaults)
4. return Boolean is
5. begin
6. return X.Acc /= null;
7. end Is_Good;
8.
9. function Good return No_Defaults is
10. begin
11. return Result : constant No_Defaults
12. := (Comp => 0, Acc => new String'("xxx"))
13. do
14. pragma Assert (Result in No_Defaults_P);
15. pragma Assert (Is_Good (Result));
16. end return;
17. end Good;
18.
19. function Bad return No_Defaults is
20. begin
21. return Result : constant No_Defaults
22. := (Comp => 0, Acc => null)
23. do
24. pragma Assert
25. (Result not in No_Defaults_P);
26. pragma Assert (not Is_Good (Result));
27. end return;
28. end Bad;
29.
30. procedure Set_To_Bad (X : out No_Defaults) is
31. begin
32. X.Acc := null;
33. pragma Assert (X not in No_Defaults_P);
34. pragma Assert (not Is_Good (X));
35. end Set_To_Bad;
36.
37. procedure Set_To_Good (X : out No_Defaults) is
38. begin
39. X.Acc := new String'("xxx");
40. pragma Assert (X in No_Defaults_P);
41. pragma Assert (Is_Good (X));
42. end Set_To_Good;
43.
44. function Is_Good (X : Defaults)
45. return Boolean is
46. begin
47. return X.Acc /= null;
48. end Is_Good;
49.
50. function Good return Defaults is
51. begin
52. return Result : constant Defaults
53. := (Comp => 0,
54. Acc => new String'("xxx"))
55. do
56. pragma Assert (Is_Good (Result));
57. pragma Assert
58. (Result in Defaults_P);
59. end return;
60. end Good;
61.
62. function Bad return Defaults is
63. begin
64. return Result : constant Defaults
65. := (Comp => 0, Acc => null)
66. do
67. pragma Assert
68. (not Is_Good (Result));
69. pragma Assert
70. (Result not in Defaults_P);
71. end return;
72. end Bad;
73.
74. procedure Set_To_Bad (X : out Defaults) is
75. begin
76. X.Acc := null;
77. pragma Assert (X not in Defaults_P);
78. pragma Assert (not Is_Good (X));
79. end Set_To_Bad;
80.
81. procedure Set_To_Good (X : out Defaults) is
82. begin
83. X.Acc := new String'("xxx");
84. pragma Assert (X in Defaults_P);
85. pragma Assert (Is_Good (X));
86. end Set_To_Good;
87.
88. end Test_Predicates_Lim;
Compiling: test_predicates_lim-main.adb
1. pragma Warnings (Off);
2. procedure Test_Predicates_Lim.Main is
3. -- This test should run silently
4.
5. X3 : No_Defaults;
6. -- OK; no predicate
7.
8. X4 : No_Defaults_P;
9. -- OK; predicate not checked
10.
11. X5 : Defaults;
12. -- OK; no predicate
13.
14. X7 : No_Defaults := Bad;
15. -- OK; no predicate
16.
17. X8 : No_Defaults_P := Good;
18. -- OK; predicate is True
19.
20. X9 : Defaults := Bad;
21. -- OK; no predicate
22.
23. X10 : Defaults := Good;
24. -- OK; predicate is True
25.
26. begin
27.
28. begin
29. declare
30. Var : Defaults_P;
31. -- Default init violates predicate
32. begin
33. raise Program_Error;
34. -- Predicate should have failed
35. end;
36. exception
37. when Assertion_Error =>
38. null; -- OK
39. end;
40.
41. begin
42. declare
43. Var : Defaults_P := Bad;
44. begin
45. raise Program_Error;
46. -- Predicate should have failed
47. end;
48. exception
49. when Assertion_Error =>
50. null; -- OK
51. end;
52.
53. begin
54. declare
55. Var : No_Defaults_P := Bad;
56. begin
57. raise Program_Error;
58. -- Predicate should have failed
59. end;
60. exception
61. when Assertion_Error =>
62. null; -- OK
63. end;
64.
65. declare
66. procedure P (X : No_Defaults_P) is
67. begin
68. null;
69. end P;
70. begin
71. P (Bad);
72. -- Violate predicate of 'in' param
73. exception
74. when Assertion_Error =>
75. null; -- OK
76. P (Good);
77. end;
78.
79. declare
80. procedure P (X : out No_Defaults_P) is
81. begin
82. Set_To_Bad (X);
83. -- Violate predicate of 'out' param
84. end P;
85. X : No_Defaults := Good;
86. begin
87. P (X);
88. exception
89. when Assertion_Error =>
90. null; -- OK
91. end;
92.
93. declare
94. procedure P (X : out No_Defaults_P) is
95. begin
96. Set_To_Good (X);
97. end P;
98. X : No_Defaults := Bad;
99. -- OK; no predicate
100. begin
101. P (X);
102. -- OK; no check for 'out' on the way in
103. end;
104.
105. declare
106. procedure P (X : in out No_Defaults_P) is
107. begin
108. Set_To_Bad (X);
109. -- Violate predicate of 'in out' param
110. end P;
111. X : No_Defaults := Good;
112. begin
113. P (X);
114. exception
115. when Assertion_Error =>
116. null; -- OK
117. end;
118.
119. end Test_Predicates_Lim.Main;
Tested on x86_64-pc-linux-gnu, committed on trunk
2010-10-22 Robert Dewar <dewar@adacore.com>
* exp_ch3.adb (Expand_N_Object_Declaration): Do required predicate
checks.
* sem_ch3.adb (Complete_Private_Subtype): Propagate predicates to full
view.
* sem_ch6.adb (Invariants_Or_Predicates_Present): New name for
Invariants_Present.
(Process_PPCs): Handle predicates generating post conditions
* sem_util.adb (Is_Partially_Initialized_Type): Add
Include_Null parameter.
* sem_util.ads (Is_Partially_Initialized_Type): Add
Include_Null parameter.
Attachment:
difs
Description: Text document
| Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
|---|---|---|
| Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |