diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2021-03-03 23:18:01 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-06-17 10:32:08 -0400 |
| commit | 02e9e5fb97a0342e370ea7ec0fff519b42edf097 (patch) | |
| tree | 21f59793edf59f024708ef1ccd95e453d30611a9 /gcc | |
| parent | 8cbaa09333d3e338a438b067a0c18d2d9673fc1a (diff) | |
| download | gcc-02e9e5fb97a0342e370ea7ec0fff519b42edf097.zip gcc-02e9e5fb97a0342e370ea7ec0fff519b42edf097.tar.gz gcc-02e9e5fb97a0342e370ea7ec0fff519b42edf097.tar.bz2 | |
[Ada] Reject allocators in contexts restricted by SPARK
gcc/ada/
* sem_ch4.adb (Analyze_Allocator): Reject allocators in
restricted contexts.
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index d849834..ede257b 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -889,6 +889,16 @@ 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); |