From 332429c807f56de7948885368277723a7a5ac0ac Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 19 Jan 2017 14:14:04 +0100 Subject: [PATCH] Code cleanup. From-SVN: r244634 --- gcc/ada/contracts.adb | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index d5b31034f6d..d467c942e13 100644 --- a/gcc/ada/contracts.adb +++ b/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); -- 2.30.2