From cf3e6845fd41439d52fb06791dbf13785be3db75 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Wed, 29 Jan 2014 16:20:44 +0100 Subject: [PATCH] [multiple changes] 2014-01-29 Robert Dewar * sem_ch7.adb, sem_prag.adb, sem_ch4.adb, sem_ch6.adb: Minor code reorganization. 2014-01-29 Yannick Moy * gnat_rm.texi: Update description of SPARK_Mode pragma. 2014-01-29 Tristan Gingold * exp_ch9.adb (Expand_N_Protected_Body): Remove Num_Entries. From-SVN: r207243 --- gcc/ada/ChangeLog | 13 +++++ gcc/ada/exp_ch9.adb | 3 -- gcc/ada/gnat_rm.texi | 131 ++++++++++++++++----------------------------------- gcc/ada/sem_ch4.adb | 4 +- gcc/ada/sem_ch6.adb | 28 +++++------ gcc/ada/sem_ch7.adb | 28 ++++++----- gcc/ada/sem_prag.adb | 11 +++-- 7 files changed, 92 insertions(+), 126 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8987a17..23fc402 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,16 @@ +2014-01-29 Robert Dewar + + * sem_ch7.adb, sem_prag.adb, sem_ch4.adb, sem_ch6.adb: Minor code + reorganization. + +2014-01-29 Yannick Moy + + * gnat_rm.texi: Update description of SPARK_Mode pragma. + +2014-01-29 Tristan Gingold + + * exp_ch9.adb (Expand_N_Protected_Body): Remove Num_Entries. + 2014-01-29 Thomas Quinot * sem_ch4.adb (Find_Component_In_Instance): Update comment. diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index b85dd01..694569d 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -8436,7 +8436,6 @@ package body Exp_Ch9 is Current_Node : Node_Id; Disp_Op_Body : Node_Id; New_Op_Body : Node_Id; - Num_Entries : Natural := 0; Op_Body : Node_Id; Op_Id : Entity_Id; @@ -8625,8 +8624,6 @@ package body Exp_Ch9 is when N_Entry_Body => Op_Id := Defining_Identifier (Op_Body); - Num_Entries := Num_Entries + 1; - New_Op_Body := Build_Protected_Entry (Op_Body, Op_Id, Pid); Insert_After (Current_Node, New_Op_Body); diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 6f04498..abb0038 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -6309,124 +6309,75 @@ pragma SPARK_Mode [(On | Off)] ; @end smallexample @noindent -This pragma is used to specify whether a construct must -satisfy the syntactic and semantic rules of the SPARK 2014 programming -language. The pragma is intended for use with formal verification tools -and has no effect on the generated code. +In general a program can have some parts that are in SPARK 2014 (and +follow all the rules in the SPARK Reference Manual), and some parts +that are full Ada 2012. -The SPARK_Mode pragma is used to specify the value of the SPARK_Mode aspect -(either Off or On) of an entity. -More precisely, it is used to specify the aspect value of a ``section'' -of an entity (the term ``section'' is defined below). -If a Spark_Mode pragma's (optional) argument is omitted, -an implicit argument of On is assumed. - -A SPARK_Mode pragma may be used as a configuration pragma and then has the -semantics described below. - -A SPARK_Mode pragma can be used as a local pragma only -in the following contexts: +The SPARK_Mode pragma is used to identify which parts are in SPARK +2014 (by default programs are in full Ada). The SPARK_Mode pragma can +be used in the following places: @itemize @bullet @item -When the pragma is at the start of the visible declarations (preceded only -by other pragmas) of a package declaration, it marks the visible part -of the package as being in or out of SPARK 2014. +As a configuration pragma, in which case it sets the default mode for +all units compiled with this pragma. @item -When the pragma appears at the start of the private declarations of a -package (preceded only by other pragmas), it marks the private part -of the package as being in or out of SPARK 2014. +Immediately following a library-level subprogram spec @item -When the pragma appears at the start of the declarations of a -package body (preceded only by other pragmas), -it marks the declaration list of the package body body as being -in or out of SPARK 2014. +Immediately within a library-level package body @item -When the pragma appears at the start of the elaboration statements of -a package body (preceded only by other pragmas), -it marks the handled_sequence_of_statements of the package body -as being in or out of SPARK 2014. +Immediately following the @code{private} keyword of a library-level +package spec @item -When the pragma appears after a subprogram declaration (with only other -pragmas intervening), it marks the subprogram's specification as -being in or out of SPARK 2014. +Immediately following the @code{begin} keyword of a library-level +package body @item -When the pragma appears at the start of the declarations of a subprogram -body (preceded only by other pragmas), it marks the subprogram body -as being in or out of SPARK 2014. For a subprogram body which is -not a completion of another declaration, it also applies to the -specification of the subprogram. +Immediately within a library-level subprogram body @end itemize -A package is defined to have 4 ``sections'': its visible part, its private -part, its body's declaration list, and its body's -handled_sequence_of_statements. Any other construct which requires a -completion is defined to have 2 ``sections'': its declaration and its -completion. Any other construct is defined to have 1 section. +@noindent +Normally a subprogram or package spec/body inherits the current mode +that is active at the point it is declared. But this can be overridden +by pragma within the spec or body as above. -The SPARK_Mode aspect value of an arbitrary section of an arbitrary Ada entity -or construct is then defined to be the following value: +The basic consistency rule is that you can't turn SPARK_Mode back +@code{On}, once you have explicitly (with a pragma) turned if +@code{Off}. So the following rules apply: -@itemize +@noindent +If a subprogram spec has SPARK_Mode @code{Off}, then the body must +also have SPARK_Mode @code{Off}. -@item -If SPARK_Mode has been specified for the given section of the given entity or -construct, then the specified value; +@noindent +For a package, we have four parts: +@itemize @item -else if SPARK_Mode has been specified for at least one preceding section of -the same entity, then the SPARK_Mode of the immediately preceding section; - +the package public declarations @item -else for any of the visible part or body declarations of a library unit package -or either section of a library unit subprogram, if there is an applicable -SPARK_Mode configuration pragma then the value specified by the -pragma; if no such configuration pragma applies, then an implicit -specification of Off is assumed; - +the package private part @item -else for any subsequent (i.e., not the first) section of a library unit -package, the SPARK_Mode of the preceding section; - +the body of the package @item -else the SPARK_Mode of the enclosing section of the nearest enclosing package -or subprogram; - +the elaboration code after @code{begin} @end itemize -If the above computation does not specify a SPARK_Mode setting for any -construct other than one of the four sections of a package, then a result of On -or Off is determined instead based on the legality (with respect to the rules -of SPARK 2014) of the construct. The construct's SPARK_Mode is On if and only -if the construct is in SPARK 2014. - -If an earlier section of an entity has a Spark_Mode of Off, then the -Spark_Mode aspect of any later section of that entity shall not be -specified to be On. For example, -if the specification of a subprogram has a Spark_Mode of Off, then the -body of the subprogram shall not have a Spark_Mode of On. - -The following rules apply to SPARK code (i.e., constructs which -have a SPARK_Mode aspect value of On): - -@itemize - -@item -SPARK code shall only reference SPARK declarations, but a SPARK declaration -which requires a completion may have a non-SPARK completion. - -@item -SPARK code shall only enclose SPARK code, except that SPARK code may enclose -a non-SPARK completion of an enclosed SPARK declaration. - -@end itemize +@noindent +For a package, the rule is that if you explicitly turn SPARK_Mode +@code{Off} for any part, then all the following parts must have +SPARK_Mode @code{Off}. Note that this may require repeating a pragma +SPARK_Mode (@code{Off}) in the body. For example, if we have a +configuration pragma SPARK_Mode (@code{On}) that turns the mode on by +default everywhere, and one particular package spec has pragma +SPARK_Mode (@code{Off}), then that pragma will need to be repeated in +the package body. @node Pragma Static_Elaboration_Desired @unnumberedsec Pragma Static_Elaboration_Desired diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 7c0a0cc..c7fc432 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -3972,7 +3972,9 @@ package body Sem_Ch4 is Next_Component (Comp); end loop; - -- Need comment on what is going on when we fall through ??? + -- If we fall through, no match, so no changes made + + return; end Find_Component_In_Instance; ------------------------------ diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 77108b2..68775fb 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3260,7 +3260,7 @@ package body Sem_Ch6 is Error_Msg_N ("incorrect application of SPARK_Mode#", N); Error_Msg_Sloc := Sloc (SPARK_Pragma (Spec_Id)); Error_Msg_NE - ("\value Off was set for SPARK_Mode on & #", N, Spec_Id); + ("\value Off was set for SPARK_Mode on&#", N, Spec_Id); end if; elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then @@ -3270,8 +3270,7 @@ package body Sem_Ch6 is Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); Error_Msg_N ("incorrect application of SPARK_Mode#", N); Error_Msg_Sloc := Sloc (Spec_Id); - Error_Msg_NE - ("\no value was set for SPARK_Mode on & #", N, Spec_Id); + Error_Msg_NE ("\no value was set for SPARK_Mode on&#", N, Spec_Id); end if; end if; @@ -3348,12 +3347,11 @@ package body Sem_Ch6 is -- the body of the procedure. But first we deal with a special case -- where we want to modify this check. If the body of the subprogram -- starts with a raise statement or its equivalent, or if the body - -- consists entirely of a null statement, then it is pretty obvious - -- that it is OK to not reference the parameters. For example, this - -- might be the following common idiom for a stubbed function: - -- statement of the procedure raises an exception. In particular this - -- deals with the common idiom of a stubbed function, which might - -- appear as something like: + -- consists entirely of a null statement, then it is pretty obvious that + -- it is OK to not reference the parameters. For example, this might be + -- the following common idiom for a stubbed function: statement of the + -- procedure raises an exception. In particular this deals with the + -- common idiom of a stubbed function, which appears something like: -- function F (A : Integer) return Some_Type; -- X : Some_Type; @@ -3649,12 +3647,12 @@ package body Sem_Ch6 is New_Overloaded_Entity (Designator); Check_Delayed_Subprogram (Designator); - -- If the type of the first formal of the current subprogram is a - -- non-generic tagged private type, mark the subprogram as being a - -- private primitive. Ditto if this is a function with controlling - -- result, and the return type is currently private. In both cases, - -- the type of the controlling argument or result must be in the - -- current scope for the operation to be primitive. + -- If the type of the first formal of the current subprogram is a non- + -- generic tagged private type, mark the subprogram as being a private + -- primitive. Ditto if this is a function with controlling result, and + -- the return type is currently private. In both cases, the type of the + -- controlling argument or result must be in the current scope for the + -- operation to be primitive. if Has_Controlling_Result (Designator) and then Is_Private_Type (Etype (Designator)) diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 79cd31a..4b6a6e4 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -349,6 +349,7 @@ package body Sem_Ch7 is -- Set SPARK_Mode only for non-generic package if Ekind (Spec_Id) = E_Package then + -- Set SPARK_Mode from context Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); @@ -391,9 +392,9 @@ package body Sem_Ch7 is Inspect_Deferred_Constant_Completion (Declarations (N)); end if; - -- After declarations have been analyzed, the body has been set - -- its final value of SPARK_Mode. Check that SPARK_Mode for body - -- is consistent with SPARK_Mode for spec. + -- After declarations have been analyzed, the body has been set to have + -- the final value of SPARK_Mode. Check that the SPARK_Mode for the body + -- is consistent with the SPARK_Mode for the spec. if Present (SPARK_Pragma (Body_Id)) then if Present (SPARK_Aux_Pragma (Spec_Id)) then @@ -404,16 +405,16 @@ package body Sem_Ch7 is Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); Error_Msg_N ("incorrect application of SPARK_Mode#", N); Error_Msg_Sloc := Sloc (SPARK_Aux_Pragma (Spec_Id)); - Error_Msg_NE ("\value Off was set for SPARK_Mode on & #", - N, Spec_Id); + Error_Msg_NE + ("\value Off was set for SPARK_Mode on & #", N, Spec_Id); end if; else Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); Error_Msg_N ("incorrect application of SPARK_Mode#", N); Error_Msg_Sloc := Sloc (Spec_Id); - Error_Msg_NE ("\no value was set for SPARK_Mode on & #", - N, Spec_Id); + Error_Msg_NE + ("\no value was set for SPARK_Mode on & #", N, Spec_Id); end if; end if; @@ -539,12 +540,13 @@ package body Sem_Ch7 is function Has_Referencer (L : List_Id; Outer : Boolean) return Boolean; - -- Traverse the given list of declarations in reverse order. - -- Return True if a referencer is present. Return False if none is - -- found. The Outer parameter is True for the outer level call and - -- False for inner level calls for nested packages. If Outer is - -- True, then any entities up to the point of hitting a referencer - -- get their Is_Public flag cleared, so that the entities will be + -- Traverse given list of declarations in reverse order. Return + -- True if a referencer is present. Return False if none is found. + -- + -- The Outer parameter is True for the outer level call and False + -- for inner level calls for nested packages. If Outer is True, + -- then any entities up to the point of hitting a referencer get + -- their Is_Public flag cleared, so that the entities will be -- treated as static entities in the C sense, and need not have -- fully qualified names. Furthermore, if the referencer is an -- inlined subprogram that doesn't reference other subprograms, diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 1cc7fd2..b6846d4 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -18628,7 +18628,8 @@ package body Sem_Prag is procedure Check_Pragma_Conformance (Context_Pragma : Node_Id; Entity_Pragma : Node_Id; - Entity : Entity_Id) is + Entity : Entity_Id) + is begin if Present (Context_Pragma) then pragma Assert (Nkind (Context_Pragma) = N_Pragma); @@ -18654,15 +18655,17 @@ package body Sem_Prag is Error_Msg_N ("incorrect use of SPARK_Mode", Arg1); Error_Msg_Sloc := Sloc (Entity_Pragma); Error_Msg_NE - ("\value Off was set for SPARK_Mode on & #", + ("\value Off was set for SPARK_Mode on&#", Arg1, Entity); raise Pragma_Exit; end if; + else Error_Msg_N ("incorrect use of SPARK_Mode", Arg1); Error_Msg_Sloc := Sloc (Entity); - Error_Msg_NE ("\no value was set for SPARK_Mode on & #", - Arg1, Entity); + Error_Msg_NE + ("\no value was set for SPARK_Mode on&#", + Arg1, Entity); raise Pragma_Exit; end if; end if; -- 2.7.4