ada: Update annotations in runtime for proof

With bump of stable SPARK used for proof of the runtime,
some annotations need to change.

gcc/ada/

	* libgnat/s-aridou.adb (Scaled_Divide): Add assertions.
	* libgnat/s-valuti.adb: Add Loop_Variant.
	* libgnat/s-valuti.ads: Add Exceptional_Cases on No_Return
	procedure.

1 files changed, 2 insertions, 0 deletions

diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb
index ec6fdb0..ee37c1a 100644
--- a/gcc/ada/libgnat/s-valuti.adb
+++ b/gcc/ada/libgnat/s-valuti.adb
@@ -123,6 +123,7 @@ is
       while F < L and then S (F) = ' ' loop
          pragma Loop_Invariant (F in S'First .. L - 1);
          pragma Loop_Invariant (for all J in S'First .. F => S (J) = ' ');
+         pragma Loop_Variant (Increases => F);
          F := F + 1;
       end loop;
 
@@ -139,6 +140,7 @@ is
       while S (L) = ' ' loop
          pragma Loop_Invariant (L in F + 1 .. S'Last);
          pragma Loop_Invariant (for all J in L .. S'Last => S (J) = ' ');
+         pragma Loop_Variant (Decreases => L);
          L := L - 1;
       end loop;