From 1f55088db5038881cc4836ba600edb1bb8fe0141 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 18 Apr 2016 12:41:18 +0200 Subject: [multiple changes] 2016-04-18 Yannick Moy * sem_util.adb, sem_util.ads (Has_Full_Default_Initialization): used outside of GNATprove, hence it should not be removed. 2016-04-18 Hristian Kirtchev * sem_prag.adb (Analyze_Refinement_Clause): The refinement of an external abstract state can now mention non-external constituents. (Check_External_Property): Update all SPARK RM references. 2016-04-18 Bob Duff * exp_intr.adb: Remove some duplicated code. 2016-04-18 Yannick Moy * a-nudira.adb, a-nudira.ads, a-nuflra.adb, a-nuflra.ads: Mark package spec and body out of SPARK. 2016-04-18 Johannes Kanig * spark_xrefs.ads: Minor comment update. 2016-04-18 Johannes Kanig * gnat1drv.adb (Gnat1drv): Force loading of System unit for SPARK. 2016-04-18 Bob Duff * a-cuprqu.adb: Correction to previous change. If a new node is inserted at the front of the queue (because it is higher priority than the previous front node), we need to update Header.Next_Unequal -- not just in the case where the queue was previously empty. From-SVN: r235122 --- gcc/ada/ChangeLog | 38 ++++++++++++++++++ gcc/ada/a-cuprqu.adb | 9 ++++- gcc/ada/a-nudira.adb | 4 +- gcc/ada/a-nudira.ads | 4 +- gcc/ada/a-nuflra.adb | 6 ++- gcc/ada/a-nuflra.ads | 6 ++- gcc/ada/exp_intr.adb | 66 +----------------------------- gcc/ada/gnat1drv.adb | 14 +++++++ gcc/ada/sem_prag.adb | 78 ++++++++++++++---------------------- gcc/ada/sem_util.adb | 104 ++++++++++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_util.ads | 13 ++++++ gcc/ada/spark_xrefs.ads | 2 +- 12 files changed, 223 insertions(+), 121 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index fbdfabc..1269d30 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,41 @@ +2016-04-18 Yannick Moy + + * sem_util.adb, sem_util.ads (Has_Full_Default_Initialization): used + outside of GNATprove, hence it should not be removed. + +2016-04-18 Hristian Kirtchev + + * sem_prag.adb (Analyze_Refinement_Clause): + The refinement of an external abstract state can now mention + non-external constituents. + (Check_External_Property): Update all SPARK RM references. + +2016-04-18 Bob Duff + + * exp_intr.adb: Remove some duplicated code. + +2016-04-18 Yannick Moy + + * a-nudira.adb, a-nudira.ads, a-nuflra.adb, a-nuflra.ads: Mark + package spec and body out of SPARK. + +2016-04-18 Johannes Kanig + + * spark_xrefs.ads: Minor comment update. + +2016-04-18 Johannes Kanig + + * gnat1drv.adb (Gnat1drv): Force loading of System + unit for SPARK. + +2016-04-18 Bob Duff + + * a-cuprqu.adb: Correction to previous change. If a new node + is inserted at the front of the queue (because it is higher + priority than the previous front node), we need to update + Header.Next_Unequal -- not just in the case where the queue was + previously empty. + 2016-04-18 Bob Duff * a-cuprqu.ads: Change the representation of List_Type from a diff --git a/gcc/ada/a-cuprqu.adb b/gcc/ada/a-cuprqu.adb index fb02f09..7502aa9 100644 --- a/gcc/ada/a-cuprqu.adb +++ b/gcc/ada/a-cuprqu.adb @@ -187,10 +187,17 @@ package body Ada.Containers.Unbounded_Priority_Queues is Prev.Next.Prev := Node; Prev.Next := Node; - if List.Length = 0 then + if Prev = H then + + -- Make sure Next_Unequal of the Header always points to the first + -- "real" node. Here, we've inserted a new first "real" node, so + -- must update. + List.Header.Next_Unequal := Node; end if; + pragma Assert (List.Header.Next_Unequal = List.Header.Next); + List.Length := List.Length + 1; if List.Length > List.Max_Length then diff --git a/gcc/ada/a-nudira.adb b/gcc/ada/a-nudira.adb index 251f852..2e83600 100644 --- a/gcc/ada/a-nudira.adb +++ b/gcc/ada/a-nudira.adb @@ -29,7 +29,9 @@ -- -- ------------------------------------------------------------------------------ -package body Ada.Numerics.Discrete_Random is +package body Ada.Numerics.Discrete_Random with + SPARK_Mode => Off +is package SRN renames System.Random_Numbers; use SRN; diff --git a/gcc/ada/a-nudira.ads b/gcc/ada/a-nudira.ads index 77501ec..c2a7382 100644 --- a/gcc/ada/a-nudira.ads +++ b/gcc/ada/a-nudira.ads @@ -41,7 +41,9 @@ with System.Random_Numbers; generic type Result_Subtype is (<>); -package Ada.Numerics.Discrete_Random is +package Ada.Numerics.Discrete_Random with + SPARK_Mode => Off +is -- Basic facilities diff --git a/gcc/ada/a-nuflra.adb b/gcc/ada/a-nuflra.adb index 2c6fbc4..add19d4 100644 --- a/gcc/ada/a-nuflra.adb +++ b/gcc/ada/a-nuflra.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -29,7 +29,9 @@ -- -- ------------------------------------------------------------------------------ -package body Ada.Numerics.Float_Random is +package body Ada.Numerics.Float_Random with + SPARK_Mode => Off +is package SRN renames System.Random_Numbers; use SRN; diff --git a/gcc/ada/a-nuflra.ads b/gcc/ada/a-nuflra.ads index 5a448a7..ea4992c 100644 --- a/gcc/ada/a-nuflra.ads +++ b/gcc/ada/a-nuflra.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -38,7 +38,9 @@ with System.Random_Numbers; -package Ada.Numerics.Float_Random is +package Ada.Numerics.Float_Random with + SPARK_Mode => Off +is -- Basic facilities diff --git a/gcc/ada/exp_intr.adb b/gcc/ada/exp_intr.adb index b8f1fe4..f030782 100644 --- a/gcc/ada/exp_intr.adb +++ b/gcc/ada/exp_intr.adb @@ -852,11 +852,7 @@ package body Exp_Intr is ------------------------ procedure Expand_Source_Info (N : Node_Id; Nam : Name_Id) is - -- ???There is duplicated code here (see Add_Source_Info) - Loc : constant Source_Ptr := Sloc (N); - Ent : Entity_Id; - begin -- Integer cases @@ -870,67 +866,7 @@ package body Exp_Intr is else Name_Len := 0; - - case Nam is - when Name_File => - Get_Decoded_Name_String - (Reference_Name (Get_Source_File_Index (Loc))); - - when Name_Source_Location => - Build_Location_String (Loc); - - when Name_Enclosing_Entity => - - -- Skip enclosing blocks to reach enclosing unit - - Ent := Current_Scope; - while Present (Ent) loop - exit when Ekind (Ent) /= E_Block - and then Ekind (Ent) /= E_Loop; - Ent := Scope (Ent); - end loop; - - -- Ent now points to the relevant defining entity - - Write_Entity_Name (Ent); - - when Name_Compilation_ISO_Date => - Name_Buffer (1 .. 10) := Opt.Compilation_Time (1 .. 10); - Name_Len := 10; - - when Name_Compilation_Date => - declare - subtype S13 is String (1 .. 3); - Months : constant array (1 .. 12) of S13 := - ("Jan", "Feb", "Mar", "Apr", "May", "Jun", - "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"); - - M1 : constant Character := Opt.Compilation_Time (6); - M2 : constant Character := Opt.Compilation_Time (7); - - MM : constant Natural range 1 .. 12 := - (Character'Pos (M1) - Character'Pos ('0')) * 10 + - (Character'Pos (M2) - Character'Pos ('0')); - - begin - -- Reformat ISO date into MMM DD YYYY (__DATE__) format - - Name_Buffer (1 .. 3) := Months (MM); - Name_Buffer (4) := ' '; - Name_Buffer (5 .. 6) := Opt.Compilation_Time (9 .. 10); - Name_Buffer (7) := ' '; - Name_Buffer (8 .. 11) := Opt.Compilation_Time (1 .. 4); - Name_Len := 11; - end; - - when Name_Compilation_Time => - Name_Buffer (1 .. 8) := Opt.Compilation_Time (12 .. 19); - Name_Len := 8; - - when others => - raise Program_Error; - end case; - + Add_Source_Info (Loc, Nam); Rewrite (N, Make_String_Literal (Loc, Strval => String_From_Name_Buffer)); diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index b8ea585..29f2f94 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -1045,6 +1045,20 @@ begin Original_Operating_Mode := Operating_Mode; Frontend; + -- In GNATprove mode, force loading of System unit when tasking is + -- used, so that in particular System.Interrupt_Priority is available + -- to GNATprove for the generation of VCs for checking the respect of + -- Ceiling Protocol. + + if GNATprove_Mode and Opt.Tasking_Used then + declare + Unused_E : constant Entity_Id := + Rtsfind.RTE (Rtsfind.RE_Interrupt_Priority); + begin + null; + end; + end if; + -- Exit with errors if the main source could not be parsed if Sinput.Main_Source_File = No_Source_File then diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0197159..118d43d 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -25514,7 +25514,7 @@ package body Sem_Prag is Error_Msg_Name_1 := Prop_Nam; -- The property is enabled in the related Abstract_State pragma - -- that defines the state (SPARK RM 7.2.8(3)). + -- that defines the state (SPARK RM 7.2.8(2)). if Enabled then if No (Constit) then @@ -25525,7 +25525,7 @@ package body Sem_Prag is -- The property is missing in the declaration of the state, but -- a constituent is introducing it in the state refinement - -- (SPARK RM 7.2.8(3)). + -- (SPARK RM 7.2.8(2)). elsif Present (Constit) then Error_Msg_Name_2 := Chars (Constit); @@ -25746,49 +25746,31 @@ package body Sem_Prag is Analyze_Constituent (Constit); end if; - -- A refined external state is subject to special rules with respect - -- to its properties and constituents. + -- The set of properties that all external constituents yield must + -- match that of the refined state. There are two cases to detect: + -- the refined state lacks a property or has an extra property + -- (SPARK RM 7.2.8(2)). if Is_External_State (State_Id) then - - -- The set of properties that all external constituents yield must - -- match that of the refined state. There are two cases to detect: - -- the refined state lacks a property or has an extra property. - - if External_Constit_Seen then - Check_External_Property - (Prop_Nam => Name_Async_Readers, - Enabled => Async_Readers_Enabled (State_Id), - Constit => AR_Constit); - - Check_External_Property - (Prop_Nam => Name_Async_Writers, - Enabled => Async_Writers_Enabled (State_Id), - Constit => AW_Constit); - - Check_External_Property - (Prop_Nam => Name_Effective_Reads, - Enabled => Effective_Reads_Enabled (State_Id), - Constit => ER_Constit); - - Check_External_Property - (Prop_Nam => Name_Effective_Writes, - Enabled => Effective_Writes_Enabled (State_Id), - Constit => EW_Constit); - - -- An external state may be refined to null (SPARK RM 7.2.8(2)) - - elsif Null_Seen then - null; - - -- The external state has constituents, but none of them are - -- external (SPARK RM 7.2.8(2)). - - else - SPARK_Msg_NE - ("external state & requires at least one external " - & "constituent or null refinement", State, State_Id); - end if; + Check_External_Property + (Prop_Nam => Name_Async_Readers, + Enabled => Async_Readers_Enabled (State_Id), + Constit => AR_Constit); + + Check_External_Property + (Prop_Nam => Name_Async_Writers, + Enabled => Async_Writers_Enabled (State_Id), + Constit => AW_Constit); + + Check_External_Property + (Prop_Nam => Name_Effective_Reads, + Enabled => Effective_Reads_Enabled (State_Id), + Constit => ER_Constit); + + Check_External_Property + (Prop_Nam => Name_Effective_Writes, + Enabled => Effective_Writes_Enabled (State_Id), + Constit => EW_Constit); -- When a refined state is not external, it should not have external -- constituents (SPARK RM 7.2.8(1)). @@ -26760,17 +26742,17 @@ package body Sem_Prag is --------------------------------------------- procedure Collect_Inherited_Class_Wide_Conditions (Subp : Entity_Id) is - Parent_Subp : constant Entity_Id := Overridden_Operation (Subp); - Prags : constant Node_Id := Contract (Parent_Subp); + Parent_Subp : constant Entity_Id := Overridden_Operation (Subp); + Prags : constant Node_Id := Contract (Parent_Subp); + In_Spec_Expr : Boolean; + Installed : Boolean; Prag : Node_Id; New_Prag : Node_Id; - Installed : Boolean; - In_Spec_Expr : Boolean; begin Installed := False; - -- Iterate over the contract of the overridden subprogram to find + -- Iterate over the contract of the overridden subprogram to find all -- inherited class-wide pre- and postconditions. if Present (Prags) then diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 35b0888..1146b9d 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -9046,6 +9046,110 @@ package body Sem_Util is end if; end Has_Enabled_Property; + ------------------------------------- + -- Has_Full_Default_Initialization -- + ------------------------------------- + + function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is + Arg : Node_Id; + Comp : Entity_Id; + Prag : Node_Id; + + begin + -- A private type and its full view is fully default initialized when it + -- is subject to pragma Default_Initial_Condition without an argument or + -- with a non-null argument. Since any type may act as the full view of + -- a private type, this check must be performed prior to the specialized + -- tests below. + + if Has_Default_Init_Cond (Typ) + or else Has_Inherited_Default_Init_Cond (Typ) + then + Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition); + + -- Pragma Default_Initial_Condition must be present if one of the + -- related entity flags is set. + + pragma Assert (Present (Prag)); + Arg := First (Pragma_Argument_Associations (Prag)); + + -- A non-null argument guarantees full default initialization + + if Present (Arg) then + return Nkind (Arg) /= N_Null; + + -- Otherwise the missing argument defaults the pragma to "True" which + -- is considered a non-null argument (see above). + + else + return True; + end if; + end if; + + -- A scalar type is fully default initialized if it is subject to aspect + -- Default_Value. + + if Is_Scalar_Type (Typ) then + return Has_Default_Aspect (Typ); + + -- An array type is fully default initialized if its element type is + -- scalar and the array type carries aspect Default_Component_Value or + -- the element type is fully default initialized. + + elsif Is_Array_Type (Typ) then + return + Has_Default_Aspect (Typ) + or else Has_Full_Default_Initialization (Component_Type (Typ)); + + -- A protected type, record type or type extension is fully default + -- initialized if all its components either carry an initialization + -- expression or have a type that is fully default initialized. The + -- parent type of a type extension must be fully default initialized. + + elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then + + -- Inspect all entities defined in the scope of the type, looking for + -- uninitialized components. + + Comp := First_Entity (Typ); + while Present (Comp) loop + if Ekind (Comp) = E_Component + and then Comes_From_Source (Comp) + and then No (Expression (Parent (Comp))) + and then not Has_Full_Default_Initialization (Etype (Comp)) + then + return False; + end if; + + Next_Entity (Comp); + end loop; + + -- Ensure that the parent type of a type extension is fully default + -- initialized. + + if Etype (Typ) /= Typ + and then not Has_Full_Default_Initialization (Etype (Typ)) + then + return False; + end if; + + -- If we get here, then all components and parent portion are fully + -- default initialized. + + return True; + + -- A task type is fully default initialized by default + + elsif Is_Task_Type (Typ) then + return True; + + -- Otherwise the type is not fully default initialized + + else + return False; + end if; + end Has_Full_Default_Initialization; + -------------------- -- Has_Infinities -- -------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index e868c83..d8a9b52 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1034,6 +1034,19 @@ package Sem_Util is -- Determine whether subprogram Subp_Id has an effectively volatile formal -- parameter or returns an effectively volatile value. + function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ defines "full default initialization" as + -- specified by SPARK RM 3.1. To qualify as such, the type must be + -- * A scalar type with specified Default_Value + -- * An array-of-scalar type with specified Default_Component_Value + -- * An array type whose element type defines full default initialization + -- * A protected type, record type or type extension whose components + -- either include a default expression or have a type which defines + -- full default initialization. In the case of type extensions, the + -- parent type defines full default initialization. + -- * A task type + -- * A private type whose Default_Initial_Condition is non-null + function Has_Infinities (E : Entity_Id) return Boolean; -- Determines if the range of the floating-point type E includes -- infinities. Returns False if E is not a floating-point type. diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index eb95f73..f02234f 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -200,7 +200,7 @@ package SPARK_Xrefs is -- not relate to Generated Globals. -- The processing (reading and writing) of this section happens in - -- package Flow_Computed_Globals (from the SPARK 2014 sources), for + -- package Flow_Generated_Globals (from the SPARK 2014 sources), for -- further information please refer there. ---------------- -- cgit v1.1