===================================================================
@@ -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 ");
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 <schonberg@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.