diff options
author | Yannick Moy <moy@adacore.com> | 2021-11-15 21:36:34 +0100 |
---|---|---|
committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-12-02 16:26:20 +0000 |
commit | 76bbe3972ba78757abdb3bb06cccc0b461914b01 (patch) | |
tree | ebef10b159d8b7902a3e2129ae1d438b6d0b9b1a /gcc | |
parent | 7e650bf84bf61e88f05ffbf39ca677a1e3d2714a (diff) | |
download | gcc-76bbe3972ba78757abdb3bb06cccc0b461914b01.zip gcc-76bbe3972ba78757abdb3bb06cccc0b461914b01.tar.gz gcc-76bbe3972ba78757abdb3bb06cccc0b461914b01.tar.bz2 |
[Ada] Proof of Interfaces.C with SPARK
gcc/ada/
* libgnat/i-c.adb: Add ghost code.
(C_Length_Ghost): New ghost functions to query the C length of a
string.
(To_Ada): Insert constant Count_Cst where needed to comply with
SPARK. Homogeneize code between variants for char, wchar_t,
char16_t and char32_t. Use char16_nul and char32_nul
systematically instead of their value. Fix the type of index To
to be Integer instead of Positive, to avoid a possible range
check failure on an empty Target. Insert an exit statement to
avoid a possible overflow failure when the last index in Target
is Natural'Last (possibly on a small string as well).
* libgnat/i-c.ads: Add contracts.
(C_Length_Ghost): New ghost functions to query the C length of a
string.
* libgnat/s-os_lib.adb: Remove pragma Compiler_Unit_Warning
causing a spurious error during compilation of GNAT, as this
pragma is not needed anymore now that we bootstrap (stage1) with
the base compiler runtime.
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/libgnat/i-c.adb | 472 | ||||
-rw-r--r-- | gcc/ada/libgnat/i-c.ads | 420 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-os_lib.adb | 2 |
3 files changed, 825 insertions, 69 deletions
diff --git a/gcc/ada/libgnat/i-c.adb b/gcc/ada/libgnat/i-c.adb index 5be50ff..4ec920f 100644 --- a/gcc/ada/libgnat/i-c.adb +++ b/gcc/ada/libgnat/i-c.adb @@ -29,7 +29,77 @@ -- -- ------------------------------------------------------------------------------ -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 -- @@ -43,6 +113,9 @@ package body Interfaces.C is 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; @@ -56,6 +129,9 @@ package body Interfaces.C is 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; @@ -69,6 +145,9 @@ package body Interfaces.C is 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; @@ -82,6 +161,9 @@ package body Interfaces.C is 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; @@ -112,6 +194,13 @@ package body Interfaces.C is 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 @@ -121,6 +210,8 @@ package body Interfaces.C is end if; end loop; + pragma Assert (From = Item'First + C_Length_Ghost (Item)); + Count := Natural (From - Item'First); else @@ -128,11 +219,17 @@ package body Interfaces.C is 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; @@ -148,12 +245,19 @@ package body Interfaces.C is 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 @@ -178,11 +282,28 @@ package body Interfaces.C is 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 @@ -206,6 +327,13 @@ package body Interfaces.C is 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 @@ -215,6 +343,8 @@ package body Interfaces.C is end if; end loop; + pragma Assert (From = Item'First + C_Length_Ghost (Item)); + Count := Natural (From - Item'First); else @@ -222,11 +352,17 @@ package body Interfaces.C is 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; @@ -242,12 +378,19 @@ package body Interfaces.C is 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 @@ -272,6 +415,24 @@ package body Interfaces.C is 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; @@ -299,15 +460,24 @@ package body Interfaces.C is 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 @@ -315,11 +485,17 @@ package body Interfaces.C is 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; @@ -335,15 +511,22 @@ package body Interfaces.C is 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; @@ -365,6 +548,24 @@ package body Interfaces.C is 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; @@ -392,15 +593,24 @@ package body Interfaces.C is 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 @@ -408,11 +618,17 @@ package body Interfaces.C is 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; @@ -428,15 +644,22 @@ package body Interfaces.C is 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; @@ -458,6 +681,24 @@ package body Interfaces.C is 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; @@ -484,14 +725,26 @@ package body Interfaces.C is 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; @@ -512,11 +765,19 @@ package body Interfaces.C is 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; @@ -543,6 +804,19 @@ package body Interfaces.C is 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; @@ -576,14 +850,26 @@ package body Interfaces.C is 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; @@ -600,11 +886,19 @@ package body Interfaces.C is 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; @@ -631,9 +925,31 @@ package body Interfaces.C is 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; @@ -664,14 +980,26 @@ package body Interfaces.C is 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; @@ -688,11 +1016,19 @@ package body Interfaces.C is 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; @@ -719,14 +1055,36 @@ package body Interfaces.C is 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; @@ -752,14 +1110,26 @@ package body Interfaces.C is 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; @@ -775,11 +1145,19 @@ package body Interfaces.C is 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; @@ -806,14 +1184,36 @@ package body Interfaces.C is 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; diff --git a/gcc/ada/libgnat/i-c.ads b/gcc/ada/libgnat/i-c.ads index 428ea49..2023b75 100644 --- a/gcc/ada/libgnat/i-c.ads +++ b/gcc/ada/libgnat/i-c.ads @@ -13,10 +13,30 @@ -- -- ------------------------------------------------------------------------------ +-- 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> @@ -49,7 +69,11 @@ package Interfaces.C is 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 @@ -80,33 +104,133 @@ package Interfaces.C is 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 -- @@ -117,32 +241,110 @@ package Interfaces.C is 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; @@ -156,40 +358,118 @@ package Interfaces.C is 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; @@ -198,40 +478,118 @@ package Interfaces.C is 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; diff --git a/gcc/ada/libgnat/s-os_lib.adb b/gcc/ada/libgnat/s-os_lib.adb index 19f4cf7..7df06c4 100644 --- a/gcc/ada/libgnat/s-os_lib.adb +++ b/gcc/ada/libgnat/s-os_lib.adb @@ -29,8 +29,6 @@ -- -- ------------------------------------------------------------------------------ -pragma Compiler_Unit_Warning; - with Ada.Unchecked_Conversion; with Ada.Unchecked_Deallocation; with System; use System; |