Message ID | 20220926091453.273010-1-poulhies@adacore.com |
---|---|
State | New |
Headers | show |
Series | [COMMITED] ada: Only reject volatile ghost objects when SPARK_Mode is On | expand |
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)).
From: Piotr Trojanek <trojanek@adacore.com> 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(-)