diff options
| author | Yannick Moy <moy@adacore.com> | 2021-04-07 12:15:04 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-07-05 13:09:11 +0000 |
| commit | f7b2ce2f53b18c9770a5caae42e58791d41ae522 (patch) | |
| tree | f8b2599508e3421775f12b28b33eb405c6b5d1fe | |
| parent | 36d4f97d589085ddb0abccf3e0f76a3a1c8045c2 (diff) | |
| download | gcc-f7b2ce2f53b18c9770a5caae42e58791d41ae522.zip gcc-f7b2ce2f53b18c9770a5caae42e58791d41ae522.tar.gz gcc-f7b2ce2f53b18c9770a5caae42e58791d41ae522.tar.bz2 | |
[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.
| -rw-r--r-- | gcc/ada/libgnat/a-uncdea.ads | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 10 | ||||
| -rw-r--r-- | 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 a61cd50..439fa61 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 ede257b..d849834 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 e639fab..b6a9b1d 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. |