An incomplete type may appear in the profile of a subprogram used in a
predicate for the type. Analysis of the constructed predicate function will
include a call to the subprogram, and an actual of the full type will be
resolved against an actual of the incomplete view. This patch handles this
construction properly.

Compiling

   gcc -c -gnatc invariant_question.ads

must yield:

invariant_question.ads:12:27: warning:
     predicate check includes a function call that requires a predicate check
invariant_question.ads:12:27: warning: this will result in infinite recursion

---
package Invariant_Question
is

   type Record_T;

   function Is_Valid (X : Record_T) return Boolean;

   type Record_T is record
      X : Boolean;
      Y : Boolean;
   end record with
     Dynamic_Predicate => Is_Valid (Record_T);

end Invariant_Question;

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

2015-01-06  Ed Schonberg  <schonb...@adacore.com>

        * sem_ch4.adb (Analyze_One_Call): If formal has an incomplete
        type and actual has the corresponding full view, there is no
        error, but a case of use of incomplete type in a predicate or
        invariant expression.

Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb (revision 219191)
+++ sem_ch4.adb (working copy)
@@ -3195,6 +3195,18 @@
                   Next_Actual (Actual);
                   Next_Formal (Formal);
 
+               --  For an Ada 2012 predicate or invariant, a call may mention
+               --  an incomplete type, while resolution of the corresponding
+               --  predicate function may see the full view, as a consequence
+               --  of the delayed resolution of the corresponding expressions.
+
+               elsif Ekind (Etype (Formal)) = E_Incomplete_Type
+                 and then Full_View (Etype (Formal)) = Etype (Actual)
+               then
+                  Set_Etype (Formal, Etype (Actual));
+                  Next_Actual (Actual);
+                  Next_Formal (Formal);
+
                else
                   if Debug_Flag_E then
                      Write_Str (" type checking fails in call ");

Reply via email to