Patchwork [Ada] Expression of static predicate should be static

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

Comments

Arnaud Charlet - April 25, 2013, 10:13 a.m.
This patch updates the mechanism which creates predicate functions to ensure
that the expression of a static predicate is static.

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

--  pack.ads

package Pack is
   subtype T1 is Integer with Dynamic_Predicate => T1 /= 0;
   subtype T2 is T1 with Static_Predicate => T2 mod 2 = 0;
end Pack;

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

$ gcc -c -gnat12 pack.ads
pack.ads:3:55: expression does not have required form for static predicate

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

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

	* sem_ch13.adb (Add_Call): Do not capture the nature of the inherited
	predicate.
	(Add_Predicates): Save the static predicate for diagnostics and error
	reporting purposes.
	(Process_PPCs): Remove local variables Dynamic_Predicate_Present and
	Static_Predicate_Present. Add local variable Static_Pred. Ensure that
	the expression of a static predicate is static.

Patch

Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 198243)
+++ sem_ch13.adb	(working copy)
@@ -5741,6 +5741,9 @@ 
       Raise_Expression_Present : Boolean := False;
       --  Set True if Expr has at least one Raise_Expression
 
+      Static_Predic : Node_Id := Empty;
+      --  Set to N_Pragma node for a static predicate if one is encountered
+
       procedure Add_Call (T : Entity_Id);
       --  Includes a call to the predicate function for type T in Expr if T
       --  has predicates and Predicate_Function (T) is non-empty.
@@ -5765,13 +5768,6 @@ 
       procedure Process_REs is new Traverse_Proc (Process_RE);
       --  Marks any raise expressions in Expr_M to return False
 
-      Dynamic_Predicate_Present : Boolean := False;
-      --  Set True if a dynamic predicate is present, results in the entire
-      --  predicate being considered dynamic even if it looks static.
-
-      Static_Predicate_Present : Node_Id := Empty;
-      --  Set to N_Pragma node for a static predicate if one is encountered
-
       --------------
       -- Add_Call --
       --------------
@@ -5783,12 +5779,6 @@ 
          if Present (T) and then Present (Predicate_Function (T)) then
             Set_Has_Predicates (Typ);
 
-            --  Capture the nature of the inherited ancestor predicate
-
-            if Has_Dynamic_Predicate_Aspect (T) then
-               Dynamic_Predicate_Present := True;
-            end if;
-
             --  Build the call to the predicate function of T
 
             Exp :=
@@ -5872,17 +5862,14 @@ 
             if Nkind (Ritem) = N_Pragma
               and then Pragma_Name (Ritem) = Name_Predicate
             then
-               --  Capture the nature of the predicate
+               --  Save the static predicate of the type for diagnostics and
+               --  error reporting purposes.
 
-               if Present (Corresponding_Aspect (Ritem)) then
-                  case Chars (Identifier (Corresponding_Aspect (Ritem))) is
-                     when Name_Dynamic_Predicate =>
-                        Dynamic_Predicate_Present := True;
-                     when Name_Static_Predicate =>
-                        Static_Predicate_Present := Ritem;
-                     when others =>
-                        null;
-                  end case;
+               if Present (Corresponding_Aspect (Ritem))
+                 and then Chars (Identifier (Corresponding_Aspect (Ritem))) =
+                            Name_Static_Predicate
+               then
+                  Static_Predic := Ritem;
                end if;
 
                --  Acquire arguments
@@ -6211,7 +6198,9 @@ 
 
             --  Attempt to build a static predicate for a discrete or a real
             --  subtype. This action may fail because the actual expression may
-            --  not be static.
+            --  not be static. Note that the presence of an inherited or
+            --  explicitly declared dynamic predicate is orthogonal to this
+            --  check because we are only interested in the static predicate.
 
             if Ekind_In (Typ, E_Decimal_Fixed_Point_Subtype,
                               E_Enumeration_Subtype,
@@ -6222,30 +6211,26 @@ 
             then
                Build_Static_Predicate (Typ, Expr, Object_Name);
 
-               --  The predicate is categorized as static but its expression is
-               --  dynamic. Note that the predicate may become non-static when
-               --  inherited dynamic predicates are involved.
+               --  Emit an error when the predicate is categorized as static
+               --  but its expression is dynamic.
 
-               if Present (Static_Predicate_Present)
+               if Present (Static_Predic)
                  and then No (Static_Predicate (Typ))
-                 and then not Dynamic_Predicate_Present
                then
                   Error_Msg_F
                     ("expression does not have required form for "
                      & "static predicate",
                      Next (First (Pragma_Argument_Associations
-                                   (Static_Predicate_Present))));
+                                   (Static_Predic))));
                end if;
             end if;
 
-         --  If a Static_Predicate applies on other types, that's an error:
+         --  If a static predicate applies on other types, that's an error:
          --  either the type is scalar but non-static, or it's not even a
          --  scalar type. We do not issue an error on generated types, as
          --  these may be duplicates of the same error on a source type.
 
-         elsif Present (Static_Predicate_Present)
-           and then Comes_From_Source (Typ)
-         then
+         elsif Present (Static_Predic) and then Comes_From_Source (Typ) then
             if Is_Scalar_Type (Typ) then
                Error_Msg_FE
                  ("static predicate not allowed for non-static type&",