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 ");
