sem_util.adb (Check_Result_And_Post_State): Do not issue a warning about missing…

sem_util.adb (Check_Result_And_Post_State): Do not issue a warning about missing reference to an outcome if...

2017-09-11  Yannick Moy  <moy@adacore.com>

	* sem_util.adb (Check_Result_And_Post_State):
	Do not issue a warning about missing reference to an outcome if
	the subprogram is ghost and has no outputs.
	* lib-xref-spark_specific.adb, sem_aggr.adb, sem_aux.ads: Minor
	reformatting.

From-SVN: r251960

gcc/ada/ChangeLog

 2017-09-11  Yannick Moy  <moy@adacore.com>
 
+	* sem_util.adb (Check_Result_And_Post_State):
+	Do not issue a warning about missing reference to an outcome if
+	the subprogram is ghost and has no outputs.
+	* lib-xref-spark_specific.adb, sem_aggr.adb, sem_aux.ads: Minor
+        reformatting.
+
+2017-09-11  Yannick Moy  <moy@adacore.com>
+
 	* gnat1drv.adb (Adjust_Global_Switches): Set
 	Check_Validity_Of_Parameters to False in GNATprove mode.
 	* opt.ads (Check_Validity_Of_Parameters): Document switch to

gcc/ada/sem_aggr.adb

@@ -4022,7 +4022,6 @@ package body Sem_Aggr is
       -------------------
 
       procedure Rewrite_Range (Root_Type : Entity_Id; Rge : Node_Id) is
