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/libgnat | |
| 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/libgnat')
| -rw-r--r-- | gcc/ada/libgnat/a-uncdea.ads | 5 |
1 files changed, 4 insertions, 1 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); |