This patch corrects the mechanism which verifies the legality of references to variables and constants acting as Part_Of constituents of single protected or task types to continue examining the context of the reference when it appears in an expression function.
------------ -- Source -- ------------ -- prot.ads package Prot with SPARK_Mode is protected P is end P; function Func return Boolean; private G : Boolean := False with Part_Of => P; end Prot; -- prot.adb package body Prot with SPARK_Mode is protected body P is end P; function Flip return Boolean is (G); function Func return Boolean is begin return G; end Func; end Prot; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c prot.adb prot.adb:5:37: reference to variable "G" cannot appear in this context prot.adb:5:37: "G" is constituent of single task type "P" prot.adb:9:14: reference to variable "G" cannot appear in this context prot.adb:9:14: "G" is constituent of single task type "P" Tested on x86_64-pc-linux-gnu, committed on trunk 2017-04-25 Hristian Kirtchev <kirtc...@adacore.com> * sem_util.adb (Check_Part_Of_Reference): Continue to examine the context if the reference appears within an expression function.
Index: sem_util.adb =================================================================== --- sem_util.adb (revision 247151) +++ sem_util.adb (working copy) @@ -1823,9 +1823,21 @@ N_Subprogram_Declaration) and then not Comes_From_Source (Par) then - OK_Use := True; - exit; + -- Continue to examine the context if the reference appears in a + -- subprogram body which was previously an expression function. + if Nkind (Par) = N_Subprogram_Body + and then Was_Expression_Function (Par) + then + null; + + -- Otherwise the reference is legal + + else + OK_Use := True; + exit; + end if; + -- The reference has been relocated to an inlined body for GNATprove. -- Assume that the reference is legal as the real check was already -- performed in the original context of the reference.