ada: Support new SPARK aspect Side_Effects

[gcc.git] / gcc / ada / sem_ch13.adb

diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index f89135983cf64d9e96212b611b417c871bf586ea..ae06313aa8d0c796447332ea957c69859c37096d 100644 (file)
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1438,6 +1438,7 @@ package body Sem_Ch13 is
       --    Refined_Global
       --    Refined_Post
       --    Refined_State
+      --    Side_Effects
       --    SPARK_Mode
       --    Secondary_Stack_Size
       --    Subprogram_Variant
@@ -3934,6 +3935,21 @@ package body Sem_Ch13 is
 
                   goto Continue;
 
+               --  Aspect Side_Effects is never delayed because it is
+               --  equivalent to a source pragma which appears after
+               --  the related subprogram.
+
+               when Aspect_Side_Effects =>
+                  Aitem := Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Side_Effects);
+
+                  Decorate (Aspect, Aitem);
+                  Insert_Pragma (Aitem);
+                  goto Continue;
+
                --  SPARK_Mode
 
                when Aspect_SPARK_Mode =>
@@ -11374,6 +11390,7 @@ package body Sem_Ch13 is
             | Aspect_Postcondition
             | Aspect_Pre
             | Aspect_Precondition
+            | Aspect_Side_Effects
             | Aspect_Refined_Depends
             | Aspect_Refined_Global
             | Aspect_Refined_Post