mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-08 19:20:44 +08:00
Code Issues Packages Projects Releases Wiki Activity

[multiple changes]

Browse Source 
2014-01-29  Robert Dewar  <dewar@adacore.com>

	* sem_ch7.adb, sem_prag.adb, sem_ch4.adb, sem_ch6.adb: Minor code
	reorganization.

2014-01-29  Yannick Moy  <moy@adacore.com>

	* gnat_rm.texi: Update description of SPARK_Mode pragma.

2014-01-29  Tristan Gingold  <gingold@adacore.com>

	* exp_ch9.adb (Expand_N_Protected_Body): Remove Num_Entries.

From-SVN: r207243
This commit is contained in:
Arnaud Charlet 2014-01-29 16:20:44 +01:00
parent f90d14ac69
commit cf3e6845fd
7 changed files with 93 additions and 127 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
gcc/ada/ChangeLog
View File

@ -1,3 +1,16 @@
2014-01-29 Robert Dewar <dewar@adacore.com>
* sem_ch7.adb, sem_prag.adb, sem_ch4.adb, sem_ch6.adb: Minor code
reorganization.
2014-01-29 Yannick Moy <moy@adacore.com>
* gnat_rm.texi: Update description of SPARK_Mode pragma.
2014-01-29 Tristan Gingold <gingold@adacore.com>
* exp_ch9.adb (Expand_N_Protected_Body): Remove Num_Entries.
2014-01-29 Thomas Quinot <quinot@adacore.com>
* sem_ch4.adb (Find_Component_In_Instance): Update comment.

3
gcc/ada/exp_ch9.adb
View File

@ -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);

133
gcc/ada/gnat_rm.texi
View File

@ -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:
@noindent
If a subprogram spec has SPARK_Mode @code{Off}, then the body must
also have SPARK_Mode @code{Off}.
@noindent
For a package, we have four parts:
@itemize
@item
If SPARK_Mode has been specified for the given section of the given entity or
construct, then the specified value;
the package public declarations
@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 private part
@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 body of the package
@item
else for any subsequent (i.e., not the first) section of a library unit
package, the SPARK_Mode of the preceding section;
@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

4
gcc/ada/sem_ch4.adb
View File

@ -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;
------------------------------

28
gcc/ada/sem_ch6.adb
View File

@ -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))

28
gcc/ada/sem_ch7.adb
View File

@ -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,

11
gcc/ada/sem_prag.adb
View File

@ -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;