diff options
| author | Yannick Moy <moy@adacore.com> | 2020-01-07 17:39:31 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-06-03 06:01:32 -0400 |
| commit | 9ff488f0292841a709840b6d2cb4d18e2f1b491a (patch) | |
| tree | fdfbdc27fff956a7854c0e0992bb2c5bd2492798 | |
| parent | 3c5fb4f4957a7046f631c648b362522d55d19fbc (diff) | |
| download | gcc-9ff488f0292841a709840b6d2cb4d18e2f1b491a.zip gcc-9ff488f0292841a709840b6d2cb4d18e2f1b491a.tar.gz gcc-9ff488f0292841a709840b6d2cb4d18e2f1b491a.tar.bz2 | |
[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.
| -rw-r--r-- | gcc/ada/inline.adb | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index b6e6a27..e49b83e 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; |