From 5549d2695a36f1cd97a1a5d2089c9c5a7f3fb03b Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Thu, 8 Sep 2022 14:58:24 +0200 Subject: [PATCH] ada: Only reject volatile ghost objects when SPARK_Mode is On SPARK rule that forbids ghost volatile objects is only affecting proof and not generation of object code. It is now only applied where SPARK_Mode is On. This flexibility is needed to compile code automatically instrumented by GNATcoverage. gcc/ada/ * contracts.adb (Analyze_Object_Contract): Check SPARK_Mode before applying SPARK rule. --- gcc/ada/contracts.adb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 34db67a8cab..dd573d374c6 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -1207,7 +1207,7 @@ package body Contracts is -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and -- SPARK RM 6.9(19)). - elsif Is_Effectively_Volatile (Obj_Id) then + elsif SPARK_Mode = On and then Is_Effectively_Volatile (Obj_Id) then Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)). -- 2.11.4.GIT