[multiple changes]

2017-01-13  Arnaud Charlet  <charlet@adacore.com>

	* bindusg.adb: Improve usage output for -f switch.

2017-01-13  Hristian Kirtchev  <kirtchev@adacore.com>

	* frontend.adb, freeze.adb, sem_res.adb, sem_attr.adb, sem_ch8.adb:
	Minor reformatting.

2017-01-13  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch13.adb (Is_Predicate_Static): Following the intent of the RM,
	treat comparisons on strings as legal in a Static_Predicate.
	(Is_Predicate_Static, Is_Type_Ref): Predicate also returns true on
	a function call that is the expansion of a string comparison.The
	function call is built when compiling the corresponding predicate
	function, but the expression has been found legal as a static
	predicate during earlier analysis.
	* sem_eval.adb (Real_Or_String_Static_Predicate_Matches): Handle
	properly a function call that is the expansion of a string
	comparison operation, in order to recover the Static_Predicate
	expression and apply it to a static argument when needed.

From-SVN: r244400

gcc/ada/ChangeLog

+2017-01-13  Arnaud Charlet  <charlet@adacore.com>
+
+	* bindusg.adb: Improve usage output for -f switch.
+
+2017-01-13  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* frontend.adb, freeze.adb, sem_res.adb, sem_attr.adb, sem_ch8.adb:
+	Minor reformatting.
+
+2017-01-13  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb (Is_Predicate_Static): Following the intent of the RM,
+	treat comparisons on strings as legal in a Static_Predicate.
+	(Is_Predicate_Static, Is_Type_Ref): Predicate also returns true on
+	a function call that is the expansion of a string comparison.The
+	function call is built when compiling the corresponding predicate
+	function, but the expression has been found legal as a static
+	predicate during earlier analysis.
+	* sem_eval.adb (Real_Or_String_Static_Predicate_Matches): Handle
+	properly a function call that is the expansion of a string
+	comparison operation, in order to recover the Static_Predicate
+	expression and apply it to a static argument when needed.
+
 2017-01-13  Tristan Gingold  <gingold@adacore.com>
 
 	* s-mmap.adb, s-mmap.ads (Open_Read_No_Exception): New function.

gcc/ada/bindusg.adb

@@ -115,7 +115,7 @@ package body Bindusg is
 
       --  Line for -f switch
 
-      Write_Line ("  -felab-order  Force elaboration order");
+      Write_Line ("  -ffile    Force elaboration order from given file");
 
       --  Line for -F switch
 

gcc/ada/freeze.adb

@@ -1457,8 +1457,12 @@ package body Freeze is
             if Present (A_Pre) and then Class_Present (A_Pre) then
                A_Pre :=
                  Expression (First (Pragma_Argument_Associations (A_Pre)));
+
                Build_Class_Wide_Expression
-                 (New_Copy_Tree (A_Pre), Prim, Par_Prim, Adjust_Sloc => False);
+                 (Prag        => New_Copy_Tree (A_Pre),
+                  Subp        => Prim,
+                  Par_Subp    => Par_Prim,
+                  Adjust_Sloc => False);
             end if;
 
             A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition);
@@ -1466,9 +1470,12 @@ package body Freeze is
             if Present (A_Post) and then Class_Present (A_Post) then
                A_Post :=
                  Expression (First (Pragma_Argument_Associations (A_Post)));
+
                Build_Class_Wide_Expression
-                 (New_Copy_Tree (A_Post),
-                  Prim, Par_Prim, Adjust_Sloc => False);
+                 (Prag        => New_Copy_Tree (A_Post),
+                  Subp        => Prim,
+                  Par_Subp    => Par_Prim,
+                  Adjust_Sloc => False);
             end if;
          end if;
 

gcc/ada/frontend.adb

@@ -460,20 +460,21 @@ begin
       end if;
    end if;
 
-   --  In GNATprove mode, force loading of a few RTE units.
+   --  In GNATprove mode, force the loading of a few RTE units
 
    if GNATprove_Mode then
       declare
-         Unused_E : Entity_Id;
+         Unused : Entity_Id;
+
       begin
