[Ada] Adapt SPARK checking after change in rules regarding heap modeling

[Pierre-Marie de Rodat]

Rules in SPARK RM section 3.10 regarding modeling of heap through
dynamic (de)allocation has changed. As a result, the dependency contract
of Ada.Unchecked_Deallocation can be added directly in the sources,
and placement of allocators is not checked in the frontend anymore.

Tested on x86_64-pc-linux-gnu, committed on trunk

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