diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2020-12-31 15:26:03 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-05-03 05:28:27 -0400 |
| commit | 13b26a958071d818e051f4b3230d381ec974772a (patch) | |
| tree | 27b5401ad50f639325955ea6971af63523536dc1 /gcc/ada/rtsfind.adb | |
| parent | 8d0d46f4a284946eccc504c58d1d9343f0967916 (diff) | |
| download | gcc-13b26a958071d818e051f4b3230d381ec974772a.zip gcc-13b26a958071d818e051f4b3230d381ec974772a.tar.gz gcc-13b26a958071d818e051f4b3230d381ec974772a.tar.bz2 | |
[Ada] Simplify implicit loading for GNATprove with Discard_Node
gcc/ada/
* rtsfind.adb (SPARK_Implicit_Load): Simplify with Discard_Node.
Diffstat (limited to 'gcc/ada/rtsfind.adb')
| -rw-r--r-- | gcc/ada/rtsfind.adb | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index cab8679..33ce7cd 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.adb @@ -1795,14 +1795,12 @@ package body Rtsfind is ------------------------- procedure SPARK_Implicit_Load (E : RE_Id) is - Unused : Entity_Id; - begin pragma Assert (GNATprove_Mode); -- Force loading of a predefined unit - Unused := RTE (E); + Discard_Node (RTE (E)); end SPARK_Implicit_Load; end Rtsfind; |