1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
Description: remove references to SPARK.
.
some files in gnat/ contain references to a 'SPARK' enumeral,
which is supposed to be defined in All_Restrictions, in
.../adainclude/s-rident.ads, installed by the gnat-x.y package.
However, the current version of gnat does not define SPARK; that is
introduced in AdaCore GPL 2011. So we remove references to SPARK.
Author: Stephen Leake <stephen_leake@stephe-leake.org>
Forwarded: not-needed
Index: gprbuild-2011/gnat/scng.adb
===================================================================
--- gprbuild-2011.orig/gnat/scng.adb 2011-08-01 05:19:05.000000000 -0400
+++ gprbuild-2011/gnat/scng.adb 2011-08-01 05:19:41.000000000 -0400
@@ -1792,47 +1792,6 @@
Token := Tok_Comment;
return;
end if;
-
- -- If the SPARK restriction is set for this unit, then generate
- -- a token Tok_SPARK_Hide for a SPARK HIDE directive.
-
- if Restriction_Check_Required (SPARK)
- and then Source (Start_Of_Comment) = '#'
- then
- declare
- Scan_SPARK_Ptr : Source_Ptr;
-
- begin
- Scan_SPARK_Ptr := Start_Of_Comment + 1;
-
- -- Scan out blanks
-
- while Source (Scan_SPARK_Ptr) = ' '
- or else Source (Scan_SPARK_Ptr) = HT
- loop
- Scan_SPARK_Ptr := Scan_SPARK_Ptr + 1;
- end loop;
-
- -- Recognize HIDE directive. SPARK input cannot be
- -- encoded as wide characters, so only deal with
- -- lower/upper case.
-
- if (Source (Scan_SPARK_Ptr) = 'h'
- or else Source (Scan_SPARK_Ptr) = 'H')
- and then (Source (Scan_SPARK_Ptr + 1) = 'i'
- or else Source (Scan_SPARK_Ptr + 1) = 'I')
- and then (Source (Scan_SPARK_Ptr + 2) = 'd'
- or else Source (Scan_SPARK_Ptr + 2) = 'D')
- and then (Source (Scan_SPARK_Ptr + 3) = 'e'
- or else Source (Scan_SPARK_Ptr + 3) = 'E')
- and then (Source (Scan_SPARK_Ptr + 4) = ' '
- or else Source (Scan_SPARK_Ptr + 4) = HT)
- then
- Token := Tok_SPARK_Hide;
- return;
- end if;
- end;
- end if;
end if;
end Minus_Case;
Index: gprbuild-2011/gnat/restrict.adb
===================================================================
--- gprbuild-2011.orig/gnat/restrict.adb 2011-09-08 19:12:58.000000000 -0400
+++ gprbuild-2011/gnat/restrict.adb 2011-09-08 19:11:57.000000000 -0400
@@ -114,58 +114,32 @@
N : Node_Id;
Force : Boolean := False)
is
- Msg_Issued : Boolean;
- Save_Error_Msg_Sloc : Source_Ptr;
- begin
- if Force or else Comes_From_Source (N) then
-
- if Restriction_Check_Required (SPARK)
- and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
- then
- return;
- end if;
-
- -- Since the call to Restriction_Msg from Check_Restriction may set
- -- Error_Msg_Sloc to the location of the pragma restriction, save and
- -- restore the previous value of the global variable around the call.
-
- Save_Error_Msg_Sloc := Error_Msg_Sloc;
- Check_Restriction (Msg_Issued, SPARK, First_Node (N));
- Error_Msg_Sloc := Save_Error_Msg_Sloc;
-
- if Msg_Issued then
- Error_Msg_F ("\\| " & Msg, N);
- end if;
- end if;
+ pragma Unreferenced (Msg);
+ pragma Unreferenced (N);
+ pragma Unreferenced (Force);
+ begin
+ -- Patched to work with Debian gnat-4.6, which does not define
+ -- SPARK in All_Restrictions (that is introduced in gnat GPL
+ -- 2011).
+ --
+ -- We don't delete this procedure in order to minimize the size
+ -- of the patch.
+ null;
end Check_SPARK_Restriction;
- procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id) is
- Msg_Issued : Boolean;
- Save_Error_Msg_Sloc : Source_Ptr;
- begin
- pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
-
- if Comes_From_Source (N) then
-
- if Restriction_Check_Required (SPARK)
- and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
- then
- return;
- end if;
-
- -- Since the call to Restriction_Msg from Check_Restriction may set
- -- Error_Msg_Sloc to the location of the pragma restriction, save and
- -- restore the previous value of the global variable around the call.
-
- Save_Error_Msg_Sloc := Error_Msg_Sloc;
- Check_Restriction (Msg_Issued, SPARK, First_Node (N));
- Error_Msg_Sloc := Save_Error_Msg_Sloc;
-
- if Msg_Issued then
- Error_Msg_F ("\\| " & Msg1, N);
- Error_Msg_F (Msg2, N);
- end if;
- end if;
+ procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id)
+ is
+ pragma Unreferenced (Msg1);
+ pragma Unreferenced (Msg2);
+ pragma Unreferenced (N);
+ begin
+ -- Patched to work with Debian gnat-4.6, which does not define
+ -- SPARK in All_Restrictions (that is introduced in gnat GPL
+ -- 2011).
+ --
+ -- We don't delete this procedure in order to minimize the size
+ -- of the patch.
+ null;
end Check_SPARK_Restriction;
-----------------------------------------
@@ -750,11 +724,7 @@
Name_Buffer (1 .. S'Last) := S;
Name_Len := S'Length;
- if R = SPARK then
- Set_All_Upper_Case;
- else
- Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N))));
- end if;
+ Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N))));
Error_Msg_Strlen := Name_Len;
Error_Msg_String (1 .. Name_Len) := Name_Buffer (1 .. Name_Len);
|
