Patchwork [Ada] Implement new assertion kind Statement_Assertions

login
register
mail settings
Submitter Arnaud Charlet
Date April 23, 2013, 9:56 a.m.
Message ID <20130423095615.GA5216@adacore.com>
Download mbox | patch
Permalink /patch/238845/
State New
Headers show

Comments

Arnaud Charlet - April 23, 2013, 9:56 a.m.
This patch implements a new assertion kind (usable in a Check_Policy
or Assertion_Policy pragma) "Statement_Assertions" which applies to
Assert, Assert_And_Cut, Assume, and Loop_Invariant.

The following program is to be compiled with the -gnatd.F switch (this
switch can be removed soon when we make the other assertion kinds first
class citizens)

     1. pragma Ada_2012;
     2. with Text_IO; use Text_IO;
     3. with System.Assertions; use System.Assertions;
     4. procedure StmAssert is
     5.    function Id (X : Integer) return Integer
     6.    is begin return X; end;
     7.
     8.    Y : Integer := Id (10);
     9.
    10. begin
    11.    declare
    12.       pragma Check_Policy
    13.         (Statement_Assertions, Check);
    14.    begin
    15.       begin
    16.          pragma Assert (Y = 11);
    17.          Put_Line ("not OK1");
    18.       exception
    19.          when Assert_Failure =>
    20.             Put_Line ("OK1");
    21.       end;
    22.       begin
    23.          pragma Assert_And_Cut (Y = 11);
    24.          Put_Line ("not OK2");
    25.       exception
    26.          when Assert_Failure =>
    27.             Put_Line ("OK2");
    28.       end;
    29.       begin
    30.          pragma Assume (Y = 11);
    31.          Put_Line ("not OK3");
    32.       exception
    33.          when Assert_Failure =>
    34.             Put_Line ("OK3");
    35.       end;
    36.       begin
    37.          for J in 1 .. 1 loop
    38.             pragma Loop_Invariant (Y = 11);
    39.             Put_Line ("not OK4");
    40.          end loop;
    41.       exception
    42.          when Assert_Failure =>
    43.             Put_Line ("OK4");
    44.       end;
    45.    end;
    46.    declare
    47.       pragma Assertion_Policy
    48.         (Statement_Assertions => Ignore);
    49.    begin
    50.       pragma Assert (Y = 11);
    51.       pragma Assert_And_Cut (Y = 11);
    52.       pragma Assume (Y = 11);
    53.       for J in 1 .. 1 loop
    54.          pragma Loop_Invariant (J = 2);
    55.       end loop;
    56.       Put_Line ("OK5");
    57.    exception
    58.       when others => Put_Line ("not OK5");
    59.    end;
    60.
    61. end StmAssert;

The output is:

OK1
OK2
OK3
OK4
OK5

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

2013-04-23  Robert Dewar  <dewar@adacore.com>

	* exp_prag.adb (Expand_Pragma_Check): Check for Assert rather
	than Assertion.
	* sem_prag.adb (Is_Valid_Assertion_Kind): Moved to spec
	(Effective_Name): New function (Analyze_Pragma, case Check):
	Disallow [Statement_]Assertions (Check_Kind): Implement
	Statement_Assertions (Check_Applicable_Policy): Use Effective_Name
	(Is_Valid_Assertion_Kind): Allow Statement_Assertions.
	* sem_prag.ads (Is_Valid_Assertion_Kind): Moved here from body
	(Effective_Name): New function.
	* sem_res.adb: Minor reformatting.
	* snames.ads-tmpl (Name_Statement_Assertions): New entry.
	* gnat_rm.texi: Add documentation of new assertion kind
	Statement_Assertions.

Patch

Index: exp_prag.adb
===================================================================
--- exp_prag.adb	(revision 198175)
+++ exp_prag.adb	(working copy)
@@ -377,7 +377,7 @@ 
 
                --  For Assert, we just use the location
 
-               if Nam = Name_Assertion then
+               if Nam = Name_Assert then
                   null;
 
                --  For predicate, we generate the string "predicate failed
@@ -446,7 +446,7 @@ 
          then
             return;
 
-         elsif Nam = Name_Assertion then
+         elsif Nam = Name_Assert then
             Error_Msg_N ("?A?assertion will fail at run time", N);
          else
 
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 198175)
+++ gnat_rm.texi	(working copy)
@@ -1251,7 +1251,8 @@ 
                       Type_Invariant       |
                       Type_Invariant'Class
 
