[gcc r12-2017] [Ada] Adapt SPARK checking after change in rules regarding heap modeling

[gcc r12-2017] [Ada] Adapt SPARK checking after change in rules regarding heap modeling

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:f7b2ce2f53b18c9770a5caae42e58791d41ae522

commit r12-2017-gf7b2ce2f53b18c9770a5caae42e58791d41ae522
Author: Yannick Moy <moy@adacore.com>
Date:   Wed Apr 7 12:15:04 2021 +0200

    [Ada] Adapt SPARK checking after change in rules regarding heap modeling
    
    gcc/ada/
    
            * libgnat/a-uncdea.ads: Add Depends/Post to
            Ada.Unchecked_Deallocation.
            * sem_ch4.adb (Analyze_Allocator): Remove checking of allocator
            placement.
            * sem_res.adb (Flag_Object): Same.

Diff:
---
 gcc/ada/libgnat/a-uncdea.ads |  5 ++++-
 gcc/ada/sem_ch4.adb          | 10 ----------
 gcc/ada/sem_res.adb          | 12 ------------
 3 files changed, 4 insertions(+), 23 deletions(-)

diff --git a/gcc/ada/libgnat/a-uncdea.ads b/gcc/ada/libgnat/a-uncdea.ads
index a61cd5003f9..439fa616ccb 100644
--- a/gcc/ada/libgnat/a-uncdea.ads
+++ b/gcc/ada/libgnat/a-uncdea.ads
@@ -17,7 +17,10 @@ generic
    type Object (<>) is limited private;
    type Name is access Object;
 
-procedure Ada.Unchecked_Deallocation (X : in out Name);
+procedure Ada.Unchecked_Deallocation (X : in out Name) with
+  Depends => (X    => null,  --  X on exit does not depend on its input value
+              null => X),    --  X's input value has no effect
+  Post => X = null;          --  X's output value is null
 pragma Preelaborate (Unchecked_Deallocation);
 
 pragma Import (Intrinsic, Ada.Unchecked_Deallocation);
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index ede257b6d40..d8498343157 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -889,16 +889,6 @@ package body Sem_Ch4 is
          Check_Restriction (No_Local_Allocators, N);
       end if;
 
-      if SPARK_Mode = On
-        and then Comes_From_Source (N)
-        and then not Is_OK_Volatile_Context (Context       => Parent (N),
-                                             Obj_Ref       => N,
-                                             Check_Actuals => False)
-      then
-         Error_Msg_N
-           ("allocator cannot appear in this context (SPARK RM 7.1.3(10))", N);
-      end if;
-
       if Serious_Errors_Detected > Sav_Errs then
          Set_Error_Posted (N);
          Set_Etype (N, Any_Type);
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index e639fab92e4..b6a9b1d653c 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3753,18 +3753,6 @@ package body Sem_Res is
 
          begin
             case Nkind (N) is
-               when N_Allocator =>
-                  if not Is_OK_Volatile_Context (Context       => Parent (N),
-                                                 Obj_Ref       => N,
-                                                 Check_Actuals => True)
-                  then
-                     Error_Msg_N
-                       ("allocator cannot appear in this context"
-                        & " (SPARK RM 7.1.3(10))", N);
-                  end if;
-
-                  return Skip;
-
                --  Do not consider nested function calls because they have
                --  already been processed during their own resolution.