===================================================================
@@ -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.
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 <kirtchev@adacore.com> * sem_util.adb (Check_Part_Of_Reference): Continue to examine the context if the reference appears within an expression function.