From: Yannick Moy <moy@adacore.com>
Date: Thu, 21 Dec 2023 16:38:21 +0000 (+0100)
Subject: ada: SPARK rule changed on functions with side effects
X-Git-Tag: basepoints/gcc-16~9313
X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=428f83d7b10d92e223dac171cdfba4e9d084823f;p=thirdparty%2Fgcc.git

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 --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.