-ID_ASSERTION_KIND ::= Assert_And_Cut       |
+ID_ASSERTION_KIND ::= Assertions           |
+                      Assert_And_Cut       |
                       Assume               |
                       Contract_Cases       |
                       Debug                |
@@ -1262,6 +1263,7 @@ 
                       Postcondition        |
                       Precondition         |
                       Predicate
+                      Statement_Assertions
 
 POLICY_IDENTIFIER ::= Check | Disable | Ignore
 @end smallexample
@@ -1292,6 +1294,15 @@ 
 in a with'ed package which is replaced by a dummy package
 for the final build.
 
+The implementation defined policy @code{Assertions} applies to all
+assertion kinds. The form with no assertion kind given implies this
+choice, so it applies to all assertion kinds (RM defined, and
+implementation defined).
+
+The implementation defined policy @code{Statement_Assertions}
+applies to @code{Assert}, @code{Assert_And_Cut},
+@code{Assume}, and @code{Loop_Invariant}.
+
 @node Pragma Assume_No_Invalid_Values
 @unnumberedsec Pragma Assume_No_Invalid_Values
 @findex Assume_No_Invalid_Values
@@ -1460,6 +1471,11 @@ 
 be activated either by the command line option @option{-gnata}, which turns on
 all checks, or individually controlled using pragma @code{Check_Policy}.
 
+The identifiers @code{Assertions} and @code{Statement_Assertions} are not
+permitted as check kinds, since this would cause confusion with the use
+of these identifiers in @code{Assertion_Policy} and @code{Check_Policy}
+pragmas, where they are used to refer to sets of assertions.
+
 @node Pragma Check_Float_Overflow
 @unnumberedsec Pragma Check_Float_Overflow
 @cindex Floating-point overflow
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 198184)
+++ sem_prag.adb	(working copy)
@@ -181,13 +181,6 @@ 
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
-   function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
-   --  Returns True if Nam is one of the names recognized as a valid assertion
-   --  kind by the Assertion_Policy pragma. Note that the 'Class cases are
-   --  represented by the corresponding special names Name_uPre, Name_uPost,
-   --  Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant,
-   --  and _Type_Invariant).
-
    procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id);
    --  Preanalyze the boolean expressions in the Requires and Ensures arguments
    --  of a Test_Case pragma if present (possibly Empty). We treat these as
@@ -352,9 +345,7 @@ 
       --  In ASIS mode, for a pragma generated from a source aspect, also
       --  analyze the original aspect expression.
 
-      if ASIS_Mode
-        and then Present (Corresponding_Aspect (N))
-      then
+      if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
          Preanalyze_Assert_Expression
            (Expression (Corresponding_Aspect (N)), Standard_Boolean);
       end if;
@@ -2222,9 +2213,7 @@ 
                --  In ASIS mode, for a pragma generated from a source aspect,
                --  also analyze the original aspect expression.
 
-               if ASIS_Mode
-                 and then Present (Corresponding_Aspect (N))
-               then
+               if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
                   Preanalyze_Assert_Expression
                     (Expression (Corresponding_Aspect (N)), Standard_Boolean);
                end if;
@@ -2411,9 +2400,7 @@ 
          --  In ASIS mode, for a pragma generated from a source aspect, also
          --  analyze the original aspect expression.
 
-         if ASIS_Mode
-           and then Present (Corresponding_Aspect (N))
-         then
+         if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
             Check_Expr_Is_Static_Expression
               (Original_Node (Get_Pragma_Arg (Arg1)), Standard_String);
          end if;
@@ -2882,10 +2869,7 @@ 
 
             --  Get name from corresponding aspect
 
-            if Present (Corresponding_Aspect (N)) then
-               Error_Msg_Name_1 :=
-                 Chars (Identifier (Corresponding_Aspect (N)));
-            end if;
+            Error_Msg_Name_1 := Effective_Name (N);
          end if;
       end Fix_Error;
 
@@ -6765,11 +6749,8 @@ 
       --  Here to start processing for recognized pragma
 
       Prag_Id := Get_Pragma_Id (Pname);
+      Pname := Effective_Name (N);
 
