ada: Remove GNATcheck violations

Remove GNATcheck violations by refactoring code and also using
pragma Annotate to exempt them.

gcc/ada/

	* libgnat/a-comlin.adb (Argument_Count): Rewrite code so there is
	only one return, to remove Improper_Returns violation.
	(Command_Name): Add pragma to exempt Improper_Returns violation.

• [DBH] gcc/ada/libgnat/a-comlin.adb

ada: Remove GNATcheck violations

Remove GNATcheck violations by refactoring code and also using
pragma Annotate to exempt them.

gcc/ada/

	* libgnat/i-cstrin.adb (Free): Rewrite code so there is only one
	return, to remove Improper_Returns violation.
	(Position_Of_Nul): Add pragma to exempt Improper_Returns
	violation.
	(To_Chars_Ptr): Likewise.
	(Value): Likewise

• [DBH] gcc/ada/libgnat/i-cstrin.adb

ada: Add pragma Annotate for GNATcheck exemptions

Exempt the GNATcheck rule "Unassigned_OUT_Parameters"
with the rationale "the OUT parameter is assigned by component".

gcc/ada/

	* libgnat/s-imguti.adb (Set_Decimal_Digits): Add pragma to exempt
	Unassigned_OUT_Parameters.
	(Set_Floating_Invalid_Value): Likewise

• [DBH] gcc/ada/libgnat/s-imguti.adb

ada: Refactor code to remove GNATcheck violation

Rewrite for loop containing an exit (which violates GNATcheck
rule Exits_From_Conditional_Loops), to use a while loop
which contains the exit criteria in its condition.
Also, move special case of first time through loop, to come
before loop.

gcc/ada/

	* libgnat/s-imagef.adb (Set_Image_Fixed): Refactor loop.

• [DBH] gcc/ada/libgnat/s-imagef.adb

ada: Remove GNATcheck violations

Use pragma Annotate to exempt GNATcheck violations that are related
to proof code. Specifically, exempt rules "Metrics_LSLOC" and
"Metrics_Cyclomatic_Complexity" whose limits are exceeded due to
proof code, and exempt rule "Discriminated_Records" for a variant record
that is only used in proof code.

gcc/ada/

	* libgnat/s-aridou.adb: Add pragma to exempt Metrics_LSLOC.
	(Double_Divide): Add pragma to exempt
	Metrics_Cyclomatic_Complexity.
	(Scaled_Divide): Likewise.
	* libgnat/s-vauspe.ads (Uns_Option): Add pragma to exempt
	Discriminated_Records.

• [DBH] gcc/ada/libgnat/s-aridou.adb
• [DBH] gcc/ada/libgnat/s-vauspe.ads