[Ada] Add contracts to Interfaces.C.Strings
Commit Message
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.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
@@ -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,
@@ -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;