[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 --git a/gcc/ada/libgnat/a-uncdea.ads b/gcc/ada/libgnat/a-uncdea.ads
index a61cd5003f98cbe37cd3129c70798b44a2ab860e..439fa616ccbdb938b539087bd46ddbf9fbbdf7ba 100644 (file)
--- 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 ede257b6d4007c6d7abb355d299e012cd4845d15..d8498343157fdd95344318d2e6600567d7b54cfa 100644 (file)
--- 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 e639fab92e47f5ccc4adef5ca8540273abc7c09d..b6a9b1d653c4780ea05c8017565321849e087747 100644 (file)
--- 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.