Skip to content

Commit 41356c6

Browse files
tjj2017tjj2017
committed
Added test to check array constraints
1 parent 64883ac commit 41356c6

File tree

3 files changed

+195
-0
lines changed

3 files changed

+195
-0
lines changed

‎testsuite/gnat2goto/tests/arrays_constraints/array_constraints.adb‎

Lines changed: 184 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,184 @@
1+
procedure Array_Constraints is
2+
type Enum is (One, Two, Three, Four, Five, Six);
3+
subtype S_Enum is Enum range One .. Five;
4+
subtype S_Enum_No_Constraint is S_Enum;
5+
subtype My_Bool is Boolean;
6+
7+
type My_Mod is Mod 2**8;
8+
subtype S_Mod_Constrained is My_Mod range 1 .. 127;
9+
subtype S_Mod_No_Constraint is My_Mod;
10+
11+
subtype S_Constrained is Integer range 1 .. 10;
12+
subtype S_No_Constraint is S_Constrained;
13+
subtype S_No_Constraint_2 is S_No_Constraint;
14+
15+
-- The following subtype declaration causes gnat2goto to report unsupported
16+
-- lower and upper range kinds and so has been coomented and placed in a
17+
-- separate test program
18+
-- subtype S_Char_Constrained is Character range 'a' .. 'z';
19+
subtype S_Char_No_Constraint is Character;
20+
21+
type Constrained_Array_1 is array (Integer range 1 .. 10) of Integer;
22+
type Constrained_Array_2 is array (S_Constrained) of Integer;
23+
type Constrained_Array_3 is array (S_No_Constraint) of Integer;
24+
type Constrained_Array_4 is array (S_No_Constraint_2) of Integer;
25+
26+
type Unconstrained_Array is array (Integer range <>) of Integer;
27+
type U_A_Enum is array (Enum range <>) of Integer;
28+
type U_A_Bool is array (Boolean range <>) of Integer;
29+
type U_A_Char is array (Character range <>) of Integer;
30+
type U_A_Mod is array (My_Mod range <>) of Integer;
31+
32+
subtype UA1 is Unconstrained_Array (S_Constrained);
33+
subtype UA2 is Unconstrained_Array (S_No_Constraint);
34+
subtype UA3 is Unconstrained_Array (S_No_Constraint_2);
35+
subtype UA4 is Unconstrained_Array (S_Constrained range 2 .. 9);
36+
37+
subtype UA_Enum_1 is U_A_Enum (One .. Two);
38+
subtype UA_Enum_2 is U_A_Enum (Enum);
39+
subtype UA_Enum_3 is U_A_Enum (S_Enum);
40+
subtype UA_Enum_4 is U_A_Enum (S_Enum_No_Constraint);
41+
subtype UA_Enum_5 is U_A_Enum (Enum range Two .. Six);
42+
43+
subtype UA_Bool_1 is U_A_Bool (False .. True);
44+
subtype UA_Bool_2 is U_A_Bool (Boolean);
45+
subtype UA_Bool_3 is U_A_Bool (My_Bool);
46+
subtype UA_Bool_4 is U_A_Bool (My_Bool range True .. True);
47+
48+
subtype UA_Char_1 is U_A_Char ('A' .. 'Z');
49+
-- subtype UA_Char_2 is U_A_Char (S_Char_Constrained);
50+
subtype UA_Char_3 is U_A_Char (S_Char_No_Constraint);
51+
subtype UA_Char_4 is U_A_Char (Character);
52+
subtype UA_Char_5 is U_A_Char (Character range '0' .. '9');
53+
54+
subtype UA_Mod_1 is U_A_Mod (My_Mod range 1 .. 10);
55+
subtype UA_Mod_2 is U_A_Mod (S_Mod_Constrained);
56+
subtype UA_Mod_3 is U_A_Mod (S_Mod_No_Constraint);
57+
subtype UA_Mod_4 is U_A_Mod (My_Mod);
58+
59+
VUA1 : UA1;
60+
VUA2 : UA2;
61+
VUA3 : UA3;
62+
VUA4 : Unconstrained_Array (S_Constrained);
63+
VUA5 : Unconstrained_Array (S_No_Constraint);
64+
VUA6 : Unconstrained_Array (S_No_Constraint_2);
65+
VUA7 : Unconstrained_Array (1 .. 10);
66+
VUA8 : UA4;
67+
68+
VCA1 : Constrained_Array_1;
69+
VCA2 : Constrained_Array_2;
70+
VCA3 : Constrained_Array_3;
71+
VCA4 : Constrained_Array_4;
72+
73+
VEA1 : UA_Enum_1;
74+
VEA2 : UA_Enum_2;
75+
VEA3 : U_A_Enum (One .. Three);
76+
VEA4 : U_A_Enum (Enum);
77+
VEA5 : UA_Enum_4;
78+
VEA6 : UA_Enum_5;
79+
80+
81+
VBA1 : UA_Bool_1;
82+
VBA2 : UA_Bool_2;
83+
VBA3 : U_A_Bool (False .. True);
84+
VBA4 : U_A_Bool (Boolean);
85+
VBA5 : UA_Bool_3;
86+
VBA6 : UA_Bool_4;
87+
88+
VAC1 : UA_Char_1;
89+
-- VAC2 : UA_Char_2;
90+
VAC3 : UA_Char_3;
91+
VAC4 : UA_Char_4;
92+
VAC5 : UA_Char_5;
93+
VAC6 : U_A_Char ('x' .. 'z');
94+
-- VAC7 : U_A_Char (S_Char_Constrained);
95+
VAC8 : U_A_Char (S_Char_No_Constraint);
96+
VAC9 : U_A_Char (S_Char_No_Constraint range 'a' .. 'f');
97+
98+
VAM1 : UA_Mod_1;
99+
VAM2 : UA_Mod_2;
100+
VAM3 : UA_Mod_3;
101+
VAM4 : UA_Mod_4;
102+
VAM5 : U_A_Mod (My_Mod range 1 .. 10);
103+
VAM6 : U_A_Mod (S_Mod_Constrained);
104+
VAM7 : U_A_Mod (S_Mod_No_Constraint);
105+
VAM8 : U_A_Mod (My_Mod);
106+
VAM9 : U_A_Mod (1 .. 20);
107+
108+
begin
109+
VUA1 (1) := 1;
110+
VUA2 (2) := 2;
111+
VUA3 (3) := 3;
112+
VUA4 (4) := 4;
113+
VUA5 (5) := 5;
114+
VUA6 (6) := 6;
115+
VUA7 (7) := 7;
116+
VUA8 (8) := 8;
117+
pragma Assert (VUA1 (1) +
118+
VUA2 (2) +
119+
VUA3 (3) +
120+
VUA4 (4) +
121+
VUA5 (5) +
122+
VUA6 (6) +
123+
VUA7 (7) +
124+
VUA8 (8) =
125+
36);
126+
127+
VCA1 (VCA1'Last) := 1;
128+
VCA2 (VCA2'Last - 1) := 2;
129+
VCA3 (VCA3'Last - 2) := 3;
130+
VCA4 (Constrained_Array_4'Last - 3) := 4;
131+
pragma Assert (VCA1 (VCA1'Last) +
132+
VCA2 (VCA2'Last - 1) +
133+
VCA3 (VCA3'Last - 2) +
134+
VCA4 (Constrained_Array_4'Last - 3) =
135+
10);
136+
137+
VEA1 (One) := 1;
138+
VEA2 (Two) := 2;
139+
VEA3 (Three) := 3;
140+
VEA4 (Four) := 4;
141+
VEA5 (Five) := 5;
142+
VEA6 (Six) := 6;
143+
pragma Assert (VEA1 (One) + VEA2 (Two) + VEA3 (Three) +
144+
VEA4 (Four) + VEA5 (Five) + VEA6 (Six) = 21);
145+
146+
VBA1 (False) := 0;
147+
VBA2 (True) := 1;
148+
149+
VBA3 (False) := 0;
150+
VBA4 (True) := 1;
151+
152+
VBA5 (False) := 2;
153+
VBA6 (True) := 3;
154+
pragma Assert (VBA1 (False) + VBA2 (True) + VBA3 (False) + VBA4 (True) +
155+
VBA5 (False) + VBA6 (True) = 7);
156+
157+
VAC1 ('A') := 1;
158+
-- VAC2 ('a') := 2;
159+
VAC3 ('b') := 3;
160+
VAC4 ('c') := 4;
161+
VAC5 ('0') := 5;
162+
VAC6 ('x') := 6;
163+
-- VAC7 ('d') := 7;
164+
VAC8 ('e') := 8;
165+
VAC9 ('f') := 9;
166+
pragma Assert (VAC1 ('A') + -- VAC2 ('a') +
167+
VAC3 ('b') + VAC4 ('c') +
168+
VAC5 ('0') + VAC6 ('x') + -- VAC7 ('d') +
169+
VAC8 ('e') + VAC9 ('f') = 36);
170+
171+
VAM1 (1) := 1;
172+
VAM2 (2) := 2;
173+
VAM3 (3) := 3;
174+
VAM4 (4) := 4;
175+
VAM5 (5) := 5;
176+
VAM6 (6) := 6;
177+
VAM7 (7) := 7;
178+
VAM8 (8) := 8;
179+
VAM9 (9) := 9;
180+
pragma Assert (VAM1 (1) + VAM2 (2) + VAM3 (3) + VAM4 (4) +
181+
VAM5 (5) + VAM6 (6) + VAM7 (7) + VAM8 (8) + VAM9 (9) = 45);
182+
183+
end Array_Constraints
184+
;

‎testsuite/gnat2goto/tests/arrays_constraints/test.out‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
[1] file array_constraints.adb line 117 assertion: SUCCESS
2+
[2] file array_constraints.adb line 131 assertion: SUCCESS
3+
[3] file array_constraints.adb line 143 assertion: SUCCESS
4+
[4] file array_constraints.adb line 154 assertion: SUCCESS
5+
[5] file array_constraints.adb line 166 assertion: SUCCESS
6+
[6] file array_constraints.adb line 180 assertion: SUCCESS
7+
VERIFICATION SUCCESSFUL
8+

‎testsuite/gnat2goto/tests/arrays_constraints/test.py‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
from test_support import *
2+
3+
prove()

0 commit comments

Comments
 (0)