[gcc/devel/gccgo] [Ada] Fix missing overflow checks in analysis of predefined unit

[Ian Lance Taylor]

https://gcc.gnu.org/g:9ff488f0292841a709840b6d2cb4d18e2f1b491a

commit 9ff488f0292841a709840b6d2cb4d18e2f1b491a
Author: Yannick Moy <moy@adacore.com>
Date:   Tue Jan 7 17:39:31 2020 +0100

    [Ada] Fix missing overflow checks in analysis of predefined unit
    
    2020-06-03  Yannick Moy  <moy@adacore.com>
    
    gcc/ada/
    
            * inline.adb (Expand_Inlined_Call): Do not suppress checks on
            inlined code in GNATprove mode.

Diff:
---
 gcc/ada/inline.adb | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index b6e6a27d185..e49b83e88a0 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -4103,7 +4103,15 @@ package body Inline is
 
                Reset_Dispatching_Calls (Blk);
 
-               Analyze (Blk, Suppress => All_Checks);
+               --  In GNATprove mode, always consider checks on, even for
+               --  predefined units.
+
+               if GNATprove_Mode then
+                  Analyze (Blk);
+               else
+                  Analyze (Blk, Suppress => All_Checks);
+               end if;
+
                Style_Check := Style;
             end;