-- --
------------------------------------------------------------------------------
-package body Interfaces.C is
+-- Ghost code, loop invariants and assertions in this unit are meant for
+-- analysis only, not for run-time checking, as it would be too costly
+-- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
+package body Interfaces.C
+ with SPARK_Mode
+is
+
+ --------------------
+ -- C_Length_Ghost --
+ --------------------
+
+ function C_Length_Ghost (Item : char_array) return size_t is
+ begin
+ for J in Item'Range loop
+ if Item (J) = nul then
+ return J - Item'First;
+ end if;
+
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Item (K) /= nul);
+ end loop;
+
+ raise Program_Error;
+ end C_Length_Ghost;
+
+ function C_Length_Ghost (Item : wchar_array) return size_t is
+ begin
+ for J in Item'Range loop
+ if Item (J) = wide_nul then
+ return J - Item'First;
+ end if;
+
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Item (K) /= wide_nul);
+ end loop;
+
+ raise Program_Error;
+ end C_Length_Ghost;
+
+ function C_Length_Ghost (Item : char16_array) return size_t is
+ begin
+ for J in Item'Range loop
+ if Item (J) = char16_nul then
+ return J - Item'First;
+ end if;
+
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Item (K) /= char16_nul);
+ end loop;
+
+ raise Program_Error;
+ end C_Length_Ghost;
+
+ function C_Length_Ghost (Item : char32_array) return size_t is
+ begin
+ for J in Item'Range loop
+ if Item (J) = char32_nul then
+ return J - Item'First;
+ end if;
+
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Item (K) /= char32_nul);
+ end loop;
+
+ raise Program_Error;
+ end C_Length_Ghost;
-----------------------
-- Is_Nul_Terminated --
if Item (J) = nul then
return True;
end if;
+
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Item (K) /= nul);
end loop;
return False;
if Item (J) = wide_nul then
return True;
end if;
+
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Item (K) /= wide_nul);
end loop;
return False;
if Item (J) = char16_nul then
return True;
end if;
+
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Item (K) /= char16_nul);
end loop;
return False;
if Item (J) = char32_nul then
return True;
end if;
+
+ pragma Loop_Invariant
+ (for all K in Item'First .. J => Item (K) /= char32_nul);
end loop;
return False;
From := Item'First;
loop
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant
+ (for some J in From .. Item'Last => Item (J) = nul);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From when J /= From =>
+ Item (J) /= nul);
+
if From > Item'Last then
raise Terminator_Error;
elsif Item (From) = nul then
end if;
end loop;
+ pragma Assert (From = Item'First + C_Length_Ghost (Item));
+
Count := Natural (From - Item'First);
else
end if;
declare
- R : String (1 .. Count);
+ Count_Cst : constant Natural := Count;
+ R : String (1 .. Count_Cst) with Relaxed_Initialization;
begin
for J in R'Range loop
- R (J) := To_Ada (Item (size_t (J) + (Item'First - 1)));
+ R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
+
+ pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
end loop;
return R;
Trim_Nul : Boolean := True)
is
From : size_t;
- To : Positive;
+ To : Integer;
begin
if Trim_Nul then
From := Item'First;
loop
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant
+ (for some J in From .. Item'Last => Item (J) = nul);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From when J /= From =>
+ Item (J) /= nul);
+
if From > Item'Last then
raise Terminator_Error;
elsif Item (From) = nul then
for J in 1 .. Count loop
Target (To) := Character (Item (From));
+
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant (To in Target'Range);
+ pragma Loop_Invariant (To = Target'First + (J - 1));
+ pragma Loop_Invariant (From = Item'First + size_t (J - 1));
+ pragma Loop_Invariant
+ (for all J in Target'First .. To => Target (J)'Initialized);
+ pragma Loop_Invariant
+ (Target (Target'First .. To)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Target'First .. To =>
+ Target (K) =
+ To_Ada (Item (size_t (K - Target'First) + Item'First)));
+
+ -- Avoid possible overflow when incrementing To in the last
+ -- iteration of the loop.
+ exit when J = Count;
+
From := From + 1;
To := To + 1;
end loop;
end if;
-
end To_Ada;
-- Convert wchar_t to Wide_Character
From := Item'First;
loop
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant
+ (for some J in From .. Item'Last => Item (J) = wide_nul);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From when J /= From =>
+ Item (J) /= wide_nul);
+
if From > Item'Last then
raise Terminator_Error;
elsif Item (From) = wide_nul then
end if;
end loop;
+ pragma Assert (From = Item'First + C_Length_Ghost (Item));
+
Count := Natural (From - Item'First);
else
end if;
declare
- R : Wide_String (1 .. Count);
+ Count_Cst : constant Natural := Count;
+ R : Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
begin
for J in R'Range loop
- R (J) := To_Ada (Item (size_t (J) + (Item'First - 1)));
+ R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
+
+ pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
end loop;
return R;
Trim_Nul : Boolean := True)
is
From : size_t;
- To : Positive;
+ To : Integer;
begin
if Trim_Nul then
From := Item'First;
loop
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant
+ (for some J in From .. Item'Last => Item (J) = wide_nul);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From when J /= From =>
+ Item (J) /= wide_nul);
+
if From > Item'Last then
raise Terminator_Error;
elsif Item (From) = wide_nul then
for J in 1 .. Count loop
Target (To) := To_Ada (Item (From));
+
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant (To in Target'Range);
+ pragma Loop_Invariant (To = Target'First + (J - 1));
+ pragma Loop_Invariant (From = Item'First + size_t (J - 1));
+ pragma Loop_Invariant
+ (for all J in Target'First .. To => Target (J)'Initialized);
+ pragma Loop_Invariant
+ (Target (Target'First .. To)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Target'First .. To =>
+ Target (K) =
+ To_Ada (Item (size_t (K - Target'First) + Item'First)));
+
+ -- Avoid possible overflow when incrementing To in the last
+ -- iteration of the loop.
+ exit when J = Count;
+
From := From + 1;
To := To + 1;
end loop;
From := Item'First;
loop
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant
+ (for some J in From .. Item'Last => Item (J) = char16_nul);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From when J /= From =>
+ Item (J) /= char16_nul);
+
if From > Item'Last then
raise Terminator_Error;
- elsif Item (From) = char16_t'Val (0) then
+ elsif Item (From) = char16_nul then
exit;
else
From := From + 1;
end if;
end loop;
+ pragma Assert (From = Item'First + C_Length_Ghost (Item));
+
Count := Natural (From - Item'First);
else
end if;
declare
- R : Wide_String (1 .. Count);
+ Count_Cst : constant Natural := Count;
+ R : Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
begin
for J in R'Range loop
- R (J) := To_Ada (Item (size_t (J) + (Item'First - 1)));
+ R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
+
+ pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
end loop;
return R;
Trim_Nul : Boolean := True)
is
From : size_t;
- To : Positive;
+ To : Integer;
begin
if Trim_Nul then
From := Item'First;
loop
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant
+ (for some J in From .. Item'Last => Item (J) = char16_nul);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From when J /= From =>
+ Item (J) /= char16_nul);
+
if From > Item'Last then
raise Terminator_Error;
- elsif Item (From) = char16_t'Val (0) then
+ elsif Item (From) = char16_nul then
exit;
else
From := From + 1;
for J in 1 .. Count loop
Target (To) := To_Ada (Item (From));
+
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant (To in Target'Range);
+ pragma Loop_Invariant (To = Target'First + (J - 1));
+ pragma Loop_Invariant (From = Item'First + size_t (J - 1));
+ pragma Loop_Invariant
+ (for all J in Target'First .. To => Target (J)'Initialized);
+ pragma Loop_Invariant
+ (Target (Target'First .. To)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Target'First .. To =>
+ Target (K) =
+ To_Ada (Item (size_t (K - Target'First) + Item'First)));
+
+ -- Avoid possible overflow when incrementing To in the last
+ -- iteration of the loop.
+ exit when J = Count;
+
From := From + 1;
To := To + 1;
end loop;
From := Item'First;
loop
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant
+ (for some J in From .. Item'Last => Item (J) = char32_nul);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From when J /= From =>
+ Item (J) /= char32_nul);
+
if From > Item'Last then
raise Terminator_Error;
- elsif Item (From) = char32_t'Val (0) then
+ elsif Item (From) = char32_nul then
exit;
else
From := From + 1;
end if;
end loop;
+ pragma Assert (From = Item'First + C_Length_Ghost (Item));
+
Count := Natural (From - Item'First);
else
end if;
declare
- R : Wide_Wide_String (1 .. Count);
+ Count_Cst : constant Natural := Count;
+ R : Wide_Wide_String (1 .. Count_Cst) with Relaxed_Initialization;
begin
for J in R'Range loop
- R (J) := To_Ada (Item (size_t (J) + (Item'First - 1)));
+ R (J) := To_Ada (Item (size_t (J) - 1 + Item'First));
+
+ pragma Loop_Invariant (for all K in 1 .. J => R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ R (K) = To_Ada (Item (size_t (K) - 1 + Item'First)));
end loop;
return R;
Trim_Nul : Boolean := True)
is
From : size_t;
- To : Positive;
+ To : Integer;
begin
if Trim_Nul then
From := Item'First;
loop
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant
+ (for some J in From .. Item'Last => Item (J) = char32_nul);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From when J /= From =>
+ Item (J) /= char32_nul);
+
if From > Item'Last then
raise Terminator_Error;
- elsif Item (From) = char32_t'Val (0) then
+ elsif Item (From) = char32_nul then
exit;
else
From := From + 1;
for J in 1 .. Count loop
Target (To) := To_Ada (Item (From));
+
+ pragma Loop_Invariant (From in Item'Range);
+ pragma Loop_Invariant (To in Target'Range);
+ pragma Loop_Invariant (To = Target'First + (J - 1));
+ pragma Loop_Invariant (From = Item'First + size_t (J - 1));
+ pragma Loop_Invariant
+ (for all J in Target'First .. To => Target (J)'Initialized);
+ pragma Loop_Invariant
+ (Target (Target'First .. To)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Target'First .. To =>
+ Target (K) =
+ To_Ada (Item (size_t (K - Target'First) + Item'First)));
+
+ -- Avoid possible overflow when incrementing To in the last
+ -- iteration of the loop.
+ exit when J = Count;
+
From := From + 1;
To := To + 1;
end loop;
begin
if Append_Nul then
declare
- R : char_array (0 .. Item'Length);
+ R : char_array (0 .. Item'Length) with Relaxed_Initialization;
begin
for J in Item'Range loop
R (size_t (J - Item'First)) := To_C (Item (J));
+
+ pragma Loop_Invariant
+ (for all K in 0 .. size_t (J - Item'First) =>
+ R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ R (size_t (K - Item'First)) = To_C (Item (K)));
end loop;
R (R'Last) := nul;
+
+ pragma Assert
+ (for all J in Item'Range =>
+ R (size_t (J - Item'First)) = To_C (Item (J)));
+
return R;
end;
else
declare
- R : char_array (0 .. Item'Length - 1);
+ R : char_array (0 .. Item'Length - 1)
+ with Relaxed_Initialization;
begin
for J in Item'Range loop
R (size_t (J - Item'First)) := To_C (Item (J));
+
+ pragma Loop_Invariant
+ (for all K in 0 .. size_t (J - Item'First) =>
+ R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ R (size_t (K - Item'First)) = To_C (Item (K)));
end loop;
return R;
To := Target'First;
for From in Item'Range loop
Target (To) := char (Item (From));
+
+ pragma Loop_Invariant (To in Target'Range);
+ pragma Loop_Invariant
+ (To - Target'First = size_t (From - Item'First));
+ pragma Loop_Invariant
+ (for all J in Target'First .. To => Target (J)'Initialized);
+ pragma Loop_Invariant
+ (Target (Target'First .. To)'Initialized);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From =>
+ Target (Target'First + size_t (J - Item'First)) =
+ To_C (Item (J)));
+
To := To + 1;
end loop;
begin
if Append_Nul then
declare
- R : wchar_array (0 .. Item'Length);
+ R : wchar_array (0 .. Item'Length) with Relaxed_Initialization;
begin
for J in Item'Range loop
R (size_t (J - Item'First)) := To_C (Item (J));
+
+ pragma Loop_Invariant
+ (for all K in 0 .. size_t (J - Item'First) =>
+ R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ R (size_t (K - Item'First)) = To_C (Item (K)));
end loop;
R (R'Last) := wide_nul;
+
+ pragma Assert
+ (for all J in Item'Range =>
+ R (size_t (J - Item'First)) = To_C (Item (J)));
+
return R;
end;
else
declare
- R : wchar_array (0 .. Item'Length - 1);
+ R : wchar_array (0 .. Item'Length - 1)
+ with Relaxed_Initialization;
begin
- for J in size_t range 0 .. Item'Length - 1 loop
- R (J) := To_C (Item (Integer (J) + Item'First));
+ for J in Item'Range loop
+ R (size_t (J - Item'First)) := To_C (Item (J));
+
+ pragma Loop_Invariant
+ (for all K in 0 .. size_t (J - Item'First) =>
+ R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ R (size_t (K - Item'First)) = To_C (Item (K)));
end loop;
return R;
To := Target'First;
for From in Item'Range loop
Target (To) := To_C (Item (From));
+
+ pragma Loop_Invariant (To in Target'Range);
+ pragma Loop_Invariant
+ (To - Target'First = size_t (From - Item'First));
+ pragma Loop_Invariant
+ (for all J in Target'First .. To => Target (J)'Initialized);
+ pragma Loop_Invariant
+ (Target (Target'First .. To)'Initialized);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From =>
+ Target (Target'First + size_t (J - Item'First)) =
+ To_C (Item (J)));
+
To := To + 1;
end loop;
+ pragma Assert
+ (for all J in Item'Range =>
+ Target (Target'First + size_t (J - Item'First)) =
+ To_C (Item (J)));
+ pragma Assert
+ (if Item'Length /= 0 then
+ Target (Target'First ..
+ Target'First + (Item'Length - 1))'Initialized);
+
if Append_Nul then
if To > Target'Last then
raise Constraint_Error;
begin
if Append_Nul then
declare
- R : char16_array (0 .. Item'Length);
+ R : char16_array (0 .. Item'Length) with Relaxed_Initialization;
begin
for J in Item'Range loop
R (size_t (J - Item'First)) := To_C (Item (J));
+
+ pragma Loop_Invariant
+ (for all K in 0 .. size_t (J - Item'First) =>
+ R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ R (size_t (K - Item'First)) = To_C (Item (K)));
end loop;
- R (R'Last) := char16_t'Val (0);
+ R (R'Last) := char16_nul;
+
+ pragma Assert
+ (for all J in Item'Range =>
+ R (size_t (J - Item'First)) = To_C (Item (J)));
+
return R;
end;
else
declare
- R : char16_array (0 .. Item'Length - 1);
+ R : char16_array (0 .. Item'Length - 1)
+ with Relaxed_Initialization;
begin
- for J in size_t range 0 .. Item'Length - 1 loop
- R (J) := To_C (Item (Integer (J) + Item'First));
+ for J in Item'Range loop
+ R (size_t (J - Item'First)) := To_C (Item (J));
+
+ pragma Loop_Invariant
+ (for all K in 0 .. size_t (J - Item'First) =>
+ R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ R (size_t (K - Item'First)) = To_C (Item (K)));
end loop;
return R;
To := Target'First;
for From in Item'Range loop
Target (To) := To_C (Item (From));
+
+ pragma Loop_Invariant (To in Target'Range);
+ pragma Loop_Invariant
+ (To - Target'First = size_t (From - Item'First));
+ pragma Loop_Invariant
+ (for all J in Target'First .. To => Target (J)'Initialized);
+ pragma Loop_Invariant
+ (Target (Target'First .. To)'Initialized);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From =>
+ Target (Target'First + size_t (J - Item'First)) =
+ To_C (Item (J)));
+
To := To + 1;
end loop;
+ pragma Assert
+ (for all J in Item'Range =>
+ Target (Target'First + size_t (J - Item'First)) =
+ To_C (Item (J)));
+ pragma Assert
+ (if Item'Length /= 0 then
+ Target (Target'First ..
+ Target'First + (Item'Length - 1))'Initialized);
+
if Append_Nul then
if To > Target'Last then
raise Constraint_Error;
else
- Target (To) := char16_t'Val (0);
+ Target (To) := char16_nul;
Count := Item'Length + 1;
end if;
begin
if Append_Nul then
declare
- R : char32_array (0 .. Item'Length);
+ R : char32_array (0 .. Item'Length) with Relaxed_Initialization;
begin
for J in Item'Range loop
R (size_t (J - Item'First)) := To_C (Item (J));
+
+ pragma Loop_Invariant
+ (for all K in 0 .. size_t (J - Item'First) =>
+ R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ R (size_t (K - Item'First)) = To_C (Item (K)));
end loop;
- R (R'Last) := char32_t'Val (0);
+ R (R'Last) := char32_nul;
+
+ pragma Assert
+ (for all J in Item'Range =>
+ R (size_t (J - Item'First)) = To_C (Item (J)));
+
return R;
end;
else
declare
- R : char32_array (0 .. Item'Length - 1);
+ R : char32_array (0 .. Item'Length - 1)
+ with Relaxed_Initialization;
begin
- for J in size_t range 0 .. Item'Length - 1 loop
- R (J) := To_C (Item (Integer (J) + Item'First));
+ for J in Item'Range loop
+ R (size_t (J - Item'First)) := To_C (Item (J));
+
+ pragma Loop_Invariant
+ (for all K in 0 .. size_t (J - Item'First) =>
+ R (K)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Item'First .. J =>
+ R (size_t (K - Item'First)) = To_C (Item (K)));
end loop;
return R;
To := Target'First;
for From in Item'Range loop
Target (To) := To_C (Item (From));
+
+ pragma Loop_Invariant (To in Target'Range);
+ pragma Loop_Invariant
+ (To - Target'First = size_t (From - Item'First));
+ pragma Loop_Invariant
+ (for all J in Target'First .. To => Target (J)'Initialized);
+ pragma Loop_Invariant
+ (Target (Target'First .. To)'Initialized);
+ pragma Loop_Invariant
+ (for all J in Item'First .. From =>
+ Target (Target'First + size_t (J - Item'First)) =
+ To_C (Item (J)));
+
To := To + 1;
end loop;
+ pragma Assert
+ (for all J in Item'Range =>
+ Target (Target'First + size_t (J - Item'First)) =
+ To_C (Item (J)));
+ pragma Assert
+ (if Item'Length /= 0 then
+ Target (Target'First ..
+ Target'First + (Item'Length - 1))'Initialized);
+
if Append_Nul then
if To > Target'Last then
raise Constraint_Error;
else
- Target (To) := char32_t'Val (0);
+ Target (To) := char32_nul;
Count := Item'Length + 1;
end if;
-- --
------------------------------------------------------------------------------
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
with System.Parameters;
-package Interfaces.C is
- pragma Pure;
+package Interfaces.C
+ with SPARK_Mode, Pure
+is
+ -- Each of the types declared in Interfaces.C is C-compatible.
+
+ -- The types int, short, long, unsigned, ptrdiff_t, size_t, double,
+ -- char, wchar_t, char16_t, and char32_t correspond respectively to the
+ -- C types having the same names. The types signed_char, unsigned_short,
+ -- unsigned_long, unsigned_char, C_bool, C_float, and long_double
+ -- correspond respectively to the C types signed char, unsigned
+ -- short, unsigned long, unsigned char, bool, float, and long double.
-- Declaration's based on C's <limits.h>
type unsigned_char is mod (UCHAR_MAX + 1);
for unsigned_char'Size use CHAR_BIT;
- subtype plain_char is unsigned_char; -- ??? should be parameterized
+ -- Note: Ada RM states that the type of the subtype plain_char is either
+ -- signed_char or unsigned_char, depending on the C implementation. GNAT
+ -- instead choses unsigned_char always.
+
+ subtype plain_char is unsigned_char;
-- Note: the Integer qualifications used in the declaration of ptrdiff_t
-- avoid ambiguities when compiling in the presence of s-auxdec.ads and
nul : constant char := char'First;
- function To_C (Item : Character) return char;
- function To_Ada (Item : char) return Character;
+ -- The functions To_C and To_Ada map between the Ada type Character and the
+ -- C type char.
+
+ function To_C (Item : Character) return char
+ with
+ Post => To_C'Result = char'Val (Character'Pos (Item));
+
+ function To_Ada (Item : char) return Character
+ with
+ Post => To_Ada'Result = Character'Val (char'Pos (Item));
type char_array is array (size_t range <>) of aliased char;
for char_array'Component_Size use CHAR_BIT;
- function Is_Nul_Terminated (Item : char_array) return Boolean;
+ function Is_Nul_Terminated (Item : char_array) return Boolean
+ with
+ Post => Is_Nul_Terminated'Result = (for some C of Item => C = nul);
+ -- The result of Is_Nul_Terminated is True if Item contains nul, and is
+ -- False otherwise.
+
+ function C_Length_Ghost (Item : char_array) return size_t
+ with
+ Ghost,
+ Pre => Is_Nul_Terminated (Item),
+ Post => C_Length_Ghost'Result <= Item'Last - Item'First
+ and then Item (Item'First + C_Length_Ghost'Result) = nul
+ and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
+ when J /= Item'First + C_Length_Ghost'Result =>
+ Item (J) /= nul);
+ -- Ghost function to compute the length of a char_array up to the first nul
+ -- character.
function To_C
(Item : String;
- Append_Nul : Boolean := True) return char_array;
+ Append_Nul : Boolean := True) return char_array
+ with
+ Pre => not (Append_Nul = False and then Item'Length = 0),
+ Post => To_C'Result'First = 0
+ and then To_C'Result'Length =
+ (if Append_Nul then Item'Length + 1 else Item'Length)
+ and then (for all J in Item'Range =>
+ To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
+ and then (if Append_Nul then To_C'Result (To_C'Result'Last) = nul);
+ -- The result of To_C is a char_array value of length Item'Length (if
+ -- Append_Nul is False) or Item'Length+1 (if Append_Nul is True). The lower
+ -- bound is 0. For each component Item(I), the corresponding component
+ -- in the result is To_C applied to Item(I). The value nul is appended if
+ -- Append_Nul is True. If Append_Nul is False and Item'Length is 0, then
+ -- To_C propagates Constraint_Error.
function To_Ada
(Item : char_array;
- Trim_Nul : Boolean := True) return String;
+ Trim_Nul : Boolean := True) return String
+ with
+ Pre => (if Trim_Nul then
+ Is_Nul_Terminated (Item)
+ and then C_Length_Ghost (Item) <= size_t (Natural'Last)
+ else
+ Item'Last - Item'First < size_t (Natural'Last)),
+ Post => To_Ada'Result'First = 1
+ and then To_Ada'Result'Length =
+ (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
+ and then (for all J in To_Ada'Result'Range =>
+ To_Ada'Result (J) =
+ To_Ada (Item (size_t (J) - 1 + Item'First)));
+ -- The result of To_Ada is a String whose length is Item'Length (if
+ -- Trim_Nul is False) or the length of the slice of Item preceding the
+ -- first nul (if Trim_Nul is True). The lower bound of the result is 1.
+ -- If Trim_Nul is False, then for each component Item(I) the corresponding
+ -- component in the result is To_Ada applied to Item(I). If Trim_Nul
+ -- is True, then for each component Item(I) before the first nul the
+ -- corresponding component in the result is To_Ada applied to Item(I). The
+ -- function propagates Terminator_Error if Trim_Nul is True and Item does
+ -- not contain nul.
procedure To_C
(Item : String;
Target : out char_array;
Count : out size_t;
- Append_Nul : Boolean := True);
+ Append_Nul : Boolean := True)
+ with
+ Relaxed_Initialization => Target,
+ Pre => Target'Length >=
+ (if Append_Nul then Item'Length + 1 else Item'Length),
+ Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
+ and then
+ (if Count /= 0 then
+ Target (Target'First .. Target'First + (Count - 1))'Initialized)
+ and then
+ (for all J in Item'Range =>
+ Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
+ and then
+ (if Append_Nul then Target (Target'First + (Count - 1)) = nul);
+ -- For procedure To_C, each element of Item is converted (via the To_C
+ -- function) to a char, which is assigned to the corresponding element of
+ -- Target. If Append_Nul is True, nul is then assigned to the next element
+ -- of Target. In either case, Count is set to the number of Target elements
+ -- assigned. If Target is not long enough, Constraint_Error is propagated.
procedure To_Ada
(Item : char_array;
Target : out String;
Count : out Natural;
- Trim_Nul : Boolean := True);
+ Trim_Nul : Boolean := True)
+ with
+ Relaxed_Initialization => Target,
+ Pre => (if Trim_Nul then
+ Is_Nul_Terminated (Item)
+ and then C_Length_Ghost (Item) <= size_t (Target'Length)
+ else
+ Item'Last - Item'First < size_t (Target'Length)),
+ Post => Count =
+ (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
+ and then
+ (if Count /= 0 then
+ Target (Target'First .. Target'First + (Count - 1))'Initialized)
+ and then
+ (for all J in Target'First .. Target'First + (Count - 1) =>
+ Target (J) =
+ To_Ada (Item (size_t (J - Target'First) + Item'First)));
+ -- For procedure To_Ada, each element of Item (if Trim_Nul is False) or
+ -- each element of Item preceding the first nul (if Trim_Nul is True) is
+ -- converted (via the To_Ada function) to a Character, which is assigned
+ -- to the corresponding element of Target. Count is set to the number of
+ -- Target elements assigned. If Target is not long enough, Constraint_Error
+ -- is propagated. If Trim_Nul is True and Item does not contain nul, then
+ -- Terminator_Error is propagated.
------------------------------------
-- Wide Character and Wide String --
wide_nul : constant wchar_t := wchar_t'First;
- function To_C (Item : Wide_Character) return wchar_t;
- function To_Ada (Item : wchar_t) return Wide_Character;
+ -- To_C and To_Ada provide the mappings between the Ada and C wide
+ -- character types.
+
+ function To_C (Item : Wide_Character) return wchar_t
+ with
+ Post => To_C'Result = wchar_t (Item);
+
+ function To_Ada (Item : wchar_t) return Wide_Character
+ with
+ Post => To_Ada'Result = Wide_Character (Item);
type wchar_array is array (size_t range <>) of aliased wchar_t;
- function Is_Nul_Terminated (Item : wchar_array) return Boolean;
+ function Is_Nul_Terminated (Item : wchar_array) return Boolean
+ with
+ Post => Is_Nul_Terminated'Result = (for some C of Item => C = wide_nul);
+ -- The result of Is_Nul_Terminated is True if Item contains wide_nul, and
+ -- is False otherwise.
+
+ -- The To_C and To_Ada subprograms that convert between Wide_String and
+ -- wchar_array have analogous effects to the To_C and To_Ada subprograms
+ -- that convert between String and char_array, except that wide_nul is
+ -- used instead of nul.
+
+ function C_Length_Ghost (Item : wchar_array) return size_t
+ with
+ Ghost,
+ Pre => Is_Nul_Terminated (Item),
+ Post => C_Length_Ghost'Result <= Item'Last - Item'First
+ and then Item (Item'First + C_Length_Ghost'Result) = wide_nul
+ and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
+ when J /= Item'First + C_Length_Ghost'Result =>
+ Item (J) /= wide_nul);
+ -- Ghost function to compute the length of a wchar_array up to the first
+ -- wide_nul character.
function To_C
(Item : Wide_String;
- Append_Nul : Boolean := True) return wchar_array;
+ Append_Nul : Boolean := True) return wchar_array
+ with
+ Pre => not (Append_Nul = False and then Item'Length = 0),
+ Post => To_C'Result'First = 0
+ and then To_C'Result'Length =
+ (if Append_Nul then Item'Length + 1 else Item'Length)
+ and then (for all J in Item'Range =>
+ To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
+ and then (if Append_Nul then To_C'Result (To_C'Result'Last) = wide_nul);
function To_Ada
(Item : wchar_array;
- Trim_Nul : Boolean := True) return Wide_String;
+ Trim_Nul : Boolean := True) return Wide_String
+ with
+ Pre => (if Trim_Nul then
+ Is_Nul_Terminated (Item)
+ and then C_Length_Ghost (Item) <= size_t (Natural'Last)
+ else
+ Item'Last - Item'First < size_t (Natural'Last)),
+ Post => To_Ada'Result'First = 1
+ and then To_Ada'Result'Length =
+ (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
+ and then (for all J in To_Ada'Result'Range =>
+ To_Ada'Result (J) =
+ To_Ada (Item (size_t (J) - 1 + Item'First)));
procedure To_C
(Item : Wide_String;
Target : out wchar_array;
Count : out size_t;
- Append_Nul : Boolean := True);
+ Append_Nul : Boolean := True)
+ with
+ Relaxed_Initialization => Target,
+ Pre => Target'Length >=
+ (if Append_Nul then Item'Length + 1 else Item'Length),
+ Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
+ and then
+ (if Count /= 0 then
+ Target (Target'First .. Target'First + (Count - 1))'Initialized)
+ and then
+ (for all J in Item'Range =>
+ Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
+ and then
+ (if Append_Nul then Target (Target'First + (Count - 1)) = wide_nul);
procedure To_Ada
(Item : wchar_array;
Target : out Wide_String;
Count : out Natural;
- Trim_Nul : Boolean := True);
+ Trim_Nul : Boolean := True)
+ with
+ Relaxed_Initialization => Target,
+ Pre => (if Trim_Nul then
+ Is_Nul_Terminated (Item)
+ and then C_Length_Ghost (Item) <= size_t (Target'Length)
+ else
+ Item'Last - Item'First < size_t (Target'Length)),
+ Post => Count =
+ (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
+ and then
+ (if Count /= 0 then
+ Target (Target'First .. Target'First + (Count - 1))'Initialized)
+ and then
+ (for all J in Target'First .. Target'First + (Count - 1) =>
+ Target (J) =
+ To_Ada (Item (size_t (J - Target'First) + Item'First)));
Terminator_Error : exception;
char16_nul : constant char16_t := char16_t'Val (0);
pragma Ada_05 (char16_nul);
- function To_C (Item : Wide_Character) return char16_t;
+ -- To_C and To_Ada provide mappings between the Ada and C 16-bit character
+ -- types.
+
+ function To_C (Item : Wide_Character) return char16_t
+ with
+ Post => To_C'Result = char16_t (Item);
pragma Ada_05 (To_C);
- function To_Ada (Item : char16_t) return Wide_Character;
+ function To_Ada (Item : char16_t) return Wide_Character
+ with
+ Post => To_Ada'Result = Wide_Character (Item);
pragma Ada_05 (To_Ada);
type char16_array is array (size_t range <>) of aliased char16_t;
pragma Ada_05 (char16_array);
- function Is_Nul_Terminated (Item : char16_array) return Boolean;
+ function Is_Nul_Terminated (Item : char16_array) return Boolean
+ with
+ Post => Is_Nul_Terminated'Result = (for some C of Item => C = char16_nul);
pragma Ada_05 (Is_Nul_Terminated);
+ -- The result of Is_Nul_Terminated is True if Item contains char16_nul, and
+ -- is False otherwise.
+
+ -- The To_C and To_Ada subprograms that convert between Wide_String and
+ -- char16_array have analogous effects to the To_C and To_Ada subprograms
+ -- that convert between String and char_array, except that char16_nul is
+ -- used instead of nul.
+
+ function C_Length_Ghost (Item : char16_array) return size_t
+ with
+ Ghost,
+ Pre => Is_Nul_Terminated (Item),
+ Post => C_Length_Ghost'Result <= Item'Last - Item'First
+ and then Item (Item'First + C_Length_Ghost'Result) = char16_nul
+ and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
+ when J /= Item'First + C_Length_Ghost'Result =>
+ Item (J) /= char16_nul);
+ -- Ghost function to compute the length of a char16_array up to the first
+ -- char16_nul character.
function To_C
(Item : Wide_String;
- Append_Nul : Boolean := True) return char16_array;
+ Append_Nul : Boolean := True) return char16_array
+ with
+ Pre => not (Append_Nul = False and then Item'Length = 0),
+ Post => To_C'Result'First = 0
+ and then To_C'Result'Length =
+ (if Append_Nul then Item'Length + 1 else Item'Length)
+ and then (for all J in Item'Range =>
+ To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
+ and then
+ (if Append_Nul then To_C'Result (To_C'Result'Last) = char16_nul);
pragma Ada_05 (To_C);
function To_Ada
(Item : char16_array;
- Trim_Nul : Boolean := True) return Wide_String;
+ Trim_Nul : Boolean := True) return Wide_String
+ with
+ Pre => (if Trim_Nul then
+ Is_Nul_Terminated (Item)
+ and then C_Length_Ghost (Item) <= size_t (Natural'Last)
+ else
+ Item'Last - Item'First < size_t (Natural'Last)),
+ Post => To_Ada'Result'First = 1
+ and then To_Ada'Result'Length =
+ (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
+ and then (for all J in To_Ada'Result'Range =>
+ To_Ada'Result (J) =
+ To_Ada (Item (size_t (J) - 1 + Item'First)));
pragma Ada_05 (To_Ada);
procedure To_C
(Item : Wide_String;
Target : out char16_array;
Count : out size_t;
- Append_Nul : Boolean := True);
+ Append_Nul : Boolean := True)
+ with
+ Relaxed_Initialization => Target,
+ Pre => Target'Length >=
+ (if Append_Nul then Item'Length + 1 else Item'Length),
+ Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
+ and then
+ (if Count /= 0 then
+ Target (Target'First .. Target'First + (Count - 1))'Initialized)
+ and then
+ (for all J in Item'Range =>
+ Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
+ and then
+ (if Append_Nul then Target (Target'First + (Count - 1)) = char16_nul);
pragma Ada_05 (To_C);
procedure To_Ada
(Item : char16_array;
Target : out Wide_String;
Count : out Natural;
- Trim_Nul : Boolean := True);
+ Trim_Nul : Boolean := True)
+ with
+ Relaxed_Initialization => Target,
+ Pre => (if Trim_Nul then
+ Is_Nul_Terminated (Item)
+ and then C_Length_Ghost (Item) <= size_t (Target'Length)
+ else
+ Item'Last - Item'First < size_t (Target'Length)),
+ Post => Count =
+ (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
+ and then
+ (if Count /= 0 then
+ Target (Target'First .. Target'First + (Count - 1))'Initialized)
+ and then
+ (for all J in Target'First .. Target'First + (Count - 1) =>
+ Target (J) =
+ To_Ada (Item (size_t (J - Target'First) + Item'First)));
pragma Ada_05 (To_Ada);
type char32_t is new Wide_Wide_Character;
char32_nul : constant char32_t := char32_t'Val (0);
pragma Ada_05 (char32_nul);
- function To_C (Item : Wide_Wide_Character) return char32_t;
+ -- To_C and To_Ada provide mappings between the Ada and C 32-bit character
+ -- types.
+
+ function To_C (Item : Wide_Wide_Character) return char32_t
+ with
+ Post => To_C'Result = char32_t (Item);
pragma Ada_05 (To_C);
- function To_Ada (Item : char32_t) return Wide_Wide_Character;
+ function To_Ada (Item : char32_t) return Wide_Wide_Character
+ with
+ Post => To_Ada'Result = Wide_Wide_Character (Item);
pragma Ada_05 (To_Ada);
type char32_array is array (size_t range <>) of aliased char32_t;
pragma Ada_05 (char32_array);
- function Is_Nul_Terminated (Item : char32_array) return Boolean;
+ function Is_Nul_Terminated (Item : char32_array) return Boolean
+ with
+ Post => Is_Nul_Terminated'Result = (for some C of Item => C = char32_nul);
pragma Ada_05 (Is_Nul_Terminated);
+ -- The result of Is_Nul_Terminated is True if Item contains char32_nul, and
+ -- is False otherwise.
+
+ function C_Length_Ghost (Item : char32_array) return size_t
+ with
+ Ghost,
+ Pre => Is_Nul_Terminated (Item),
+ Post => C_Length_Ghost'Result <= Item'Last - Item'First
+ and then Item (Item'First + C_Length_Ghost'Result) = char32_nul
+ and then (for all J in Item'First .. Item'First + C_Length_Ghost'Result
+ when J /= Item'First + C_Length_Ghost'Result =>
+ Item (J) /= char32_nul);
+ -- Ghost function to compute the length of a char32_array up to the first
+ -- char32_nul character.
+
+ -- The To_C and To_Ada subprograms that convert between Wide_Wide_String
+ -- and char32_array have analogous effects to the To_C and To_Ada
+ -- subprograms that convert between String and char_array, except
+ -- that char32_nul is used instead of nul.
function To_C
(Item : Wide_Wide_String;
- Append_Nul : Boolean := True) return char32_array;
+ Append_Nul : Boolean := True) return char32_array
+ with
+ Pre => not (Append_Nul = False and then Item'Length = 0),
+ Post => To_C'Result'First = 0
+ and then To_C'Result'Length =
+ (if Append_Nul then Item'Length + 1 else Item'Length)
+ and then (for all J in Item'Range =>
+ To_C'Result (size_t (J - Item'First)) = To_C (Item (J)))
+ and then
+ (if Append_Nul then To_C'Result (To_C'Result'Last) = char32_nul);
pragma Ada_05 (To_C);
function To_Ada
(Item : char32_array;
- Trim_Nul : Boolean := True) return Wide_Wide_String;
+ Trim_Nul : Boolean := True) return Wide_Wide_String
+ with
+ Pre => (if Trim_Nul then
+ Is_Nul_Terminated (Item)
+ and then C_Length_Ghost (Item) <= size_t (Natural'Last)
+ else
+ Item'Last - Item'First < size_t (Natural'Last)),
+ Post => To_Ada'Result'First = 1
+ and then To_Ada'Result'Length =
+ (if Trim_Nul then C_Length_Ghost (Item) else Item'Length)
+ and then (for all J in To_Ada'Result'Range =>
+ To_Ada'Result (J) =
+ To_Ada (Item (size_t (J) - 1 + Item'First)));
pragma Ada_05 (To_Ada);
procedure To_C
(Item : Wide_Wide_String;
Target : out char32_array;
Count : out size_t;
- Append_Nul : Boolean := True);
+ Append_Nul : Boolean := True)
+ with
+ Relaxed_Initialization => Target,
+ Pre => Target'Length >=
+ (if Append_Nul then Item'Length + 1 else Item'Length),
+ Post => Count = (if Append_Nul then Item'Length + 1 else Item'Length)
+ and then
+ (if Count /= 0 then
+ Target (Target'First .. Target'First + (Count - 1))'Initialized)
+ and then
+ (for all J in Item'Range =>
+ Target (Target'First + size_t (J - Item'First)) = To_C (Item (J)))
+ and then
+ (if Append_Nul then Target (Target'First + (Count - 1)) = char32_nul);
pragma Ada_05 (To_C);
procedure To_Ada
(Item : char32_array;
Target : out Wide_Wide_String;
Count : out Natural;
- Trim_Nul : Boolean := True);
+ Trim_Nul : Boolean := True)
+ with
+ Relaxed_Initialization => Target,
+ Pre => (if Trim_Nul then
+ Is_Nul_Terminated (Item)
+ and then C_Length_Ghost (Item) <= size_t (Target'Length)
+ else
+ Item'Last - Item'First < size_t (Target'Length)),
+ Post => Count =
+ (if Trim_Nul then Natural (C_Length_Ghost (Item)) else Item'Length)
+ and then
+ (if Count /= 0 then
+ Target (Target'First .. Target'First + (Count - 1))'Initialized)
+ and then
+ (for all J in Target'First .. Target'First + (Count - 1) =>
+ Target (J) =
+ To_Ada (Item (size_t (J - Target'First) + Item'First)));
pragma Ada_05 (To_Ada);
end Interfaces.C;
projects / thirdparty / gcc.git / commitdiff
