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 /gcc/ada/sem_ch4.adb | |
| 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.
Diffstat (limited to 'gcc/ada/sem_ch4.adb')
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 10 |
1 files changed, 0 insertions, 10 deletions
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); |