Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 237434)
+++ sem_util.adb	(working copy)
@@ -9581,6 +9581,65 @@
           and then Nkind (Node (First_Elmt (Constits))) /= N_Null;
    end Has_Non_Null_Refinement;
 
+   -------------------
+   -- Has_Null_Body --
+   -------------------
+
+   function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is
+      Body_Id : Entity_Id;
+      Decl    : Node_Id;
+      Spec    : Node_Id;
+      Stmt1   : Node_Id;
+      Stmt2   : Node_Id;
+
+   begin
+      Spec := Parent (Proc_Id);
+      Decl := Parent (Spec);
+
+      --  Retrieve the entity of the procedure body (e.g. invariant proc).
+
+      if Nkind (Spec) = N_Procedure_Specification
+        and then Nkind (Decl) = N_Subprogram_Declaration
+      then
+         Body_Id := Corresponding_Body (Decl);
+
+      --  The body acts as a spec
+
+      else
+         Body_Id := Proc_Id;
+      end if;
+
+      --  The body will be generated later
+
+      if No (Body_Id) then
+         return False;
+      end if;
+
+      Spec := Parent (Body_Id);
+      Decl := Parent (Spec);
+
+      pragma Assert
+        (Nkind (Spec) = N_Procedure_Specification
+          and then Nkind (Decl) = N_Subprogram_Body);
+
+      Stmt1 := First (Statements (Handled_Statement_Sequence (Decl)));
+
+      --  Look for a null statement followed by an optional return
+      --  statement.
+
+      if Nkind (Stmt1) = N_Null_Statement then
+         Stmt2 := Next (Stmt1);
+
+         if Present (Stmt2) then
+            return Nkind (Stmt2) = N_Simple_Return_Statement;
+         else
+            return True;
+         end if;
+      end if;
+
+      return False;
+   end Has_Null_Body;
+
    ------------------------
    -- Has_Null_Exclusion --
    ------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 237434)
+++ sem_util.ads	(working copy)
@@ -1103,6 +1103,11 @@
    --  as expressed in pragma Refined_State. This function does not take into
    --  account the visible refinement region of abstract state Id.
 
+   function Has_Null_Body (Proc_Id : Entity_Id) return Boolean;
+   --  Determine whether the body of procedure Proc_Id contains a sole
+   --  null statement, possibly followed by an optional return. Used to
+   --  optimize useless calls to assertion checks.
+
    function Has_Null_Exclusion (N : Node_Id) return Boolean;
    --  Determine whether node N has a null exclusion
 
Index: contracts.adb
===================================================================
--- contracts.adb	(revision 237429)
+++ contracts.adb	(working copy)
@@ -1452,73 +1452,10 @@
          -------------------------
 
          function Invariant_Checks_OK (Typ : Entity_Id) return Boolean is
-            function Has_Null_Body (Proc_Id : Entity_Id) return Boolean;
-            --  Determine whether the body of procedure Proc_Id contains a sole
-            --  null statement, possibly followed by an optional return.
-
             function Has_Public_Visibility_Of_Subprogram return Boolean;
             --  Determine whether type Typ has public visibility of subprogram
             --  Subp_Id.
 
-            -------------------
-            -- Has_Null_Body --
-            -------------------
-
-            function Has_Null_Body (Proc_Id : Entity_Id) return Boolean is
-               Body_Id : Entity_Id;
-               Decl    : Node_Id;
-               Spec    : Node_Id;
-               Stmt1   : Node_Id;
-               Stmt2   : Node_Id;
-
-            begin
-               Spec := Parent (Proc_Id);
-               Decl := Parent (Spec);
-
-               --  Retrieve the entity of the invariant procedure body
-
-               if Nkind (Spec) = N_Procedure_Specification
-                 and then Nkind (Decl) = N_Subprogram_Declaration
-               then
-                  Body_Id := Corresponding_Body (Decl);
-
-               --  The body acts as a spec
-
-               else
-                  Body_Id := Proc_Id;
-               end if;
-
-               --  The body will be generated later
-
-               if No (Body_Id) then
-                  return False;
-               end if;
-
-               Spec := Parent (Body_Id);
-               Decl := Parent (Spec);
-
-               pragma Assert
-                 (Nkind (Spec) = N_Procedure_Specification
-                   and then Nkind (Decl) = N_Subprogram_Body);
-
-               Stmt1 := First (Statements (Handled_Statement_Sequence (Decl)));
-
-               --  Look for a null statement followed by an optional return
-               --  statement.
-
-               if Nkind (Stmt1) = N_Null_Statement then
-                  Stmt2 := Next (Stmt1);
-
-                  if Present (Stmt2) then
-                     return Nkind (Stmt2) = N_Simple_Return_Statement;
-                  else
-                     return True;
-                  end if;
-               end if;
-
-               return False;
-            end Has_Null_Body;
-
             -----------------------------------------
             -- Has_Public_Visibility_Of_Subprogram --
             -----------------------------------------
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb	(revision 237434)
+++ exp_ch3.adb	(working copy)
@@ -3714,9 +3714,9 @@
          Sel_Comp : Node_Id;
          Typ      : Entity_Id;
          Call     : Node_Id;
+         Proc     : Entity_Id;
 
       begin
-         Invariant_Found := True;
          Typ := Etype (Comp);
 
          Sel_Comp :=
@@ -3744,10 +3744,16 @@
 
          --  The aspect is type-specific, so retrieve it from the base type
 
+         Proc := Invariant_Procedure (Base_Type (Typ));
+
+         if Has_Null_Body (Proc) then
+            return Make_Null_Statement (Loc);
+         end if;
+
+         Invariant_Found := True;
          Call :=
            Make_Procedure_Call_Statement (Loc,
-             Name                   =>
-               New_Occurrence_Of (Invariant_Procedure (Base_Type (Typ)), Loc),
+             Name                   => New_Occurrence_Of (Proc, Loc),
              Parameter_Associations => New_List (Sel_Comp));
 
          if Is_Access_Type (Etype (Comp)) then
