Skip to content
Snippets Groups Projects
Commit 41d7d32c authored by Piotr Trojanek's avatar Piotr Trojanek Committed by Marc Poulhiès
Browse files

ada: Extend precondition of Interfaces.C.String.Value with Length

The existing precondition guarded against exception Dereference_Error,
but not against Constraint_Error.

The RM rule B.3.1(36/3) only mentions Constraint_Error for the Value
function which returns char_array, but the one which returns String
has the same restriction, because it is equivalent to calling the
variant which returns char_array and then converted.

gcc/ada/

	* libgnat/i-cstrin.ads (Value): Extend preconditions; adapt comment for
	the package.
parent 43057533
No related branches found
No related tags found
No related merge requests found
...@@ -36,8 +36,8 @@ ...@@ -36,8 +36,8 @@
-- Preconditions in this unit are meant for analysis only, not for run-time -- 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 -- checking, so that the expected exceptions are raised. This is enforced by
-- setting the corresponding assertion policy to Ignore. These preconditions -- setting the corresponding assertion policy to Ignore. These preconditions
-- protect from Dereference_Error and Update_Error, but not from -- protect from Constraint_Error, Dereference_Error and Update_Error, but not
-- Storage_Error. -- from Storage_Error.
pragma Assertion_Policy (Pre => Ignore); pragma Assertion_Policy (Pre => Ignore);
...@@ -95,7 +95,7 @@ is ...@@ -95,7 +95,7 @@ is
(Item : chars_ptr; (Item : chars_ptr;
Length : size_t) return char_array Length : size_t) return char_array
with with
Pre => Item /= Null_Ptr, Pre => Item /= Null_Ptr and then Length /= 0,
Global => (Input => C_Memory); Global => (Input => C_Memory);
function Value (Item : chars_ptr) return String with function Value (Item : chars_ptr) return String with
...@@ -106,7 +106,7 @@ is ...@@ -106,7 +106,7 @@ is
(Item : chars_ptr; (Item : chars_ptr;
Length : size_t) return String Length : size_t) return String
with with
Pre => Item /= Null_Ptr, Pre => Item /= Null_Ptr and then Length /= 0,
Global => (Input => C_Memory); Global => (Input => C_Memory);
function Strlen (Item : chars_ptr) return size_t with function Strlen (Item : chars_ptr) return size_t with
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment