Skip to content

Commit fb2e038

Browse files
chrisr-diffbluechrisr-diffblue
authored
Merge pull request #258 from tjj2017/subtype_constraint
Subtype constraint
2 parents 9f260a1 + 6c0bf21 commit fb2e038

File tree

7 files changed

+248
-4
lines changed

7 files changed

+248
-4
lines changed

‎experiments/golden-results/SPARK-tetris-summary.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,11 @@ Calling function: Process_Declaration
33
Error message: Package declaration
44
Nkind: N_Package_Declaration
55
--
6+
Occurs: 4 times
7+
Calling function: Process_Pragma_Declaration
8+
Error message: Unknown pragma
9+
Nkind: N_Pragma
10+
--
611
Occurs: 1 times
712
Redacted compiler error message:
813
"REDACTED" not declared in "REDACTED"

‎experiments/golden-results/UKNI-Information-Barrier-summary.txt

Lines changed: 22 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,44 @@
1-
Occurs: 27 times
1+
Occurs: 47 times
22
Calling function: Do_Expression
33
Error message: Unknown expression kind
44
Nkind: N_Expanded_Name
55
--
6-
Occurs: 3 times
6+
Occurs: 20 times
7+
Calling function: Do_Expression
8+
Error message: In
9+
Nkind: N_In
10+
--
11+
Occurs: 15 times
712
Calling function: Do_While_Statement
813
Error message: Wrong Nkind spec
914
Nkind: N_Loop_Statement
1015
--
16+
Occurs: 3 times
17+
Calling function: Do_Base_Range_Constraint
18+
Error message: unsupported upper range kind
19+
Nkind: N_Op_Add
20+
--
1121
Occurs: 1 times
1222
Calling function: Do_Base_Range_Constraint
1323
Error message: unsupported lower range kind
1424
Nkind: N_Attribute_Reference
1525
--
1626
Occurs: 1 times
1727
Calling function: Do_Base_Range_Constraint
28+
Error message: unsupported lower range kind
29+
Nkind: N_Selected_Component
30+
--
31+
Occurs: 1 times
32+
Calling function: Do_Base_Range_Constraint
1833
Error message: unsupported upper range kind
1934
Nkind: N_Attribute_Reference
2035
--
2136
Occurs: 1 times
37+
Calling function: Do_Base_Range_Constraint
38+
Error message: unsupported upper range kind
39+
Nkind: N_Selected_Component
40+
--
41+
Occurs: 1 times
2242
Calling function: Do_Expression
2343
Error message: Unknown expression kind
2444
Nkind: N_Range

‎experiments/golden-results/muen-summary.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,11 @@ Error message: Generic declaration
134134
Nkind: N_Generic_Subprogram_Declaration
135135
--
136136
Occurs: 2 times
137+
Calling function: Do_Expression
138+
Error message: Unknown expression kind
139+
Nkind: N_Expanded_Name
140+
--
141+
Occurs: 2 times
137142
Calling function: Do_Type_Definition
138143
Error message: Unknown expression kind
139144
Nkind: N_Access_Procedure_Definition

‎gnat2goto/driver/arrays.adb

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -382,12 +382,31 @@ package body Arrays is
382382
-- is pure
383383

384384
function Make_Array_Default_Initialiser (E : Entity_Id) return Irep is
385+
-- Note this function only works for one dimensional arrays at present.
385386
Idx : constant Node_Id := First_Index (E);
387+
-- The Entity is an array object
388+
-- The first index is a discrete_subtype_definition which
389+
-- may be a subtype_indication or a range.
390+
-- For determining the upper bounds and lower bounds a range is required
391+
-- and if the first index is a subtype_indication, the constraints
392+
-- of the subtype have to be obtained - which should be a range.
393+
Bound_Range : constant Node_Id :=
394+
(if Nkind (Idx) = N_Range
395+
then
396+
-- It is a range
397+
Idx
398+
elsif Nkind (Idx) = N_Subtype_Indication then
399+
-- It is an anonymous subtype
400+
Scalar_Range (Etype (Idx))
401+
else
402+
-- It is an explicitly declared subtype
403+
Scalar_Range (Entity (Idx)));
404+
386405
Lbound : constant Irep :=
387-
Typecast_If_Necessary (Do_Expression (Low_Bound (Idx)),
406+
Typecast_If_Necessary (Do_Expression (Low_Bound (Bound_Range)),
388407
CProver_Size_T, Global_Symbol_Table);
389408
Hbound : constant Irep :=
390-
Typecast_If_Necessary (Do_Expression (High_Bound (Idx)),
409+
Typecast_If_Necessary (Do_Expression (High_Bound (Bound_Range)),
391410
CProver_Size_T, Global_Symbol_Table);
392411
Source_Loc : constant Source_Ptr := Sloc (E);
393412
Len : constant Irep :=

‎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)