[gcc r14-1063] ada: Incorrect constant folding in postcondition involving 'Old

[Marc Poulhi?s]

https://gcc.gnu.org/g:6675552bacd41361d8d445438cb6d978d44c1402

commit r14-1063-g6675552bacd41361d8d445438cb6d978d44c1402
Author: Justin Squirek <squirek@adacore.com>
Date:   Thu Feb 9 17:00:46 2023 +0000

    ada: Incorrect constant folding in postcondition involving 'Old
    
    The following patch fixes an issue in the compiler whereby certain flavors of
    access comparisons may be incorrectly constant-folded out of contract
    expressions - notably in postcondition expressions featuring a reference to
    'Old.
    
    gcc/ada/
    
            * checks.adb (Install_Null_Excluding_Check): Avoid non-null
            optimizations when assertions are enabled.

Diff:
---
 gcc/ada/checks.adb | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 9f3c679ed7e..0d472964ff5 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -8437,7 +8437,18 @@ package body Checks is
               Right_Opnd => Make_Null (Loc)),
           Reason => CE_Access_Check_Failed));
 
-      Mark_Non_Null;
+      --  Mark the entity of N "non-null" except when assertions are enabled -
+      --  since expansion becomes much more complicated (especially when it
+      --  comes to contracts) due to the generation of wrappers and wholesale
+      --  moving of declarations and statements which may happen.
+
+      --  Additionally, it is assumed that extra checks will exist with
+      --  assertions enabled so some potentially redundant checks are
+      --  acceptable.
+
+      if not Assertions_Enabled then
+         Mark_Non_Null;
+      end if;
    end Install_Null_Excluding_Check;
 
    -----------------------------------------