-- 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);