diff mbox series

[Ada] Do not insert calls to invariant procedure in GNATprove mode

Message ID 20170925095307.GA13233@adacore.com
State New
Headers show
Series [Ada] Do not insert calls to invariant procedure in GNATprove mode | expand

Commit Message

Pierre-Marie de Rodat Sept. 25, 2017, 9:53 a.m. UTC 
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  <moy@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.
diff mbox series

Patch

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;