Patchwork [Ada] Locally enabled invariants are ignored

login
register
mail settings
Submitter Arnaud Charlet
Date April 25, 2013, 10:11 a.m.
Message ID <20130425101113.GA32723@adacore.com>
Download mbox | patch
Permalink /patch/239452/
State New
Headers show

Comments

Arnaud Charlet - April 25, 2013, 10:11 a.m.
This patch modifies the logic that generates procedure _Postconditions to take
into account empty invariant procedures and disabled predicates.

------------
-- Source --
------------

--  main.adb

pragma Assertion_Policy (Invariant => Check);

procedure Main is
   X : Integer := 1;
   type R is new Integer with Predicate => X > 0;
   package Pack is
      type T is tagged private;
      procedure P (Arg1 : in out T; Arg2 : in out R) with
        Post       => X > 0,
        Post'Class => X > 0;
   private
      type T is tagged null record with Invariant => X > 0;
   end Pack;
   package body Pack is
      procedure P (Arg1 : in out T; Arg2 : in out R) is
      begin
         null;
      end P;
   end Pack;
   use Pack;
   Y : T;
   Z : R := 2;
begin
   X := 0;
   P (Y, Z);
end Main;

----------------------------
-- Compilation and output --
----------------------------

$ gnatmake -q -gnat12 main.adb
$ ./main
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed invariant from main.adb:12

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-04-25  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch6.adb (Check_Access_Invariants): Test whether an
	invariant procedure is empty before generating a call to it.
	(Has_Enabled_Predicate): New routine.
	(Has_Null_Body): New routine.
	(Process_PPCs): Test whether an invariant procedure is
	empty before generating a call to it. Test whether predicates are
	enabled for a particular type before generating a predicate call.
	* sem_util.ads, sem_util.adb (Find_Pragma): New routine.

Patch

Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 198237)
+++ sem_util.adb	(working copy)
@@ -4882,6 +4882,26 @@ 
       end if;
    end Find_Parameter_Type;
 
+   -----------------
+   -- Find_Pragma --
+   -----------------
+
+   function Find_Pragma (Id : Entity_Id; Name : Name_Id) return Node_Id is
+      Item : Node_Id;
+
+   begin
+      Item := First_Rep_Item (Id);
+      while Present (Item) loop
+         if Nkind (Item) = N_Pragma and then Pragma_Name (Item) = Name then
+            return Item;
+         end if;
+
+         Item := Next_Rep_Item (Item);
+      end loop;
+
+      return Empty;
+   end Find_Pragma;
+
    -----------------------------
    -- Find_Static_Alternative --
    -----------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 198237)
+++ sem_util.ads	(working copy)
@@ -494,6 +494,11 @@ 
    --  Return the type of formal parameter Param as determined by its
    --  specification.
 
+   function Find_Pragma (Id : Entity_Id; Name : Name_Id) return Node_Id;
+   --  Given entity Id and pragma name Name, attempt to find the corresponding
+   --  pragma in Id's chain of representation items. The function returns Empty
+   --  if no such pragma has been found.
+
    function Find_Static_Alternative (N : Node_Id) return Node_Id;
    --  N is a case statement whose expression is a compile-time value.
    --  Determine the alternative chosen, so that the code of non-selected
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 198275)
+++ sem_ch6.adb	(working copy)
@@ -11241,6 +11241,14 @@ 
       --  references to parameters of the inherited subprogram to point to the
       --  corresponding parameters of the current subprogram.
 
+      function Has_Checked_Predicate (Typ : Entity_Id) return Boolean;
+      --  Determine whether type Typ has or inherits at least one predicate
+      --  aspect or pragma, for which the applicable policy is Checked.
+
+      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.
+
       procedure Insert_After_Last_Declaration (Nod : Node_Id);
       --  Insert node Nod after the last declaration of the context
 
@@ -11294,6 +11302,7 @@ 
 
             if Has_Invariants (Typ)
               and then Present (Invariant_Procedure (Typ))
+              and then not Has_Null_Body (Invariant_Procedure (Typ))
               and then Is_Public_Subprogram_For (Typ)
             then
                Obj :=
@@ -11886,6 +11895,91 @@ 
          return CP;
       end Grab_PPC;
 
+      ---------------------------
+      -- Has_Checked_Predicate --
+      ---------------------------
+
+      function Has_Checked_Predicate (Typ : Entity_Id) return Boolean is
+         Anc  : Entity_Id;
+         Pred : Node_Id;
+
+      begin
+         --  Climb the ancestor type chain staring from the input. This is done
+         --  because the input type may lack aspect/pragma predicate and simply
+         --  inherit those from its ancestor.
+
+         Anc := Typ;
+         while Present (Anc) loop
+            Pred := Find_Pragma (Anc, Name_Predicate);
+
+            if Present (Pred) and then not Is_Ignored (Pred) then
+               return True;
+            end if;
+
+            Anc := Nearest_Ancestor (Anc);
+         end loop;
+
+         return False;
+      end Has_Checked_Predicate;
+
+      -------------------
+      -- 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;
+
       -----------------------------------
       -- Insert_After_Last_Declaration --
       -----------------------------------
@@ -12262,11 +12356,7 @@ 
 
       --  Add an invariant call to check the result of a function
 
-      if Ekind (Designator) /= E_Procedure
-        and then Expander_Active
-        --  Check of Assertions_Enabled is certainly wrong ???
-        and then Assertions_Enabled
-      then
+      if Ekind (Designator) /= E_Procedure and then Expander_Active then
          Func_Typ := Etype (Designator);
          Result   := Make_Defining_Identifier (Loc, Name_uResult);
 
@@ -12285,6 +12375,7 @@ 
 
          if Has_Invariants (Func_Typ)
            and then Present (Invariant_Procedure (Func_Typ))
+           and then not Has_Null_Body (Invariant_Procedure (Func_Typ))
            and then Is_Public_Subprogram_For (Func_Typ)
          then
             Append_Enabled_Item
@@ -12305,8 +12396,7 @@ 
       --  this is done for functions as well, since in Ada 2012 they can have
       --  IN OUT args.
 
-      if Expander_Active and then Assertions_Enabled then
-         --  Check of Assertions_Enabled is certainly wrong ???
+      if Expander_Active then
          Formal := First_Formal (Designator);
          while Present (Formal) loop
             if Ekind (Formal) /= E_In_Parameter
@@ -12316,6 +12406,7 @@ 
 
                if Has_Invariants (Formal_Typ)
                  and then Present (Invariant_Procedure (Formal_Typ))
+                 and then not Has_Null_Body (Invariant_Procedure (Formal_Typ))
                  and then Is_Public_Subprogram_For (Formal_Typ)
                then
                   Append_Enabled_Item
@@ -12325,7 +12416,10 @@ 
 
                Check_Access_Invariants (Formal);
 
-               if Present (Predicate_Function (Formal_Typ)) then
+               if Has_Predicates (Formal_Typ)
+                 and then Present (Predicate_Function (Formal_Typ))
+                 and then Has_Checked_Predicate (Formal_Typ)
+               then
                   Append_Enabled_Item
                     (Make_Predicate_Check
                       (Formal_Typ, New_Occurrence_Of (Formal, Loc)),