[COMMITTED] ada: SPARK rule changed on functions with side effects
Checks
Commit Message
From: Yannick Moy <moy@adacore.com>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sem_util.adb | 5 +++++
1 file changed, 5 insertions(+)
@@ -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.