+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.
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;
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);
@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
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;
------------------------------
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
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;
-- 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;
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))
-- 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);
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
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;
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,
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);
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;
projects / gcc.git / commitdiff