diff options
author | Yannick Moy <moy@adacore.com> | 2023-12-21 17:38:21 +0100 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2024-05-07 09:55:51 +0200 |
commit | 428f83d7b10d92e223dac171cdfba4e9d084823f (patch) | |
tree | 42c06941857e32617efe9e6170468f528303cd5c /gcc/ada | |
parent | 262d6de0a97d88ea1edbab51d4cd2b3aa36f91a5 (diff) | |
download | gcc-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.adb | 5 |
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. |