1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- I N T E R F A C E S . C --
9 -- This specification is derived from the Ada Reference Manual for use with --
10 -- GNAT. In accordance with the copyright of that document, you can freely --
11 -- copy and modify this specification, provided that if you redistribute a --
12 -- modified version, any changes that you have made are clearly indicated. --
14 ------------------------------------------------------------------------------
16 -- Preconditions in this unit are meant for analysis only, not for run-time
17 -- checking, so that the expected exceptions are raised. This is enforced by
18 -- setting the corresponding assertion policy to Ignore. Postconditions and
19 -- contract cases should not be executed at runtime as well, in order not to
20 -- slow down the execution of these functions.
22 pragma Assertion_Policy
(Pre
=> Ignore
,
24 Contract_Cases
=> Ignore
,
27 -- Pre/postconditions use a fully qualified name for the standard "+" operator
28 -- in order to work around an internal limitation of the compiler.
31 with System
.Parameters
;
33 package Interfaces
.C
with
39 -- Each of the types declared in Interfaces.C is C-compatible.
41 -- The types int, short, long, unsigned, ptrdiff_t, size_t, double,
42 -- char, wchar_t, char16_t, and char32_t correspond respectively to the
43 -- C types having the same names. The types signed_char, unsigned_short,
44 -- unsigned_long, unsigned_char, C_bool, C_float, and long_double
45 -- correspond respectively to the C types signed char, unsigned
46 -- short, unsigned long, unsigned char, bool, float, and long double.
48 -- Declaration's based on C's <limits.h>
50 CHAR_BIT
: constant := 8;
51 SCHAR_MIN
: constant := -128;
52 SCHAR_MAX
: constant := 127;
53 UCHAR_MAX
: constant := 255;
55 -- Signed and Unsigned Integers. Note that in GNAT, we have ensured that
56 -- the standard predefined Ada types correspond to the standard C types
58 -- Note: the Integer qualifications used in the declaration of type long
59 -- avoid ambiguities when compiling in the presence of s-auxdec.ads and
60 -- a non-private system.address type.
62 type int
is new Integer;
63 type short
is new Short_Integer;
64 type long
is range -(2 ** (System
.Parameters
.long_bits
- Integer'(1)))
65 .. +(2 ** (System.Parameters.long_bits - Integer'(1))) - 1;
66 type long_long
is new Long_Long_Integer;
68 type signed_char
is range SCHAR_MIN
.. SCHAR_MAX
;
69 for signed_char
'Size use CHAR_BIT
;
71 type unsigned
is mod 2 ** int
'Size;
72 type unsigned_short
is mod 2 ** short
'Size;
73 type unsigned_long
is mod 2 ** long
'Size;
74 type unsigned_long_long
is mod 2 ** long_long
'Size;
76 type unsigned_char
is mod (UCHAR_MAX
+ 1);
77 for unsigned_char
'Size use CHAR_BIT
;
79 -- Note: Ada RM states that the type of the subtype plain_char is either
80 -- signed_char or unsigned_char, depending on the C implementation. GNAT
81 -- instead choses unsigned_char always.
83 subtype plain_char
is unsigned_char
;
85 -- Note: the Integer qualifications used in the declaration of ptrdiff_t
86 -- avoid ambiguities when compiling in the presence of s-auxdec.ads and
87 -- a non-private system.address type.
90 range -System
.Memory_Size
/ 2 .. System
.Memory_Size
/ 2 - 1;
92 type size_t
is mod System
.Memory_Size
;
96 type C_bool
is new Boolean;
97 pragma Convention
(C
, C_bool
);
101 type C_float
is new Float;
102 type double
is new Standard
.Long_Float;
103 type long_double
is new Standard
.Long_Long_Float;
105 ----------------------------
106 -- Characters and Strings --
107 ----------------------------
109 type char
is new Character;
111 nul
: constant char
:= char
'First;
113 -- The functions To_C and To_Ada map between the Ada type Character and the
116 function To_C
(Item
: Character) return char
118 Post
=> To_C
'Result = char
'Val (Character'Pos (Item
));
120 function To_Ada
(Item
: char
) return Character
122 Post
=> To_Ada
'Result = Character'Val (char
'Pos (Item
));
124 type char_array
is array (size_t
range <>) of aliased char
;
125 for char_array
'Component_Size use CHAR_BIT
;
127 function Is_Nul_Terminated
(Item
: char_array
) return Boolean
129 Post
=> Is_Nul_Terminated
'Result = (for some C
of Item
=> C
= nul
);
130 -- The result of Is_Nul_Terminated is True if Item contains nul, and is
133 function C_Length_Ghost
(Item
: char_array
) return size_t
136 Pre
=> Is_Nul_Terminated
(Item
),
137 Post
=> C_Length_Ghost
'Result <= Item
'Last - Item
'First
138 and then Item
(Item
'First + C_Length_Ghost
'Result) = nul
139 and then (for all J
in Item
'First .. Item
'First + C_Length_Ghost
'Result
140 when J
/= Item
'First + C_Length_Ghost
'Result =>
142 -- Ghost function to compute the length of a char_array up to the first nul
147 Append_Nul
: Boolean := True) return char_array
149 Pre
=> not (Append_Nul
= False and then Item
'Length = 0),
150 Post
=> To_C
'Result'First = 0
151 and then To_C'Result'Length
=
152 (if Append_Nul
then Standard
."+" (Item
'Length, 1) else Item
'Length)
153 and then (for all J
in Item
'Range =>
154 To_C
'Result (size_t
(J
- Item
'First)) = To_C
(Item
(J
)))
155 and then (if Append_Nul
then To_C
'Result (To_C
'Result'Last) = nul);
156 -- The result of To_C is a char_array value of length Item'Length (if
157 -- Append_Nul is False) or Item'Length+1 (if Append_Nul is True). The lower
158 -- bound is 0. For each component Item(I), the corresponding component
159 -- in the result is To_C applied to Item(I). The value nul is appended if
160 -- Append_Nul is True. If Append_Nul is False and Item'Length is 0, then
161 -- To_C propagates Constraint_Error.
165 Trim_Nul : Boolean := True) return String
167 Pre => (if Trim_Nul then
168 Is_Nul_Terminated (Item)
169 and then C_Length_Ghost (Item) <= size_t (Natural'Last)
171 Item'Last - Item'First < size_t (Natural'Last)),
172 Post => To_Ada'Result'First
= 1
173 and then To_Ada
'Result'Length =
174 (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
175 and then (for all J in To_Ada'Result'Range =>
177 To_Ada
(Item
(size_t
(J
) - 1 + Item
'First)));
178 -- The result of To_Ada is a String whose length is Item'Length (if
179 -- Trim_Nul is False) or the length of the slice of Item preceding the
180 -- first nul (if Trim_Nul is True). The lower bound of the result is 1.
181 -- If Trim_Nul is False, then for each component Item(I) the corresponding
182 -- component in the result is To_Ada applied to Item(I). If Trim_Nul
183 -- is True, then for each component Item(I) before the first nul the
184 -- corresponding component in the result is To_Ada applied to Item(I). The
185 -- function propagates Terminator_Error if Trim_Nul is True and Item does
190 Target
: out char_array
;
192 Append_Nul
: Boolean := True)
194 Relaxed_Initialization
=> Target
,
195 Pre
=> Target
'Length >=
196 (if Append_Nul
then Standard
."+" (Item
'Length, 1) else Item
'Length),
197 Post
=> Count
= (if Append_Nul
then Item
'Length + 1 else Item
'Length)
200 Target
(Target
'First .. Target
'First + (Count
- 1))'Initialized)
202 (for all J
in Item
'Range =>
203 Target
(Target
'First + size_t
(J
- Item
'First)) = To_C
(Item
(J
)))
205 (if Append_Nul
then Target
(Target
'First + (Count
- 1)) = nul
);
206 -- For procedure To_C, each element of Item is converted (via the To_C
207 -- function) to a char, which is assigned to the corresponding element of
208 -- Target. If Append_Nul is True, nul is then assigned to the next element
209 -- of Target. In either case, Count is set to the number of Target elements
210 -- assigned. If Target is not long enough, Constraint_Error is propagated.
216 Trim_Nul
: Boolean := True)
218 Relaxed_Initialization
=> Target
,
219 Pre
=> (if Trim_Nul
then
220 Is_Nul_Terminated
(Item
)
221 and then C_Length_Ghost
(Item
) <= size_t
(Target
'Length)
223 Item
'Last - Item
'First < size_t
(Target
'Length)),
225 (if Trim_Nul
then Natural (C_Length_Ghost
(Item
)) else Item
'Length)
228 Target
(Target
'First .. Target
'First + (Count
- 1))'Initialized)
230 (for all J
in Target
'First .. Target
'First + (Count
- 1) =>
232 To_Ada
(Item
(size_t
(J
- Target
'First) + Item
'First)));
233 -- For procedure To_Ada, each element of Item (if Trim_Nul is False) or
234 -- each element of Item preceding the first nul (if Trim_Nul is True) is
235 -- converted (via the To_Ada function) to a Character, which is assigned
236 -- to the corresponding element of Target. Count is set to the number of
237 -- Target elements assigned. If Target is not long enough, Constraint_Error
238 -- is propagated. If Trim_Nul is True and Item does not contain nul, then
239 -- Terminator_Error is propagated.
241 ------------------------------------
242 -- Wide Character and Wide String --
243 ------------------------------------
245 type wchar_t
is new Wide_Character;
246 for wchar_t
'Size use Standard
'Wchar_T_Size;
248 wide_nul
: constant wchar_t
:= wchar_t
'First;
250 -- To_C and To_Ada provide the mappings between the Ada and C wide
253 function To_C
(Item
: Wide_Character) return wchar_t
255 Post
=> To_C
'Result = wchar_t
(Item
);
257 function To_Ada
(Item
: wchar_t
) return Wide_Character
259 Post
=> To_Ada
'Result = Wide_Character (Item
);
261 type wchar_array
is array (size_t
range <>) of aliased wchar_t
;
263 function Is_Nul_Terminated
(Item
: wchar_array
) return Boolean
265 Post
=> Is_Nul_Terminated
'Result = (for some C
of Item
=> C
= wide_nul
);
266 -- The result of Is_Nul_Terminated is True if Item contains wide_nul, and
267 -- is False otherwise.
269 -- The To_C and To_Ada subprograms that convert between Wide_String and
270 -- wchar_array have analogous effects to the To_C and To_Ada subprograms
271 -- that convert between String and char_array, except that wide_nul is
272 -- used instead of nul.
274 function C_Length_Ghost
(Item
: wchar_array
) return size_t
277 Pre
=> Is_Nul_Terminated
(Item
),
278 Post
=> C_Length_Ghost
'Result <= Item
'Last - Item
'First
279 and then Item
(Item
'First + C_Length_Ghost
'Result) = wide_nul
280 and then (for all J
in Item
'First .. Item
'First + C_Length_Ghost
'Result
281 when J
/= Item
'First + C_Length_Ghost
'Result =>
282 Item
(J
) /= wide_nul
);
283 -- Ghost function to compute the length of a wchar_array up to the first
284 -- wide_nul character.
288 Append_Nul
: Boolean := True) return wchar_array
290 Pre
=> not (Append_Nul
= False and then Item
'Length = 0),
291 Post
=> To_C
'Result'First = 0
292 and then To_C'Result'Length
=
293 (if Append_Nul
then Standard
."+" (Item
'Length, 1) else Item
'Length)
294 and then (for all J
in Item
'Range =>
295 To_C
'Result (size_t
(J
- Item
'First)) = To_C
(Item
(J
)))
296 and then (if Append_Nul
then To_C
'Result (To_C
'Result'Last) = wide_nul);
300 Trim_Nul : Boolean := True) return Wide_String
302 Pre => (if Trim_Nul then
303 Is_Nul_Terminated (Item)
304 and then C_Length_Ghost (Item) <= size_t (Natural'Last)
306 Item'Last - Item'First < size_t (Natural'Last)),
307 Post => To_Ada'Result'First
= 1
308 and then To_Ada
'Result'Length =
309 (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
310 and then (for all J in To_Ada'Result'Range =>
312 To_Ada
(Item
(size_t
(J
) - 1 + Item
'First)));
316 Target
: out wchar_array
;
318 Append_Nul
: Boolean := True)
320 Relaxed_Initialization
=> Target
,
321 Pre
=> Target
'Length >=
322 (if Append_Nul
then Standard
."+" (Item
'Length, 1) else Item
'Length),
323 Post
=> Count
= (if Append_Nul
then Item
'Length + 1 else Item
'Length)
326 Target
(Target
'First .. Target
'First + (Count
- 1))'Initialized)
328 (for all J
in Item
'Range =>
329 Target
(Target
'First + size_t
(J
- Item
'First)) = To_C
(Item
(J
)))
331 (if Append_Nul
then Target
(Target
'First + (Count
- 1)) = wide_nul
);
335 Target
: out Wide_String;
337 Trim_Nul
: Boolean := True)
339 Relaxed_Initialization
=> Target
,
340 Pre
=> (if Trim_Nul
then
341 Is_Nul_Terminated
(Item
)
342 and then C_Length_Ghost
(Item
) <= size_t
(Target
'Length)
344 Item
'Last - Item
'First < size_t
(Target
'Length)),
346 (if Trim_Nul
then Natural (C_Length_Ghost
(Item
)) else Item
'Length)
349 Target
(Target
'First .. Target
'First + (Count
- 1))'Initialized)
351 (for all J
in Target
'First .. Target
'First + (Count
- 1) =>
353 To_Ada
(Item
(size_t
(J
- Target
'First) + Item
'First)));
355 Terminator_Error
: exception;
357 -- The remaining declarations are for Ada 2005 (AI-285)
359 -- ISO/IEC 10646:2003 compatible types defined by SC22/WG14 document N1010
361 type char16_t
is new Wide_Character;
362 pragma Ada_05
(char16_t
);
364 char16_nul
: constant char16_t
:= char16_t
'Val (0);
365 pragma Ada_05
(char16_nul
);
367 -- To_C and To_Ada provide mappings between the Ada and C 16-bit character
370 function To_C
(Item
: Wide_Character) return char16_t
372 Post
=> To_C
'Result = char16_t
(Item
);
373 pragma Ada_05
(To_C
);
375 function To_Ada
(Item
: char16_t
) return Wide_Character
377 Post
=> To_Ada
'Result = Wide_Character (Item
);
378 pragma Ada_05
(To_Ada
);
380 type char16_array
is array (size_t
range <>) of aliased char16_t
;
381 pragma Ada_05
(char16_array
);
383 function Is_Nul_Terminated
(Item
: char16_array
) return Boolean
385 Post
=> Is_Nul_Terminated
'Result = (for some C
of Item
=> C
= char16_nul
);
386 pragma Ada_05
(Is_Nul_Terminated
);
387 -- The result of Is_Nul_Terminated is True if Item contains char16_nul, and
388 -- is False otherwise.
390 -- The To_C and To_Ada subprograms that convert between Wide_String and
391 -- char16_array have analogous effects to the To_C and To_Ada subprograms
392 -- that convert between String and char_array, except that char16_nul is
393 -- used instead of nul.
395 function C_Length_Ghost
(Item
: char16_array
) return size_t
398 Pre
=> Is_Nul_Terminated
(Item
),
399 Post
=> C_Length_Ghost
'Result <= Item
'Last - Item
'First
400 and then Item
(Item
'First + C_Length_Ghost
'Result) = char16_nul
401 and then (for all J
in Item
'First .. Item
'First + C_Length_Ghost
'Result
402 when J
/= Item
'First + C_Length_Ghost
'Result =>
403 Item
(J
) /= char16_nul
);
404 -- Ghost function to compute the length of a char16_array up to the first
405 -- char16_nul character.
409 Append_Nul
: Boolean := True) return char16_array
411 Pre
=> not (Append_Nul
= False and then Item
'Length = 0),
412 Post
=> To_C
'Result'First = 0
413 and then To_C'Result'Length
=
414 (if Append_Nul
then Standard
."+" (Item
'Length, 1) else Item
'Length)
415 and then (for all J
in Item
'Range =>
416 To_C
'Result (size_t
(J
- Item
'First)) = To_C
(Item
(J
)))
418 (if Append_Nul
then To_C
'Result (To_C
'Result'Last) = char16_nul);
419 pragma Ada_05 (To_C);
422 (Item : char16_array;
423 Trim_Nul : Boolean := True) return Wide_String
425 Pre => (if Trim_Nul then
426 Is_Nul_Terminated (Item)
427 and then C_Length_Ghost (Item) <= size_t (Natural'Last)
429 Item'Last - Item'First < size_t (Natural'Last)),
430 Post => To_Ada'Result'First
= 1
431 and then To_Ada
'Result'Length =
432 (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
433 and then (for all J in To_Ada'Result'Range =>
435 To_Ada
(Item
(size_t
(J
) - 1 + Item
'First)));
436 pragma Ada_05
(To_Ada
);
440 Target
: out char16_array
;
442 Append_Nul
: Boolean := True)
444 Relaxed_Initialization
=> Target
,
445 Pre
=> Target
'Length >=
446 (if Append_Nul
then Standard
."+" (Item
'Length, 1) else Item
'Length),
447 Post
=> Count
= (if Append_Nul
then Item
'Length + 1 else Item
'Length)
450 Target
(Target
'First .. Target
'First + (Count
- 1))'Initialized)
452 (for all J
in Item
'Range =>
453 Target
(Target
'First + size_t
(J
- Item
'First)) = To_C
(Item
(J
)))
455 (if Append_Nul
then Target
(Target
'First + (Count
- 1)) = char16_nul
);
456 pragma Ada_05
(To_C
);
459 (Item
: char16_array
;
460 Target
: out Wide_String;
462 Trim_Nul
: Boolean := True)
464 Relaxed_Initialization
=> Target
,
465 Pre
=> (if Trim_Nul
then
466 Is_Nul_Terminated
(Item
)
467 and then C_Length_Ghost
(Item
) <= size_t
(Target
'Length)
469 Item
'Last - Item
'First < size_t
(Target
'Length)),
471 (if Trim_Nul
then Natural (C_Length_Ghost
(Item
)) else Item
'Length)
474 Target
(Target
'First .. Target
'First + (Count
- 1))'Initialized)
476 (for all J
in Target
'First .. Target
'First + (Count
- 1) =>
478 To_Ada
(Item
(size_t
(J
- Target
'First) + Item
'First)));
479 pragma Ada_05
(To_Ada
);
481 type char32_t
is new Wide_Wide_Character
;
482 pragma Ada_05
(char32_t
);
484 char32_nul
: constant char32_t
:= char32_t
'Val (0);
485 pragma Ada_05
(char32_nul
);
487 -- To_C and To_Ada provide mappings between the Ada and C 32-bit character
490 function To_C
(Item
: Wide_Wide_Character
) return char32_t
492 Post
=> To_C
'Result = char32_t
(Item
);
493 pragma Ada_05
(To_C
);
495 function To_Ada
(Item
: char32_t
) return Wide_Wide_Character
497 Post
=> To_Ada
'Result = Wide_Wide_Character
(Item
);
498 pragma Ada_05
(To_Ada
);
500 type char32_array
is array (size_t
range <>) of aliased char32_t
;
501 pragma Ada_05
(char32_array
);
503 function Is_Nul_Terminated
(Item
: char32_array
) return Boolean
505 Post
=> Is_Nul_Terminated
'Result = (for some C
of Item
=> C
= char32_nul
);
506 pragma Ada_05
(Is_Nul_Terminated
);
507 -- The result of Is_Nul_Terminated is True if Item contains char32_nul, and
508 -- is False otherwise.
510 function C_Length_Ghost
(Item
: char32_array
) return size_t
513 Pre
=> Is_Nul_Terminated
(Item
),
514 Post
=> C_Length_Ghost
'Result <= Item
'Last - Item
'First
515 and then Item
(Item
'First + C_Length_Ghost
'Result) = char32_nul
516 and then (for all J
in Item
'First .. Item
'First + C_Length_Ghost
'Result
517 when J
/= Item
'First + C_Length_Ghost
'Result =>
518 Item
(J
) /= char32_nul
);
519 -- Ghost function to compute the length of a char32_array up to the first
520 -- char32_nul character.
522 -- The To_C and To_Ada subprograms that convert between Wide_Wide_String
523 -- and char32_array have analogous effects to the To_C and To_Ada
524 -- subprograms that convert between String and char_array, except
525 -- that char32_nul is used instead of nul.
528 (Item
: Wide_Wide_String
;
529 Append_Nul
: Boolean := True) return char32_array
531 Pre
=> not (Append_Nul
= False and then Item
'Length = 0),
532 Post
=> To_C
'Result'First = 0
533 and then To_C'Result'Length
=
534 (if Append_Nul
then Standard
."+" (Item
'Length, 1) else Item
'Length)
535 and then (for all J
in Item
'Range =>
536 To_C
'Result (size_t
(J
- Item
'First)) = To_C
(Item
(J
)))
538 (if Append_Nul
then To_C
'Result (To_C
'Result'Last) = char32_nul);
539 pragma Ada_05 (To_C);
542 (Item : char32_array;
543 Trim_Nul : Boolean := True) return Wide_Wide_String
545 Pre => (if Trim_Nul then
546 Is_Nul_Terminated (Item)
547 and then C_Length_Ghost (Item) <= size_t (Natural'Last)
549 Item'Last - Item'First < size_t (Natural'Last)),
550 Post => To_Ada'Result'First
= 1
551 and then To_Ada
'Result'Length =
552 (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
553 and then (for all J in To_Ada'Result'Range =>
555 To_Ada
(Item
(size_t
(J
) - 1 + Item
'First)));
556 pragma Ada_05
(To_Ada
);
559 (Item
: Wide_Wide_String
;
560 Target
: out char32_array
;
562 Append_Nul
: Boolean := True)
564 Relaxed_Initialization
=> Target
,
565 Pre
=> Target
'Length >=
566 (if Append_Nul
then Standard
."+" (Item
'Length, 1) else Item
'Length),
567 Post
=> Count
= (if Append_Nul
then Item
'Length + 1 else Item
'Length)
570 Target
(Target
'First .. Target
'First + (Count
- 1))'Initialized)
572 (for all J
in Item
'Range =>
573 Target
(Target
'First + size_t
(J
- Item
'First)) = To_C
(Item
(J
)))
575 (if Append_Nul
then Target
(Target
'First + (Count
- 1)) = char32_nul
);
576 pragma Ada_05
(To_C
);
579 (Item
: char32_array
;
580 Target
: out Wide_Wide_String
;
582 Trim_Nul
: Boolean := True)
584 Relaxed_Initialization
=> Target
,
585 Pre
=> (if Trim_Nul
then
586 Is_Nul_Terminated
(Item
)
587 and then C_Length_Ghost
(Item
) <= size_t
(Target
'Length)
589 Item
'Last - Item
'First < size_t
(Target
'Length)),
591 (if Trim_Nul
then Natural (C_Length_Ghost
(Item
)) else Item
'Length)
594 Target
(Target
'First .. Target
'First + (Count
- 1))'Initialized)
596 (for all J
in Target
'First .. Target
'First + (Count
- 1) =>
598 To_Ada
(Item
(size_t
(J
- Target
'First) + Item
'First)));
599 pragma Ada_05
(To_Ada
);