-      if Present (Corresponding_Aspect (N)) then
-         Pname := Chars (Identifier (Corresponding_Aspect (N)));
-      end if;
-
       --  Check applicable policy. We skip this for a pragma that came from
       --  an aspect, since we already dealt with the Disable case, and we set
       --  the Is_Ignored flag at the time the aspect was analyzed.
@@ -7426,9 +7407,9 @@ 
             Check_Arg_Order ((Name_Check, Name_Message));
             Check_Optional_Identifier (Arg1, Name_Check);
 
-            --  We treat pragma Assert as equivalent to:
+            --  We treat pragma Assert[_And_Cut] as equivalent to:
 
-            --    pragma Check (Assertion, condition [, msg]);
+            --    pragma Check (Assert[_And_Cut], condition [, msg]);
 
             --  So rewrite pragma in this manner, transfer the message
             --  argument if present, and analyze the result
@@ -7443,8 +7424,7 @@ 
             Expr := Get_Pragma_Arg (Arg1);
             Newa := New_List (
               Make_Pragma_Argument_Association (Loc,
-                Expression => Make_Identifier (Loc, Name_Assertion)),
-
+                Expression => Make_Identifier (Loc, Pname)),
               Make_Pragma_Argument_Association (Sloc (Expr),
                 Expression => Expr));
 
@@ -8083,6 +8063,9 @@ 
          --                 Invariant'Class      |
          --                 Type_Invariant'Class
 
+         --  The identifiers Assertions and Statement_Assertions are not
+         --  allowed, since they have special meaning for Check_Policy.
+
          when Pragma_Check => Check : declare
             Expr  : Node_Id;
             Eloc  : Source_Ptr;
@@ -8108,6 +8091,23 @@ 
             Check_Arg_Is_Identifier (Arg1);
             Cname := Chars (Get_Pragma_Arg (Arg1));
 
+            --  Check forbidden name Assertions or Statement_Assertions
+
+            case Cname is
+               when Name_Assertions =>
+                  Error_Pragma_Arg
+                    ("""Assertions"" is not allowed as a check kind "
+                     & "for pragma%", Arg1);
+
+               when Name_Statement_Assertions =>
+                  Error_Pragma_Arg
+                    ("""Statement_Assertions"" is not allowed as a check kind "
+                     & "for pragma%", Arg1);
+
+               when others =>
+                  null;
+            end case;
+
             --  Set Check_On to indicate check status
 
             --  If this comes from an aspect, we have already taken care of
@@ -17945,8 +17945,13 @@ 
 
          begin
             if Nam = Pnm
-              or else (Is_Valid_Assertion_Kind (Nam)
-                        and then Pnm = Name_Assertion)
+              or else (Pnm = Name_Assertion
+                        and then Is_Valid_Assertion_Kind (Nam))
+              or else (Pnm = Name_Statement_Assertions
+                        and then Nam_In (Nam, Name_Assert,
+                                              Name_Assert_And_Cut,
+                                              Name_Assume,
+                                              Name_Loop_Invariant))
             then
                case (Chars (Get_Pragma_Arg (Last (PPA)))) is
                   when Name_On | Name_Check =>
@@ -17985,36 +17990,9 @@ 
       PP     : Node_Id;
       Policy : Name_Id;
 
-      Ename : Name_Id;
-      --  Effective name of aspect or pragma, this is simply the name of
-      --  the aspect or pragma, except in the case of a pragma derived from
-      --  an aspect, in which case it is the name of the aspect (which may be
-      --  different, e.g. Pre aspect generating Precondition pragma). It also
-      --  deals with the 'Class cases for an aspect.
+      Ename : constant Name_Id := Effective_Name (N);
 
    begin
-      if Nkind (N) = N_Pragma then
-         if Present (Corresponding_Aspect (N)) then
-            Ename := Chars (Identifier (Corresponding_Aspect (N)));
-         else
-            Ename := Chars (Pragma_Identifier (N));
-         end if;
-
-      else
-         pragma Assert (Nkind (N) = N_Aspect_Specification);
-         Ename := Chars (Identifier (N));
-
-         if Class_Present (N) then
-            case Ename is
-               when Name_Invariant      => Ename := Name_uInvariant;
-               when Name_Pre            => Ename := Name_uPre;
-               when Name_Post           => Ename := Name_uPost;
-               when Name_Type_Invariant => Ename := Name_uType_Invariant;
-               when others              => raise Program_Error;
-            end case;
-         end if;
-      end if;
-
       --  No effect if not valid assertion kind name
 
       if not Is_Valid_Assertion_Kind (Ename) then
