From c3026d451dacabecc7ff42b5b81deaf420d758aa Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 27 May 2020 16:46:27 +0200 Subject: [PATCH] [Ada] Fix detection of volatile properties in SPARK gcc/ada/ * sem_util.adb (Has_Enabled_Property): Add handling of non-variable objects. --- gcc/ada/sem_util.adb | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index b70f2c8..4b4f4af 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -11537,6 +11537,14 @@ package body Sem_Util is elsif Ekind (Item_Id) = E_Variable then return Type_Or_Variable_Has_Enabled_Property (Item_Id); + -- Other objects can only inherit properties through their type. We + -- cannot call directly Type_Or_Variable_Has_Enabled_Property on + -- these as they don't have contracts attached, which is expected by + -- this function. + + elsif Is_Object (Item_Id) then + return Type_Or_Variable_Has_Enabled_Property (Etype (Item_Id)); + elsif Is_Type (Item_Id) then return Type_Or_Variable_Has_Enabled_Property (Item_Id => First_Subtype (Item_Id)); -- 2.7.4