ada: Remove GNATcheck violations

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.