https://gcc.gnu.org/g:428f83d7b10d92e223dac171cdfba4e9d084823f
commit r15-240-g428f83d7b10d92e223dac171cdfba4e9d084823f
Author: Yannick Moy <m...@adacore.com>
Date: Thu Dec 21 17:38:21 2023 +0100
ada: SPARK rule changed on functions with side effects
SPARK RM definition of function with side effects now makes them
implicitly volatile functions.
gcc/ada/
* sem_util.adb (Is_Volatile_Function): Return True on functions
with side effects.
Diff:
---
gcc/ada/sem_util.adb | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 18c9de05cf9..3af029fd9a3 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -21226,6 +21226,11 @@ package body Sem_Util is
then
return True;
+ -- A function with side-effects is volatile
+
+ elsif Is_Function_With_Side_Effects (Func_Id) then
+ return True;
+
-- Otherwise the function is treated as volatile if it is subject to
-- enabled pragma Volatile_Function.
