[gcc r13-928] [Ada] Add contracts to Interfaces.C.Strings

[gcc r13-928] [Ada] Add contracts to Interfaces.C.Strings

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:f0b7fddbefbe7af7c14ed5f2def49bbdb4a6c919

commit r13-928-gf0b7fddbefbe7af7c14ed5f2def49bbdb4a6c919
Author: Joffrey Huguet <huguet@adacore.com>
Date:   Tue May 3 14:46:35 2022 +0200

    [Ada] Add contracts to Interfaces.C.Strings
    
    This patch adds Global contracts and preconditions to subprograms of
    Interfaces.C.Strings. Effects on allocated memory are modelled
    through an abstract state, C_Memory. The preconditions protect against
    Dereference_Error, but not Storage_Error (which is not handled by
    SPARK). This patch also disables the use of To_Chars_Ptr, which
    creates an alias between an ownership pointer and the abstract state,
    and the use of Free, in SPARK code. Thus, memory leaks will happen
    if the user creates the Chars_Ptr using New_Char_Array and New_String.
    
    gcc/ada/
    
            * libgnat/i-cstrin.ads (To_Chars_Ptr): Add SPARK_Mode => Off.
            (Free): Likewise.
            (New_Char_Array): Add global contracts and Volatile attribute.
            (New_String): Likewise.
            (Value, Strlen, Update): Add global contracts and preconditions.
            * libgnat/i-cstrin.adb: Add SPARK_Mode => Off to the package
            body.

Diff:
---
 gcc/ada/libgnat/i-cstrin.adb |  4 ++-
 gcc/ada/libgnat/i-cstrin.ads | 69 ++++++++++++++++++++++++++++++++++----------
 2 files changed, 57 insertions(+), 16 deletions(-)

diff --git a/gcc/ada/libgnat/i-cstrin.adb b/gcc/ada/libgnat/i-cstrin.adb
index e2f0f2192a6..67cceb277fa 100644
--- a/gcc/ada/libgnat/i-cstrin.adb
+++ b/gcc/ada/libgnat/i-cstrin.adb
@@ -34,7 +34,9 @@ with System.Storage_Elements; use System.Storage_Elements;
 
 with Ada.Unchecked_Conversion;
 
-package body Interfaces.C.Strings is
+package body Interfaces.C.Strings with
+  SPARK_Mode => Off
+is
 
    --  Note that the type chars_ptr has a pragma No_Strict_Aliasing in the
    --  spec, to prevent any assumptions about aliasing for values of this type,
diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads
index 5c1b259ca8f..62ef9df383d 100644
--- a/gcc/ada/libgnat/i-cstrin.ads
+++ b/gcc/ada/libgnat/i-cstrin.ads
@@ -33,7 +33,18 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package Interfaces.C.Strings is
+--  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. These preconditions
+--  do not protect against Storage_Error.
+
+pragma Assertion_Policy (Pre => Ignore);
+
+package Interfaces.C.Strings with
+  SPARK_Mode     => On,
+  Abstract_State => (C_Memory),
+  Initializes    => (C_Memory)
+is
    pragma Preelaborate;
 
    type char_array_access is access all char_array;
@@ -53,47 +64,75 @@ package Interfaces.C.Strings is
 
    function To_Chars_Ptr
      (Item      : char_array_access;
-      Nul_Check : Boolean := False) return chars_ptr;
-
-   function New_Char_Array (Chars : char_array) return chars_ptr;
-
-   function New_String (Str : String) return chars_ptr;
-
-   procedure Free (Item : in out chars_ptr);
+      Nul_Check : Boolean := False) return chars_ptr
+   with
+     SPARK_Mode => Off;
+
+   function New_Char_Array (Chars : char_array) return chars_ptr with
+     Volatile_Function,
+     Post   => New_Char_Array'Result /= Null_Ptr,
+     Global => (Input => C_Memory);
+
+   function New_String (Str : String) return chars_ptr with
+     Volatile_Function,
+     Post   => New_String'Result /= Null_Ptr,
+     Global => (Input => C_Memory);
+
+   procedure Free (Item : in out chars_ptr) with
+     SPARK_Mode => Off;
    --  When deallocation is prohibited (eg: cert runtimes) this routine
    --  will raise Program_Error
 
    Dereference_Error : exception;
 
-   function Value (Item : chars_ptr) return char_array;
+   function Value (Item : chars_ptr) return char_array with
+     Pre    => Item /= Null_Ptr,
+     Global => (Input => C_Memory);
 
    function Value
      (Item   : chars_ptr;
-      Length : size_t) return char_array;
+      Length : size_t) return char_array
+   with
+     Pre    => Item /= Null_Ptr,
+     Global => (Input => C_Memory);
 
-   function Value (Item : chars_ptr) return String;
+   function Value (Item : chars_ptr) return String with
+     Pre    => Item /= Null_Ptr,
+     Global => (Input => C_Memory);
 
    function Value
      (Item   : chars_ptr;
-      Length : size_t) return String;
+      Length : size_t) return String
+   with
+     Pre    => Item /= Null_Ptr,
+     Global => (Input => C_Memory);
 
-   function Strlen (Item : chars_ptr) return size_t;
+   function Strlen (Item : chars_ptr) return size_t with
+     Pre    => Item /= Null_Ptr,
+     Global => (Input => C_Memory);
 
    procedure Update
      (Item   : chars_ptr;
       Offset : size_t;
       Chars  : char_array;
-      Check  : Boolean := True);
+      Check  : Boolean := True)
+   with
+     Pre    => Item /= Null_Ptr,
+     Global => (In_Out => C_Memory);
 
    procedure Update
      (Item   : chars_ptr;
       Offset : size_t;
       Str    : String;
-      Check  : Boolean := True);
+      Check  : Boolean := True)
+   with
+     Pre    => Item /= Null_Ptr,
+     Global => (In_Out => C_Memory);
 
    Update_Error : exception;
 
 private
+   pragma SPARK_Mode (Off);
    type chars_ptr is access all Character;
    for chars_ptr'Size use System.Parameters.ptr_bits;