From 13126368df2c6784969c126425d8ae03e4f1d284 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 11 Sep 2017 08:37:51 +0000 Subject: [PATCH] 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 * 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 | 8 ++ gcc/ada/lib-xref-spark_specific.adb | 6 +- gcc/ada/sem_aggr.adb | 24 +++--- gcc/ada/sem_aux.ads | 3 +- gcc/ada/sem_util.adb | 118 ++++++++++++++++++++++++++-- 5 files changed, 136 insertions(+), 23 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 81a0d9d4c75..4b62600d5cb 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2017-09-11 Yannick Moy + + * 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 * gnat1drv.adb (Adjust_Global_Switches): Set diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 8cb262872ef..7542d238224 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -539,9 +539,9 @@ package body SPARK_Specific is function Is_SPARK_Scope (E : Entity_Id) return Boolean is Can_Be_Renamed : constant Boolean := - Present (E) - and then (Is_Subprogram_Or_Entry (E) - or else Ekind (E) = E_Package); + Present (E) + and then (Is_Subprogram_Or_Entry (E) + or else Ekind (E) = E_Package); begin return Present (E) and then not Is_Generic_Unit (E) diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index aa2510dd943..c885ce91451 100644 --- a/gcc/ada/sem_aggr.adb +++ b/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; @@ -4063,9 +4062,8 @@ package body Sem_Aggr is Low := Low_Bound (Rge); High := High_Bound (Rge); - Disc := First_Discriminant (Root_Type); - Expr_Disc := - First_Elmt (Stored_Constraint (Etype (N))); + Disc := First_Discriminant (Root_Type); + 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,10 +4667,11 @@ 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); - Index : Node_Id; + Rec_Typ : constant Entity_Id := Scope (Component); + -- Root record type whose discriminants may be used as + -- bounds in range nodes. + + Index : Node_Id; begin -- Rewrite the range nodes occurring in the indexes @@ -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; diff --git a/gcc/ada/sem_aux.ads b/gcc/ada/sem_aux.ads index a1e38ee0fd4..2ab9ef6199b 100644 --- a/gcc/ada/sem_aux.ads +++ b/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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index fcb9453c818..97c83a26bfc 100644 --- a/gcc/ada/sem_util.adb +++ b/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 -- ------------------- -- 2.30.2