-
          procedure Rewrite_Bound
            (Bound     : Node_Id;
             Disc      : Entity_Id;
@@ -4064,8 +4063,7 @@ package body Sem_Aggr is
             High := High_Bound (Rge);
 
             Disc      := First_Discriminant (Root_Type);
-            Expr_Disc :=
-              First_Elmt (Stored_Constraint (Etype (N)));
+            Expr_Disc := First_Elmt (Stored_Constraint (Etype (N)));
             while Present (Disc) loop
                Rewrite_Bound (Low, Disc, Node (Expr_Disc));
                Rewrite_Bound (High, Disc, Node (Expr_Disc));
@@ -4081,9 +4079,9 @@ package body Sem_Aggr is
       --  Components is the list of the record components whose value must be
       --  provided in the aggregate. This list does include discriminants.
 
-      Expr            : Node_Id;
       Component       : Entity_Id;
       Component_Elmt  : Elmt_Id;
+      Expr            : Node_Id;
       Positional_Expr : Node_Id;
 
    --  Start of processing for Resolve_Record_Aggregate
@@ -4669,9 +4667,10 @@ package body Sem_Aggr is
 
                   if Is_Array_Type (Etype (Expr)) then
                      declare
-                        --  Root record type whose discriminants may be used
-                        --  as bounds in range nodes.
-                        Root_Type : constant Entity_Id := Scope (Component);
+                        Rec_Typ : constant Entity_Id := Scope (Component);
+                        --  Root record type whose discriminants may be used as
+                        --  bounds in range nodes.
+
                         Index : Node_Id;
 
                      begin
@@ -4680,9 +4679,10 @@ package body Sem_Aggr is
 
                         Index := First_Index (Etype (Expr));
                         while Present (Index) loop
-                           Rewrite_Range (Root_Type, Index);
+                           Rewrite_Range (Rec_Typ, Index);
                            Rewrite_Range
-                             (Root_Type, Scalar_Range (Etype (Index)));
+                             (Rec_Typ, Scalar_Range (Etype (Index)));
+
                            Next_Index (Index);
                         end loop;
 
@@ -4692,7 +4692,7 @@ package body Sem_Aggr is
                         if Nkind (Expr) = N_Aggregate
                           and then Present (Aggregate_Bounds (Expr))
                         then
-                           Rewrite_Range (Root_Type, Aggregate_Bounds (Expr));
+                           Rewrite_Range (Rec_Typ, Aggregate_Bounds (Expr));
                         end if;
                      end;
                   end if;

gcc/ada/sem_aux.ads

@@ -162,7 +162,8 @@ package Sem_Aux is
    --  (Op) /= E_Operator.
 
    function Get_Called_Entity (Call : Node_Id) return Entity_Id;
-   --  Returns the entity associated with the call
+   --  Obtain the entity of the entry, operator, or subprogram being invoked
+   --  by call Call.
 
    function Get_Low_Bound (E : Entity_Id) return Node_Id;
    --  For an index subtype or string literal subtype, returns its low bound

gcc/ada/sem_util.adb

@@ -3501,6 +3501,14 @@ package body Sem_Util is
             --  Returns True if the message applies to a conjunct in the
             --  expression, instead of the whole expression.
 
+            function Has_Global_Output (Subp : Entity_Id) return Boolean;
+            --  Returns True if Subp has an output in its Global contract
+
+            function Has_No_Output (Subp : Entity_Id) return Boolean;
+            --  Returns True if Subp has no declared output: no function
+            --  result, no output parameter, and no output in its Global
+            --  contract.
+
             --------------------
             -- Adjust_Message --
             --------------------
@@ -3534,6 +3542,96 @@ package body Sem_Util is
                  or else Split_PPC (Prag);
             end Applied_On_Conjunct;
 
+            -----------------------
+            -- Has_Global_Output --
+            -----------------------
+
+            function Has_Global_Output (Subp : Entity_Id) return Boolean is
+               Global : constant Node_Id := Get_Pragma (Subp, Pragma_Global);
+               List   : Node_Id;
+               Assoc  : Node_Id;
+
+            begin
+               if No (Global) then
+                  return False;
+               end if;
+
+               List := Expression (Get_Argument (Global, Subp));
+
+               --  Empty list (no global items) or single global item
+               --  declaration (only input items).
+
+               if Nkind_In (List, N_Null,
+                                  N_Expanded_Name,
+                                  N_Identifier,
+                                  N_Selected_Component)
+               then
+                  return False;
+
+               --  Simple global list (only input items) or moded global list
+               --  declaration.
+
+               elsif Nkind (List) = N_Aggregate then
+                  if Present (Expressions (List)) then
+                     return False;
+
+                  else
+                     Assoc := First (Component_Associations (List));
+                     while Present (Assoc) loop
+                        if Chars (First (Choices (Assoc))) /= Name_Input then
+                           return True;
+                        end if;
+
+                        Next (Assoc);
+                     end loop;
+
+                     return False;
+                  end if;
+
+               --  To accommodate partial decoration of disabled SPARK
+               --  features, this routine may be called with illegal input.
+               --  If this is the case, do not raise Program_Error.
+
+               else
+                  return False;
+               end if;
+            end Has_Global_Output;
+
+            -------------------
+            -- Has_No_Output --
+            -------------------
+
+            function Has_No_Output (Subp : Entity_Id) return Boolean is
+               Param : Node_Id;
+
+            begin
+               --  A function has its result as output
+
+               if Ekind (Subp) = E_Function then
+                  return False;
+               end if;
+
+               --  An OUT or IN OUT parameter is an output
+
+               Param := First_Formal (Subp);
+               while Present (Param) loop
+                  if Ekind_In (Param, E_Out_Parameter, E_In_Out_Parameter) then
+                     return False;
+                  end if;
+
+                  Next_Formal (Param);
+               end loop;
+
+               --  An item of mode Output or In_Out in the Global contract is
+               --  an output.
+
+               if Has_Global_Output (Subp) then
+                  return False;
+               end if;
+
+               return True;
+            end Has_No_Output;
+
             --  Local variables
 
             Err_Node : Node_Id;
@@ -3549,8 +3647,14 @@ package body Sem_Util is
                Err_Node := Prag;
             end if;
 
+            --  Do not report missing reference to outcome in postcondition if
+            --  either the postcondition is trivially True or False, or if the
+            --  subprogram is ghost and has no declared output.
+
             if not Is_Trivial_Boolean (Expr)
               and then not Mentions_Post_State (Expr)
+              and then not (Is_Ghost_Entity (Subp_Id)
+                             and then Has_No_Output (Subp_Id))
             then
                if Pragma_Name (Prag) = Name_Contract_Cases then
                   Error_Msg_NE (Adjust_Message
@@ -17303,13 +17407,6 @@ package body Sem_Util is
    function NCT_Table_Hash (Key : Node_Or_Entity_Id) return NCT_Table_Index;
    --  Obtain the hash value of node or entity Key
 
-   NCT_Tables_In_Use : Boolean := False;
-   --  This flag keeps track of whether the two tables NCT_New_Entities and
-   --  NCT_Pending_Itypes are in use. The flag is part of an optimization
-   --  where certain operations are not performed if the tables are not in
-   --  use. This saves up to 8% of the entire compilation time spent in the
-   --  front end.
-
    --------------------
    -- NCT_Table_Hash --
    --------------------
@@ -17357,6 +17454,13 @@ package body Sem_Util is
      Hash       => NCT_Table_Hash,
      Equal      => "=");
 
+   NCT_Tables_In_Use : Boolean := False;
+   --  This flag keeps track of whether the two tables NCT_New_Entities and
+   --  NCT_Pending_Itypes are in use. The flag is part of an optimization
+   --  where certain operations are not performed if the tables are not in
+   --  use. This saves up to 8% of the entire compilation time spent in the
+   --  front end.
+
    -------------------
    -- New_Copy_Tree --
    -------------------