aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2019-07-11 08:03:24 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2019-07-11 08:03:24 +0000
commit8b727104817f1b0c2a03013ed397e99f8673405c (patch)
tree379d8b6a9c0283f4c1cf4dada41c41399f3b9bc4
parentd99ef225ac0722ab011cd39386fed4e346311edb (diff)
downloadgcc-8b727104817f1b0c2a03013ed397e99f8673405c.zip
gcc-8b727104817f1b0c2a03013ed397e99f8673405c.tar.gz
gcc-8b727104817f1b0c2a03013ed397e99f8673405c.tar.bz2
[Ada] Avoid spurious errors on dimensionality checking in GNATprove
In the special GNATprove mode of the frontend, automatic inlining is performed, which may lead to spurious errors on dimensionality checking. Avoid performing this checking on inlined code, which has already been checked for dimensionality errors. There is no impact on compilation. 2019-07-11 Yannick Moy <moy@adacore.com> gcc/ada/ * sem_res.adb (Resolve_Call): Do not perform dimensionality checking on inlined bodies. From-SVN: r273405
-rw-r--r--gcc/ada/ChangeLog5
-rw-r--r--gcc/ada/sem_res.adb4
2 files changed, 8 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index a5273a8..59f20c4 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,10 @@
2019-07-11 Yannick Moy <moy@adacore.com>
+ * sem_res.adb (Resolve_Call): Do not perform dimensionality
+ checking on inlined bodies.
+
+2019-07-11 Yannick Moy <moy@adacore.com>
+
* debug.adb: Flip meaning of debug switch -gnatdF.
2019-07-11 Yannick Moy <moy@adacore.com>
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 730f173..4ca74f8 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6949,7 +6949,9 @@ package body Sem_Res is
-- Check the dimensions of the actuals in the call. For function calls,
-- propagate the dimensions from the returned type to N.
- Analyze_Dimension_Call (N, Nam);
+ if not In_Inlined_Body then
+ Analyze_Dimension_Call (N, Nam);
+ end if;
-- All done, evaluate call and deal with elaboration issues