[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 --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index b6e6a27d1859b4d4f70b9c0b02937294b7c83332..e49b83e88a0164d63fd0f6201a836341810e7de6 100644 (file)
--- 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;