From 902d7076663aff56198b81f8efa356c3e1024e80 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 30 Apr 2021 12:41:22 +0200 Subject: [PATCH] [Ada] Adapt SPARK RM rule on non-effectively volatile abstract state gcc/ada/ * sem_prag.adb (Analyze_Global_Item): Adapt to update SPARK RM rule. --- gcc/ada/sem_prag.adb | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index fa63fdae7300..0efdceff5e72 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2433,10 +2433,13 @@ package body Sem_Prag is SPARK_Msg_N ("\use its constituents instead", Item); return; - -- An external state cannot appear as a global item of a - -- nonvolatile function (SPARK RM 7.1.3(8)). + -- An external state which has Async_Writers or + -- Effective_Reads enabled cannot appear as a global item + -- of a nonvolatile function (SPARK RM 7.1.3(8)). elsif Is_External_State (Item_Id) + and then (Async_Writers_Enabled (Item_Id) + or else Effective_Reads_Enabled (Item_Id)) and then Ekind (Spec_Id) in E_Function | E_Generic_Function and then not Is_Volatile_Function (Spec_Id) then -- 2.47.3