From: Yannick Moy <m...@adacore.com> In order to facilitate the certification of System.Img_Bool, remove its dependency on unit System.Val_Bool. Modify the definition of ghost function Is_Boolean_Image_Ghost to take the expected boolean value and move it to System.Val_Spec.
gcc/ada/ * libgnat/s-imgboo.adb: Remove with_clause now in spec file. * libgnat/s-imgboo.ads: Remove dependency on System.Val_Bool. (Image_Boolean): Replace call to Value_Boolean by passing value V to updated ghost function Is_Boolean_Image_Ghost. * libgnat/s-valboo.ads (Is_Boolean_Image_Ghost): Move to other unit. (Value_Boolean.): Update precondition. * libgnat/s-valspe.ads (Is_Boolean_Image_Ghost): Move here. Add new parameter for expected boolean value. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/s-imgboo.adb | 2 -- gcc/ada/libgnat/s-imgboo.ads | 5 ++--- gcc/ada/libgnat/s-valboo.ads | 34 ++-------------------------------- gcc/ada/libgnat/s-valspe.ads | 36 ++++++++++++++++++++++++++++++++++++ 4 files changed, 40 insertions(+), 37 deletions(-) diff --git a/gcc/ada/libgnat/s-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb index fb3301a4270..9a6340fc010 100644 --- a/gcc/ada/libgnat/s-imgboo.adb +++ b/gcc/ada/libgnat/s-imgboo.adb @@ -37,8 +37,6 @@ pragma Assertion_Policy (Ghost => Ignore, Loop_Invariant => Ignore, Assert => Ignore); -with System.Val_Spec; - package body System.Img_Bool with SPARK_Mode is diff --git a/gcc/ada/libgnat/s-imgboo.ads b/gcc/ada/libgnat/s-imgboo.ads index d40c0860fac..92cc7c31b57 100644 --- a/gcc/ada/libgnat/s-imgboo.ads +++ b/gcc/ada/libgnat/s-imgboo.ads @@ -42,7 +42,7 @@ pragma Assertion_Policy (Pre => Ignore, Contract_Cases => Ignore, Ghost => Ignore); -with System.Val_Bool; +with System.Val_Spec; package System.Img_Bool with SPARK_Mode, Preelaborate @@ -56,8 +56,7 @@ is Pre => S'First = 1 and then (if V then S'Length >= 4 else S'Length >= 5), Post => (if V then P = 4 else P = 5) - and then System.Val_Bool.Is_Boolean_Image_Ghost (S (1 .. P)) - and then System.Val_Bool.Value_Boolean (S (1 .. P)) = V; + and then System.Val_Spec.Is_Boolean_Image_Ghost (S (1 .. P), V); -- Computes Boolean'Image (V) and stores the result in S (1 .. P) -- setting the resulting value of P. The caller guarantees that S -- is long enough to hold the result, and that S'First is 1. diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads index d48219953a0..6cdc3e559fe 100644 --- a/gcc/ada/libgnat/s-valboo.ads +++ b/gcc/ada/libgnat/s-valboo.ads @@ -47,40 +47,10 @@ package System.Val_Bool is pragma Preelaborate; - function Is_Boolean_Image_Ghost (Str : String) return Boolean is - (not System.Val_Spec.Only_Space_Ghost (Str, Str'First, Str'Last) - and then - (declare - F : constant Positive := System.Val_Spec.First_Non_Space_Ghost - (Str, Str'First, Str'Last); - begin - (F <= Str'Last - 3 - and then Str (F) in 't' | 'T' - and then Str (F + 1) in 'r' | 'R' - and then Str (F + 2) in 'u' | 'U' - and then Str (F + 3) in 'e' | 'E' - and then - (if F + 3 < Str'Last then - System.Val_Spec.Only_Space_Ghost (Str, F + 4, Str'Last))) - or else - (F <= Str'Last - 4 - and then Str (F) in 'f' | 'F' - and then Str (F + 1) in 'a' | 'A' - and then Str (F + 2) in 'l' | 'L' - and then Str (F + 3) in 's' | 'S' - and then Str (F + 4) in 'e' | 'E' - and then - (if F + 4 < Str'Last then - System.Val_Spec.Only_Space_Ghost (Str, F + 5, Str'Last))))) - with - Ghost; - -- Ghost function that returns True iff Str is the image of a boolean, that - -- is "true" or "false" in any capitalization, possibly surounded by space - -- characters. - function Value_Boolean (Str : String) return Boolean with - Pre => Is_Boolean_Image_Ghost (Str), + Pre => System.Val_Spec.Is_Boolean_Image_Ghost (Str, True) + or else System.Val_Spec.Is_Boolean_Image_Ghost (Str, False), Post => Value_Boolean'Result = (Str (System.Val_Spec.First_Non_Space_Ghost diff --git a/gcc/ada/libgnat/s-valspe.ads b/gcc/ada/libgnat/s-valspe.ads index dd861e5029f..6f0ca5317ff 100644 --- a/gcc/ada/libgnat/s-valspe.ads +++ b/gcc/ada/libgnat/s-valspe.ads @@ -72,6 +72,42 @@ is -- Ghost function that returns the index of the first non-space character -- in S, which necessarily exists given the precondition on S. + function Is_Boolean_Image_Ghost + (Str : String; + Val : Boolean) return Boolean + is + (not Only_Space_Ghost (Str, Str'First, Str'Last) + and then + (declare + F : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last); + begin + (Val + and then F <= Str'Last - 3 + and then Str (F) in 't' | 'T' + and then Str (F + 1) in 'r' | 'R' + and then Str (F + 2) in 'u' | 'U' + and then Str (F + 3) in 'e' | 'E' + and then + (if F + 3 < Str'Last then + Only_Space_Ghost (Str, F + 4, Str'Last))) + or else + (not Val + and then F <= Str'Last - 4 + and then Str (F) in 'f' | 'F' + and then Str (F + 1) in 'a' | 'A' + and then Str (F + 2) in 'l' | 'L' + and then Str (F + 3) in 's' | 'S' + and then Str (F + 4) in 'e' | 'E' + and then + (if F + 4 < Str'Last then + Only_Space_Ghost (Str, F + 5, Str'Last))))) + with + Ghost; + -- Ghost function that returns True iff Str is the image of boolean Val, + -- that is "true" or "false" in any capitalization, possibly surounded by + -- space characters. + function Only_Number_Ghost (Str : String; From, To : Integer) return Boolean is (for all J in From .. To => Str (J) in '0' .. '9' | '_') -- 2.42.0