[Ada] Compiler abort on a dynamic predicate used in a precondition

This patch suppresses the generation of a predicate check when the
expression is a formal IN parameter of a subprogram S. If the check is
being applied to the actual in a call, the call is either in the body of
S, or in an aspect specfication for S, e.g. a precondition, In both
cases the check is redundant bevause it will be applied on any call to
S. In the second case the expansion of the predicate check may lead to
out-of-scope references the the formal.

2019-07-05  Ed Schonberg  <schonberg@adacore.com>

gcc/ada/

	* checks.adb (Apply_Predicate_Check): Except within the
	subprogram body that defines the formal, do not apply predicate
	check on a formal IN parameter: such a check is redundant and
	its expansion can lead to out-of-scope references when it is
	originates in a function call in a precondition,

gcc/testsuite/

	* gnat.dg/predicate7.adb, gnat.dg/predicate7.ads,
	gnat.dg/predicate7_pkg.ads: New testcase.

From-SVN: r273106

6 files changed, 70 insertions, 0 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6f22a1a..b1b98f2 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,11 @@
+2019-07-05  Ed Schonberg  <schonberg@adacore.com>
+
+	* checks.adb (Apply_Predicate_Check): Except within the
+	subprogram body that defines the formal, do not apply predicate
+	check on a formal IN parameter: such a check is redundant and
+	its expansion can lead to out-of-scope references when it is
+	originates in a function call in a precondition,
+
 2019-07-05  Yannick Moy  <moy@adacore.com>
 
 	* sem_res.adb (Resolve_Call): Cannot inline in quantified
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 33fb27e..8176f85 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -2707,6 +2707,41 @@ package body Checks is
          --  Here for normal case of predicate active
 
          else
+            --  If the expression is an IN parameter, the predicate will have
+            --  been applied at the point of call. An additional check would
+            --  be redundant, or will lead to out-of-scope references if the
+            --  call appears within an aspect specification for a precondition.
+
+            --  However, if the reference is within the body of the subprogram
+            --  that declares the formal, the predicate can safely be applied,
+            --  which may be necessary for a nested call whose formal has a
+            --  different predicate.
+
+            if Is_Entity_Name (N)
+              and then Ekind (Entity (N)) = E_In_Parameter
+            then
+               declare
+                  In_Body : Boolean := False;
+                  P : Node_Id := Parent (N);
+
+               begin
+                  while Present (P) loop
+                     if Nkind (P) = N_Subprogram_Body
+                       and then Corresponding_Spec (P) = Scope (Entity (N))
+                     then
+                        In_Body := True;
+                        exit;
+                     end if;
+
+                     P := Parent (P);
+                  end loop;
+
+                  if not In_Body then
+                     return;
+                  end if;
+               end;
+            end if;
+
             --  If the type has a static predicate and the expression is known
             --  at compile time, see if the expression satisfies the predicate.
 
diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog
index 30b2d1f..d5905f0 100644
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,8 @@
+2019-07-05  Ed Schonberg  <schonberg@adacore.com>
+
+	* gnat.dg/predicate7.adb, gnat.dg/predicate7.ads,
+	gnat.dg/predicate7_pkg.ads: New testcase.
+
 2019-07-04  Jakub Jelinek  <jakub@redhat.com>
 
 	PR middle-end/78884
diff --git a/gcc/testsuite/gnat.dg/predicate7.adb b/gcc/testsuite/gnat.dg/predicate7.adb
new file mode 100644
index 0000000..119c190
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/predicate7.adb
@@ -0,0 +1,6 @@
+--  { dg-do compile }
+--  { dg-options "-gnata" }
+
+package body Predicate7 is
+   procedure Foo is null;
+end;
diff --git a/gcc/testsuite/gnat.dg/predicate7.ads b/gcc/testsuite/gnat.dg/predicate7.ads
new file mode 100644
index 0000000..598e2b0
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/predicate7.ads
@@ -0,0 +1,13 @@
+with Predicate7_Pkg; use Predicate7_Pkg;
+
+package Predicate7 is
+   function Always_True (I : My_Int) return Boolean;
+
+   function Identity (I : My_Int ) return Integer with Pre => Always_True (I);
+
+   procedure Foo;
+
+private
+   function Identity (I : My_Int ) return Integer is (I);
+   function Always_True (I : My_Int) return Boolean is (True);
+end;
diff --git a/gcc/testsuite/gnat.dg/predicate7_pkg.ads b/gcc/testsuite/gnat.dg/predicate7_pkg.ads
new file mode 100644
index 0000000..b90419e
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/predicate7_pkg.ads
@@ -0,0 +1,3 @@
+package Predicate7_Pkg is
+  subtype My_Int is Integer with Dynamic_Predicate => My_Int /= 0;
+end Predicate7_Pkg;