GNATprove handles specially invariant checks, and so does not expect to see calls to invariant procedures in the AST. This patch fixes the two places where such calls were inserted during semantic analysis, so that calls are only inserted when not in GNATprove mode. Possibly the same could be done in ASIS mode.
Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-25 Yannick Moy <m...@adacore.com> * sem_ch3.adb (Constant_Redeclaration): Do not insert a call to the invariant procedure in GNATprove mode. * sem_ch5.adb (Analyze_Assignment): Likewise.
Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 253141) +++ sem_ch3.adb (working copy) @@ -12755,9 +12755,13 @@ end if; -- A deferred constant is a visible entity. If type has invariants, - -- verify that the initial value satisfies them. + -- verify that the initial value satisfies them. This is not done in + -- GNATprove mode, as GNATprove handles invariant checks itself. - if Has_Invariants (T) and then Present (Invariant_Procedure (T)) then + if Has_Invariants (T) + and then Present (Invariant_Procedure (T)) + and then not GNATprove_Mode + then Insert_After (N, Make_Invariant_Call (New_Occurrence_Of (Prev, Sloc (N)))); end if; Index: sem_ch5.adb =================================================================== --- sem_ch5.adb (revision 253141) +++ sem_ch5.adb (working copy) @@ -839,14 +839,16 @@ Set_Referenced_Modified (Lhs, Out_Param => False); end if; - -- RM 7.3.2 (12/3): An assignment to a view conversion (from a type - -- to one of its ancestors) requires an invariant check. Apply check - -- only if expression comes from source, otherwise it will be applied - -- when value is assigned to source entity. + -- RM 7.3.2 (12/3): An assignment to a view conversion (from a type to + -- one of its ancestors) requires an invariant check. Apply check only + -- if expression comes from source, otherwise it will be applied when + -- value is assigned to source entity. This is not done in GNATprove + -- mode, as GNATprove handles invariant checks itself. if Nkind (Lhs) = N_Type_Conversion and then Has_Invariants (Etype (Expression (Lhs))) and then Comes_From_Source (Expression (Lhs)) + and then not GNATprove_Mode then Insert_After (N, Make_Invariant_Call (Expression (Lhs))); end if;