[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.

0 files changed, 0 insertions, 0 deletions