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

[Pierre-Marie de Rodat]

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.

Tested on x86_64-pc-linux-gnu, committed on trunk

2019-07-05  Ed Schonberg  <schonb...@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.
--- gcc/ada/checks.adb
+++ 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.
 

--- /dev/null
new file mode 100644
+++ 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;

--- /dev/null
new file mode 100644
+++ 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;

--- /dev/null
new file mode 100644
+++ 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;