@@ -18072,6 +18050,66 @@ 
                                       Name_Priority_Specific_Dispatching);
    end Delay_Config_Pragma_Analyze;
 
+   --------------------
+   -- Effective_Name --
+   --------------------
+
+   function Effective_Name (N : Node_Id) return Name_Id is
+      Pras : Node_Id;
+      Name : Name_Id;
+
+   begin
+      pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma));
+      Pras := N;
+
+      if Is_Rewrite_Substitution (Pras)
+        and then Nkind (Original_Node (Pras)) = N_Pragma
+      then
+         Pras := Original_Node (Pras);
+      end if;
+
+      --  Case where we came from aspect specication
+
+      if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then
+         Pras := Corresponding_Aspect (Pras);
+      end if;
+
+      --  Get name from aspect or pragma
+
+      if Nkind (Pras) = N_Pragma then
+         Name := Pragma_Name (Pras);
+      else
+         Name := Chars (Identifier (Pras));
+      end if;
+
+      --  Deal with 'Class
+
+      if Class_Present (Pras) then
+         case Name is
+
+         --  Names that need converting to special _xxx form
+
+            when Name_Pre             => Name := Name_uPre;
+            when Name_Post            => Name := Name_uPost;
+            when Name_Invariant       => Name := Name_uInvariant;
+            when Name_Type_Invariant  => Name := Name_uType_Invariant;
+
+               --  Names already in special _xxx form (leave them alone)
+
+            when Name_uPre            => null;
+            when Name_uPost           => null;
+            when Name_uInvariant      => null;
+            when Name_uType_Invariant => null;
+
+               --  Anything else is impossible with Class_Present set True
+
+            when others               => raise Program_Error;
+         end case;
+      end if;
+
+      return Name;
+   end Effective_Name;
+
    -------------------------
    -- Get_Base_Subprogram --
    -------------------------
@@ -18521,31 +18559,32 @@ 
          when
             --  RM defined
 
-            Name_Assert            |
-            Name_Static_Predicate  |
-            Name_Dynamic_Predicate |
-            Name_Pre               |
-            Name_uPre              |
-            Name_Post              |
-            Name_uPost             |
-            Name_Type_Invariant    |
-            Name_uType_Invariant   |
+            Name_Assert               |
+            Name_Static_Predicate     |
+            Name_Dynamic_Predicate    |
+            Name_Pre                  |
+            Name_uPre                 |
+            Name_Post                 |
+            Name_uPost                |
+            Name_Type_Invariant       |
+            Name_uType_Invariant      |
 
             --  Impl defined
 
-            Name_Assert_And_Cut    |
-            Name_Assume            |
-            Name_Contract_Cases    |
-            Name_Debug             |
-            Name_Invariant         |
-            Name_uInvariant        |
-            Name_Loop_Invariant    |
-            Name_Loop_Variant      |
-            Name_Postcondition     |
-            Name_Precondition      |
-            Name_Predicate         => return True;
+            Name_Assert_And_Cut       |
+            Name_Assume               |
+            Name_Contract_Cases       |
+            Name_Debug                |
+            Name_Invariant            |
+            Name_uInvariant           |
+            Name_Loop_Invariant       |
+            Name_Loop_Variant         |
+            Name_Postcondition        |
+            Name_Precondition         |
+            Name_Predicate            |
+            Name_Statement_Assertions => return True;
 
-         when others               => return False;
+         when others                  => return False;
       end case;
    end Is_Valid_Assertion_Kind;
 
Index: sem_prag.ads
===================================================================
--- sem_prag.ads	(revision 198175)
+++ sem_prag.ads	(working copy)
@@ -104,10 +104,30 @@ 
    --  True have their analysis delayed until after the main program is parsed
    --  and analyzed.
 
