aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2023-12-21 17:38:21 +0100
committerMarc Poulhiès <poulhies@adacore.com>2024-05-07 09:55:51 +0200
commit428f83d7b10d92e223dac171cdfba4e9d084823f (patch)
tree42c06941857e32617efe9e6170468f528303cd5c /gcc/ada
parent262d6de0a97d88ea1edbab51d4cd2b3aa36f91a5 (diff)
downloadgcc-428f83d7b10d92e223dac171cdfba4e9d084823f.zip
gcc-428f83d7b10d92e223dac171cdfba4e9d084823f.tar.gz
gcc-428f83d7b10d92e223dac171cdfba4e9d084823f.tar.bz2
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.
Diffstat (limited to 'gcc/ada')
-rw-r--r--gcc/ada/sem_util.adb5
1 files changed, 5 insertions, 0 deletions
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 18c9de05..3af029f 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.