commit 1647bc2a78b2182007f011ff0a43f872086ee512
author Pierre-Alexandre Bazin <bazin@adacore.com> Fri Jul 02 15:43:44 2021 +0200
committer Pierre-Marie de Rodat <derodat@adacore.com> Wed Sep 22 15:01:48 2021 +0000
tree 670c2c96daf0797b252ea5787c729194d78a676a
parent 5f325f5e6fd091f73f5be6ef30d27e22e4b59a74

[Ada] Contracts written for the Ada.Strings.Bounded library

gcc/ada/

	* libgnat/a-strbou.adb: Turn SPARK_Mode on.
	* libgnat/a-strbou.ads: Write contracts.
	* libgnat/a-strfix.ads (Index): Fix grammar error in a comment.
	* libgnat/a-strsea.ads (Index): Likewise.
	* libgnat/a-strsup.adb: Rewrite the body to take into account
	the new definition of Super_String using Relaxed_Initialization
	and a predicate.
	(Super_Replicate, Super_Translate, Times): Added loop
	invariants, and ghost lemmas for Super_Replicate and Times.
	(Super_Trim): Rewrite the body using search functions to
	determine the cutting points.
	(Super_Element, Super_Length, Super_Slice, Super_To_String):
	Remove (now written as expression functions in a-strsup.ads).
	* libgnat/a-strsup.ads: Added contracts.
	(Super_Element, Super_Length, Super_Slice, Super_To_String):
	Rewrite as expression functions.