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.

diff --git a/gcc/ada/libgnat/s-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb
index fb3301a4270832c8cb9b6ad1974ac28fb4a00902..9a6340fc0104dc7c6f1d141db9d1b52ac87963b0 100644 (file)
--- 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 d40c0860fac597cd77eb9d585d76716fdecab731..92cc7c31b572596a16cd56bfcb7e290bd368fac8 100644 (file)
--- 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 d48219953a0a8fec777ea6eda32b7d3b2de6a182..6cdc3e559fe9a6c93f49070457a62657c59a2784 100644 (file)
--- 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 dd861e5029f92d48652ad06678ba97427a7f46c7..6f0ca5317ff8794923441d91ce422aa5453f46f7 100644 (file)
--- 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' | '_')