[COMMITTED] ada: Remove dependency on System.Val_Bool in System.Img_Bool
Checks
Commit Message
From: Yannick Moy <moy@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(-)
@@ -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
@@ -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.
@@ -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
@@ -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' | '_')