This patch modifies the predicate which determines whether a function is volatile to correctly recognize a protected function.
------------ -- Source -- ------------ -- vol_func.ads package Vol_Func with SPARK_Mode is protected type Prot is end Prot; type Vol_Typ is null record with Volatile; function F (X : Prot) return Vol_Typ; function G return Vol_Typ; end Vol_Func; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c vol_func.ads vol_func.ads:7:16: nonvolatile function "F" cannot have a volatile parameter vol_func.ads:7:33: nonvolatile function "F" cannot have a volatile return type vol_func.ads:8:33: nonvolatile function "G" cannot have a volatile return type Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-18 Hristian Kirtchev <kirtc...@adacore.com> * sem_util.adb (Check_Nonvolatile_Function_Profile): Place the error message concerning the return type on the result definition. (Is_Volatile_Function): A function with a parameter of a protected type is a protected function if it is defined within a protected definition.
Index: sem_util.adb =================================================================== --- sem_util.adb (revision 230521) +++ sem_util.adb (working copy) @@ -3120,9 +3120,9 @@ -- Inspect the return type if Is_Effectively_Volatile (Etype (Func_Id)) then - Error_Msg_N + Error_Msg_NE ("nonvolatile function & cannot have a volatile return type", - Func_Id); + Result_Definition (Parent (Func_Id)), Func_Id); end if; end Check_Nonvolatile_Function_Profile; @@ -14010,6 +14010,7 @@ if Is_Primitive (Func_Id) and then Present (First_Formal (Func_Id)) and then Is_Protected_Type (Etype (First_Formal (Func_Id))) + and then Etype (First_Formal (Func_Id)) = Scope (Func_Id) then return True;