[COMMITTED] ada: SPARK rule changed on functions with side effects

Message ID 20240507075952.36520-1-poulhies@adacore.com
State Committed
Headers
Series [COMMITTED] ada: SPARK rule changed on functions with side effects |

Checks

Context Check Description
linaro-tcwg-bot/tcwg_gcc_build--master-arm warning Patch is already merged
linaro-tcwg-bot/tcwg_gcc_build--master-aarch64 warning Patch is already merged

Commit Message

Marc Poulhiès May 7, 2024, 7:59 a.m. UTC
  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(+)
  

Patch

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.