Code cleanup.

From-SVN: r244634

gcc/ada/contracts.adb

@@ -484,10 +484,13 @@ package body Contracts is
       --  volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
       --  check is relevant only when SPARK_Mode is on, as it is not a standard
       --  legality rule. The check is performed here because Volatile_Function
-      --  is processed after the analysis of the related subprogram body.
+      --  is processed after the analysis of the related subprogram body. The
+      --  check only applies to source subprograms and not to generated TSS
+      --  subprograms.
 
       if SPARK_Mode = On
         and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
+        and then Comes_From_Source (Spec_Id)
         and then not Is_Volatile_Function (Body_Id)
       then
          Check_Nonvolatile_Function_Profile (Body_Id);