Code cleanup.
authorArnaud Charlet <charlet@gcc.gnu.org>
Thu, 19 Jan 2017 13:14:04 +0000 (14:14 +0100)
committerArnaud Charlet <charlet@gcc.gnu.org>
Thu, 19 Jan 2017 13:14:04 +0000 (14:14 +0100)
From-SVN: r244634

gcc/ada/contracts.adb

index d5b31034f6d54ed1dc8a4d4ce2aaca572032df7b..d467c942e13584a37616a9226ec5dd2a6ad415df 100644 (file)
@@ -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);