diff options
author | Yannick Moy <moy@adacore.com> | 2023-11-03 14:49:30 +0100 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-11-28 10:35:47 +0100 |
commit | 73ecd592c9a8a99cf5d456d9a78d3c793390af1e (patch) | |
tree | 08dfb62fea7105f7156593376c8f93f17de80027 | |
parent | 834f2973606c63b4cd9e27e3bf24f01ee1347568 (diff) | |
download | gcc-73ecd592c9a8a99cf5d456d9a78d3c793390af1e.zip gcc-73ecd592c9a8a99cf5d456d9a78d3c793390af1e.tar.gz gcc-73ecd592c9a8a99cf5d456d9a78d3c793390af1e.tar.bz2 |
ada: Remove dependency on System.Val_Bool in System.Img_Bool
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.
-rw-r--r-- | gcc/ada/libgnat/s-imgboo.adb | 2 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-imgboo.ads | 5 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-valboo.ads | 34 | ||||
-rw-r--r-- | 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 fb3301a..9a6340f 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 d40c086..92cc7c3 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 d482199..6cdc3e5 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 dd861e5..6f0ca53 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' | '_') |