+   function Effective_Name (N : Node_Id) return Name_Id;
+   --  N is a pragma node or aspect specification node. This function returns
+   --  the name of the pragma or aspect, taking into account possible rewrites,
+   --  and also cases where a pragma comes from an attribute (in such cases,
+   --  the name can be different from the pragma name, e.g. Pre generates
+   --  a Precondition pragma. This also deals with the presence of 'Class
+   --  which results in one of the special names Name_uPre, Name_uPost,
+   --  Name_uInvariant, or Name_uType_Invariant being returned to represent
+   --  the corresponding aspects with x'Class names.
+
    procedure Initialize;
    --  Initializes data structures used for pragma processing. Must be called
    --  before analyzing each new main source program.
 
+   function Is_Config_Static_String (Arg : Node_Id) return Boolean;
+   --  This is called for a configuration pragma that requires either string
+   --  literal or a concatenation of string literals. We cannot use normal
+   --  static string processing because it is too early in the case of the
+   --  pragma appearing in a configuration pragmas file. If Arg is of an
+   --  appropriate form, then this call obtains the string (doing any necessary
+   --  concatenations) and places it in Name_Buffer, setting Name_Len to its
+   --  length, and then returns True. If it is not of the correct form, then an
+   --  appropriate error message is posted, and False is returned.
+
    function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
    --  The node N is a node for an entity and the issue is whether the
    --  occurrence is a reference for the purposes of giving warnings about
@@ -124,15 +144,12 @@ 
    --  False is returned, then the argument is treated as an entity reference
    --  to the operator.
 
-   function Is_Config_Static_String (Arg : Node_Id) return Boolean;
-   --  This is called for a configuration pragma that requires either string
-   --  literal or a concatenation of string literals. We cannot use normal
-   --  static string processing because it is too early in the case of the
-   --  pragma appearing in a configuration pragmas file. If Arg is of an
-   --  appropriate form, then this call obtains the string (doing any necessary
-   --  concatenations) and places it in Name_Buffer, setting Name_Len to its
-   --  length, and then returns True. If it is not of the correct form, then an
-   --  appropriate error message is posted, and False is returned.
+   function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
+   --  Returns True if Nam is one of the names recognized as a valid assertion
+   --  kind by the Assertion_Policy pragma. Note that the 'Class cases are
+   --  represented by the corresponding special names Name_uPre, Name_uPost,
+   --  Name_uInviarnat, and Name_uType_Invariant (_Pre, _Post, _Invariant,
+   --  and _Type_Invariant).
 
    procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id);
    --  This routine makes aspects from precondition or postcondition pragmas
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 198186)
+++ sem_res.adb	(working copy)
@@ -8908,27 +8908,32 @@ 
             Orig : constant Node_Id := Original_Node (Parent (N));
 
          begin
+            --  Special handling of Asssert pragma
+
             if Nkind (Orig) = N_Pragma
               and then Pragma_Name (Orig) = Name_Assert
             then
-               --  Don't want to warn if original condition is explicit False
-
                declare
                   Expr : constant Node_Id :=
                            Original_Node
                              (Expression
                                (First (Pragma_Argument_Associations (Orig))));
+
                begin
+                  --  Don't warn if original condition is explicit False,
+                  --  since obviously the failure is expected in this case.
+
                   if Is_Entity_Name (Expr)
                     and then Entity (Expr) = Standard_False
                   then
                      null;
+
+                  --  Issue warning. We do not want the deletion of the
+                  --  IF/AND-THEN to take this message with it. We achieve this
+                  --  by making sure that the expanded code points to the Sloc
+                  --  of the expression, not the original pragma.
+
                   else
-                     --  Issue warning. We do not want the deletion of the
-                     --  IF/AND-THEN to take this message with it. We achieve
-                     --  this by making sure that the expanded code points to
-                     --  the Sloc of the expression, not the original pragma.
-
                      --  Note: Use Error_Msg_F here rather than Error_Msg_N.
                      --  The source location of the expression is not usually
                      --  the best choice here. For example, it gets located on
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 198175)
+++ snames.ads-tmpl	(working copy)
@@ -761,6 +761,7 @@ 
    Name_Simple_Barriers                : constant Name_Id := N + $;
    Name_Spec_File_Name                 : constant Name_Id := N + $;
    Name_State                          : constant Name_Id := N + $;
+   Name_Statement_Assertions           : constant Name_Id := N + $;
    Name_Static                         : constant Name_Id := N + $;
    Name_Stack_Size                     : constant Name_Id := N + $;
    Name_Strict                         : constant Name_Id := N + $;