[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 --git a/gcc/ada/libgnat/i-cstrin.adb b/gcc/ada/libgnat/i-cstrin.adb
index e2f0f2192a6cbd8eee23d398f3077675568ca203..67cceb277fa7c0c6dfd1ef80dcb3b9a9aa97fdff 100644 (file)
--- 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 5c1b259ca8f5c66d920ee5ff83ca8fd3adf56dac..62ef9df383da2cc917083cf7844ae7dcbbb6ed8d 100644 (file)
--- 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;