1 ------------------------------------------------------------------------------
3 -- GNAT COMPILER COMPONENTS --
5 -- I N T E R F A C E S . C . S T R I N G S --
9 -- Copyright (C) 1993-2024, Free Software Foundation, Inc. --
11 -- This specification is derived from the Ada Reference Manual for use with --
12 -- GNAT. The copyright notice above, and the license provisions that follow --
13 -- apply solely to the contents of the part following the private keyword. --
15 -- GNAT is free software; you can redistribute it and/or modify it under --
16 -- terms of the GNU General Public License as published by the Free Soft- --
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
22 -- As a special exception under Section 7 of GPL version 3, you are granted --
23 -- additional permissions described in the GCC Runtime Library Exception, --
24 -- version 3.1, as published by the Free Software Foundation. --
26 -- You should have received a copy of the GNU General Public License and --
27 -- a copy of the GCC Runtime Library Exception along with this program; --
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
29 -- <http://www.gnu.org/licenses/>. --
31 -- GNAT was originally developed by the GNAT team at New York University. --
32 -- Extensive contributions were provided by Ada Core Technologies Inc. --
34 ------------------------------------------------------------------------------
36 -- Preconditions in this unit are meant for analysis only, not for run-time
37 -- checking, so that the expected exceptions are raised. This is enforced by
38 -- setting the corresponding assertion policy to Ignore. These preconditions
39 -- protect from Constraint_Error, Dereference_Error and Update_Error, but not
40 -- from Storage_Error.
42 pragma Assertion_Policy
(Pre
=> Ignore
);
44 package Interfaces
.C
.Strings
with
46 Abstract_State
=> (C_Memory
),
47 Initializes
=> (C_Memory
),
52 type char_array_access
is access all char_array
;
53 for char_array_access
'Size use System
.Parameters
.ptr_bits
;
55 pragma No_Strict_Aliasing
(char_array_access
);
56 -- Since this type is used for external interfacing, with the pointer
57 -- coming from who knows where, it seems a good idea to turn off any
58 -- strict aliasing assumptions for this type.
60 type chars_ptr
is private;
61 pragma Preelaborable_Initialization
(chars_ptr
);
63 type chars_ptr_array
is array (size_t
range <>) of aliased chars_ptr
;
65 Null_Ptr
: constant chars_ptr
;
68 (Item
: char_array_access
;
69 Nul_Check
: Boolean := False) return chars_ptr
71 SPARK_Mode
=> Off
; -- To_Chars_Ptr'Result is aliased with Item
73 function New_Char_Array
(Chars
: char_array
) return chars_ptr
with
75 Post
=> New_Char_Array
'Result /= Null_Ptr
,
76 Global
=> (Input
=> C_Memory
);
78 function New_String
(Str
: String) return chars_ptr
with
80 Post
=> New_String
'Result /= Null_Ptr
,
81 Global
=> (Input
=> C_Memory
);
83 procedure Free
(Item
: in out chars_ptr
) with
85 -- When deallocation is prohibited (eg: cert runtimes) this routine
86 -- will raise Program_Error
88 Dereference_Error
: exception;
90 function Value
(Item
: chars_ptr
) return char_array
with
91 Pre
=> Item
/= Null_Ptr
,
92 Global
=> (Input
=> C_Memory
);
96 Length
: size_t
) return char_array
98 Pre
=> Item
/= Null_Ptr
and then Length
/= 0,
99 Global
=> (Input
=> C_Memory
);
101 function Value
(Item
: chars_ptr
) return String with
102 Pre
=> Item
/= Null_Ptr
,
103 Global
=> (Input
=> C_Memory
);
107 Length
: size_t
) return String
109 Pre
=> Item
/= Null_Ptr
and then Length
/= 0,
110 Global
=> (Input
=> C_Memory
);
112 function Strlen
(Item
: chars_ptr
) return size_t
with
113 Pre
=> Item
/= Null_Ptr
,
114 Global
=> (Input
=> C_Memory
);
120 Check
: Boolean := True)
124 and then (Chars
'First /= 0 or else Chars
'Last /= size_t
'Last)
125 and then Chars
'Length <= size_t
'Last - Offset
126 and then Chars
'Length + Offset
<= Strlen
(Item
),
127 Global
=> (In_Out
=> C_Memory
);
133 Check
: Boolean := True)
137 and then Str
'Length <= size_t
'Last - Offset
138 and then Str
'Length + Offset
<= Strlen
(Item
),
139 Global
=> (In_Out
=> C_Memory
);
141 Update_Error
: exception;
144 pragma SPARK_Mode
(Off
);
145 type chars_ptr
is access all Character;
146 for chars_ptr
'Size use System
.Parameters
.ptr_bits
;
148 pragma No_Strict_Aliasing
(chars_ptr
);
149 -- Since this type is used for external interfacing, with the pointer
150 -- coming from who knows where, it seems a good idea to turn off any
151 -- strict aliasing assumptions for this type.
153 Null_Ptr
: constant chars_ptr
:= null;
154 end Interfaces
.C
.Strings
;