-         --  Ensure that System.Interrupt_Priority is available to
-         --  GNATprove for the generation of VCs related to ceiling
-         --  priority.
-         Unused_E := RTE (RE_Interrupt_Priority);
+         --  Ensure that System.Interrupt_Priority is available to GNATprove
+         --  for the generation of VCs related to ceiling priority.
+
+         Unused := RTE (RE_Interrupt_Priority);
       end;
    end if;
 
-   --  Qualify all entity names in inner packages, package bodies, etc.
+   --  Qualify all entity names in inner packages, package bodies, etc
 
    Exp_Dbug.Qualify_All_Entity_Names;
 

gcc/ada/sem_attr.adb

@@ -7109,13 +7109,14 @@ package body Sem_Attr is
 
       end case;
 
-      --  In SPARK some attribute references depend on Tasking_State, so we
-      --  need to make sure we load this so that gnat2why has the entity
-      --  available. See SPARK RM 9(18) for the relevant rule.
+      --  In SPARK certain attributes (see below) depend on Tasking_State.
+      --  Ensure that the entity is available for gnat2why by loading it.
+      --  See SPARK RM 9(18) for the relevant rule.
 
       if GNATprove_Mode then
          declare
             Unused : Entity_Id;
+
          begin
             case Attr_Id is
                when Attribute_Callable   |

gcc/ada/sem_ch13.adb

@@ -11603,11 +11603,18 @@ package body Sem_Ch13 is
 
       function Is_Type_Ref (N : Node_Id) return Boolean;
       pragma Inline (Is_Type_Ref);
+
       --  Returns True if N is a reference to the type for the predicate in the
       --  expression (i.e. if it is an identifier whose Chars field matches the
       --  Nam given in the call). N must not be parenthesized, if the type name
       --  appears in parens, this routine will return False.
 
+      --  The routine also returns True for function calls generated during the
+      --  expansion of comparison operators on strings, which are intended to
+      --  be legal in static predicates, and are converted into calls to array
+      --  comparison routines in the body of the corresponding predicate
+      --  function.
+
       ----------------------------------
       -- All_Static_Case_Alternatives --
       ----------------------------------
@@ -11671,9 +11678,10 @@ package body Sem_Ch13 is
 
       function Is_Type_Ref (N : Node_Id) return Boolean is
       begin
-         return Nkind (N) = N_Identifier
-           and then Chars (N) = Nam
-           and then Paren_Count (N) = 0;
+         return (Nkind (N) = N_Identifier
+                  and then Chars (N) = Nam
+                  and then Paren_Count (N) = 0)
+           or else Nkind (N) = N_Function_Call;
       end Is_Type_Ref;
 
    --  Start of processing for Is_Predicate_Static
@@ -11723,10 +11731,12 @@ package body Sem_Ch13 is
       --  and inequality operations to be valid on strings (this helps deal
       --  with cases where we transform A in "ABC" to A = "ABC).
 
+      --  In fact, it appears that the intent of the ARG is to extend static
+      --  predicates to strings, and that the extension should probably apply
+      --  to static expressions themselves. The code below accepts comparison
+      --  operators that apply to static strings.
+
       elsif Nkind (Expr) in N_Op_Compare
-        and then ((not Is_String_Type (Etype (Left_Opnd (Expr))))
-                    or else (Nkind_In (Expr, N_Op_Eq, N_Op_Ne)
-                              and then not Comes_From_Source (Expr)))
         and then ((Is_Type_Ref (Left_Opnd (Expr))
                     and then Is_OK_Static_Expression (Right_Opnd (Expr)))
                   or else
@@ -12323,7 +12333,7 @@ package body Sem_Ch13 is
            and then From_Aspect_Specification (N)
          then
             Error_Msg_NE
-              ("aspect specification causes premature freezing of&", T, N);
+              ("aspect specification causes premature freezing of&", N, T);
             Set_Has_Delayed_Freeze (T, False);
             return True;
          end if;

gcc/ada/sem_ch8.adb

@@ -1936,6 +1936,12 @@ package body Sem_Ch8 is
       is
          Loc : constant Source_Ptr := Sloc (N);
 
+         function Build_Call
+           (Subp_Id : Entity_Id;
+            Params  : List_Id) return Node_Id;
+         --  Create a dispatching call to invoke routine Subp_Id with actuals
+         --  built from the parameter specifications of list Params.
+
          function Build_Expr_Fun_Call
            (Subp_Id : Entity_Id;
             Params  : List_Id) return Node_Id;
@@ -1944,12 +1950,6 @@ package body Sem_Ch8 is
          --  directly the call, so that it can be used inside an expression
          --  function. This is a specificity of the GNATprove mode.
 
-         function Build_Call
-           (Subp_Id : Entity_Id;
-            Params  : List_Id) return Node_Id;
-         --  Create a dispatching call to invoke routine Subp_Id with actuals
-         --  built from the parameter specifications of list Params.
-
          function Build_Spec (Subp_Id : Entity_Id) return Node_Id;
          --  Create a subprogram specification based on the subprogram profile
          --  of Subp_Id.
@@ -2027,6 +2027,8 @@ package body Sem_Ch8 is
             Formal   : Node_Id;
 
          begin
+            pragma Assert (Ekind_In (Subp_Id, E_Function, E_Operator));
+
             --  Build the actual parameters of the call
 
             Formal := First (Params);
@@ -2039,11 +2041,10 @@ package body Sem_Ch8 is
             --  Generate:
             --    Subp_Id (Actuals);
 
-            pragma Assert (Ekind_In (Subp_Id, E_Function, E_Operator));
-
-            return Make_Function_Call (Loc,
-              Name                   => Call_Ref,
-              Parameter_Associations => Actuals);
+            return
+              Make_Function_Call (Loc,
+                Name                   => Call_Ref,
+                Parameter_Associations => Actuals);
          end Build_Expr_Fun_Call;
 
          ----------------
@@ -2399,9 +2400,10 @@ package body Sem_Ch8 is
             Body_Decl :=
               Make_Expression_Function (Loc,
                 Specification => New_Spec,
-                Expression    => Build_Expr_Fun_Call
-                  (Subp_Id => Prim_Op,
-                   Params  => Parameter_Specifications (New_Spec)));
+                Expression    =>
+                  Build_Expr_Fun_Call
+                    (Subp_Id => Prim_Op,
+                     Params  => Parameter_Specifications (New_Spec)));
 
             Wrap_Id := Defining_Entity (Body_Decl);
 

gcc/ada/sem_eval.adb

@@ -5469,6 +5469,40 @@ package body Sem_Eval is
                return Skip;
             end;
 
+         --  The predicate function may contain string-comparison operations
+         --  that have been converted into calls to run-time array-comparison
+         --  routines. To evaluate the predicate statically, we recover the
+         --  original comparison operation and replace the occurrence of the
+         --  formal by the static string value. The actuals of the generated
+         --  call are of the form X'Address.
+
+         elsif Nkind (N) in N_Op_Compare
+           and then Nkind (Left_Opnd (N)) = N_Function_Call
+         then
+            declare
+               C : constant Node_Id := Left_Opnd (N);
+               F : constant Node_Id := First (Parameter_Associations (C));
+               L : constant Node_Id := Prefix (F);
+               R : constant Node_Id := Prefix (Next (F));
+
+            begin
+               --  If an operand is an entity name, it is the formal of the
+               --  predicate function, so replace it with the string value.
+               --  It may be either operand in the call. The other operand
+               --  is a static string from the original predicate.
+
+               if Is_Entity_Name (L) then
+                  Rewrite (Left_Opnd (N),  New_Copy (Val));
+                  Rewrite (Right_Opnd (N), New_Copy (R));
+
+               else
+                  Rewrite (Left_Opnd (N),  New_Copy (L));
+                  Rewrite (Right_Opnd (N), New_Copy (Val));
+               end if;
+
+               return Skip;
+            end;
+
          else
             return OK;
          end if;

gcc/ada/sem_res.adb

@@ -4336,9 +4336,9 @@ package body Sem_Res is
                      Apply_Scalar_Range_Check
                        (Expression (A), Etype (Expression (A)), A_Typ);
 
-                     --  In addition, the returned value of the parameter
-                     --  must satisfy the bounds of the object type (see
-                     --  comment below).
+                     --  In addition, the returned value of the parameter must
+                     --  satisfy the bounds of the object type (see comment
+                     --  below).
 
                      Apply_Scalar_Range_Check (A, A_Typ, F_Typ);