+2013-07-08 Gary Dismukes <dismukes@adacore.com>
+
+ * freeze.adb: Minor typo fixes.
+
+2013-07-08 Robert Dewar <dewar@adacore.com>
+
+ * gnat_rm.texi: Document SPARK_05 (replaces SPARK) Document
+ obsolete recognition of SPARK Document all other obsolete synonyms
+ for old restrictions.
+ * restrict.adb (Check_SPARK_Restriction): SPARK_05 replaces
+ SPARK (Process_Restriction_Synonyms): Handle SPARK as synonym
+ for SPARK_05.
+ * restrict.ads: Restriction SPARK_05 replaces SPARK.
+ * s-rident.ads: Replace restriction SPARK by SPARK_05 Add SPARK
+ as synonym for SPARK_05.
+ * sem_prag.adb: Minor reformatting.
+ * snames.ads-tmpl: Add entries for Name_SPARK and Name_SPARK_05.
+
2013-07-08 Robert Dewar <dewar@adacore.com>
* sem_dim.adb: Minor error message change.
-- a size given for an array where the array needs to be packed,
-- but was not so the size cannot be honored. This is the case
-- where implicit packing may apply. The reason we do this so
- -- early is that if we have implicit packing, the lagout of the
+ -- early is that if we have implicit packing, the layout of the
-- base type is affected, so we must do this before we freeze
-- the base type.
-- We could do this processing only if implicit packing is enabled
-- since in all other cases, the error would be caught by the back
-- end. However, we choose to do the check even if we do not have
- -- implicit packingh enabled, since this allows us to give a more
- -- useful error message (advising the use of pack or the pragma).
+ -- implicit packing enabled, since this allows us to give a more
+ -- useful error message (advising use of pragmas Implicit_Packing
+ -- or Pack).
if Is_Array_Type (E) then
declare
* No_Implicit_Aliasing::
* No_Obsolescent_Features::
* No_Wide_Characters::
-* SPARK::
+* SPARK_05::
The Implementation of Standard I/O
restriction results in the raising of Program_Error exception at the point of
the call.
+@findex Max_Entry_Queue_Depth
+The restriction @code{Max_Entry_Queue_Depth} is recognized as a
+synonym for @code{Max_Entry_Queue_Length}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
@node Max_Protected_Entries
@unnumberedsubsec Max_Protected_Entries
@findex Max_Protected_Entries
(Is_Reserved, Is_Attached, Current_Handler, Attach_Handler, Exchange_Handler,
Detach_Handler, and Reference).
+@findex No_Dynamic_Interrupts
+The restriction @code{No_Dynamic_Interrupts} is recognized as a
+synonym for @code{No_Dynamic_Attachment}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
@node No_Dynamic_Priorities
@unnumberedsubsec No_Dynamic_Priorities
@findex No_Dynamic_Priorities
are permitted and prevents keyword @code{requeue} from being used in source
code.
+@findex No_Requeue
+The restriction @code{No_Requeue} is recognized as a
+synonym for @code{No_Requeue_Statements}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on oNobsolescent features are activated).
+
@node No_Secondary_Stack
@unnumberedsubsec No_Secondary_Stack
@findex No_Secondary_Stack
[GNAT] This restriction ensures at compile time that there are no implicit or
explicit dependencies on the package @code{Ada.Task_Attributes}.
+@findex No_Task_Attributes
+The restriction @code{No_Task_Attributes} is recognized as a synonym
+for @code{No_Task_Attributes_Package}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
@node No_Task_Hierarchy
@unnumberedsubsec No_Task_Hierarchy
@findex No_Task_Hierarchy
expressions or references to simple boolean variables defined in the private
part of the protected type. No other form of entry barriers is permitted.
+@findex Boolean_Entry_Barriers
+The restriction @code{Boolean_Entry_Barriers} is recognized as a
+synonym for @code{Simple_Barriers}. This is retained for historical
+compatibility purposes (and a warning will be generated for its use if
+warnings on obsolescent features are activated).
+
@node Static_Priorities
@unnumberedsubsec Static_Priorities
@findex Static_Priorities
* No_Implicit_Aliasing::
* No_Obsolescent_Features::
* No_Wide_Characters::
-* SPARK::
+* SPARK_05::
@end menu
@node No_Elaboration_Code
appear in the program (that is literals representing characters not in
type @code{Character}).
-@node SPARK
-@unnumberedsubsec SPARK
-@findex SPARK
+@node SPARK_05
+@unnumberedsubsec SPARK_05
+@findex SPARK_05
[GNAT] This restriction checks at compile time that some constructs
forbidden in SPARK 2005 are not present. Error messages related to
SPARK restriction have the form:
+@findex SPARK
+The restriction @code{SPARK} is recognized as a
+synonym for @code{SPARK_05}. This is retained for historical
+compatibility purposes (and an unconditional warning will be generated
+for its use, advising replacement by @code{SPARK}.
+
@smallexample
violation of restriction "SPARK" at <file>
<error message>
begin
if Force or else Comes_From_Source (Original_Node (N)) then
- if Restriction_Check_Required (SPARK)
+ if Restriction_Check_Required (SPARK_05)
and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
then
return;
-- restore the previous value of the global variable around the call.
Save_Error_Msg_Sloc := Error_Msg_Sloc;
- Check_Restriction (Msg_Issued, SPARK, First_Node (N));
+ Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
Error_Msg_Sloc := Save_Error_Msg_Sloc;
if Msg_Issued then
if Comes_From_Source (Original_Node (N)) then
- if Restriction_Check_Required (SPARK)
+ if Restriction_Check_Required (SPARK_05)
and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
then
return;
-- restore the previous value of the global variable around the call.
Save_Error_Msg_Sloc := Error_Msg_Sloc;
- Check_Restriction (Msg_Issued, SPARK, First_Node (N));
+ Check_Restriction (Msg_Issued, SPARK_05, First_Node (N));
Error_Msg_Sloc := Save_Error_Msg_Sloc;
if Msg_Issued then
when Name_No_Task_Attributes =>
New_Name := Name_No_Task_Attributes_Package;
+ -- SPARK is special in that we unconditionally warn
+
+ when Name_SPARK =>
+ Error_Msg_Name_1 := Name_SPARK;
+ Error_Msg_N ("restriction identifier % is obsolescent??", N);
+ Error_Msg_Name_1 := Name_SPARK_05;
+ Error_Msg_N ("|use restriction identifier % instead??", N);
+ return Name_SPARK_05;
+
when others =>
return Old_Name;
end case;
+ -- Output warning if we are warning on obsolescent features for all
+ -- cases other than SPARK.
+
if Warn_On_Obsolescent_Feature then
Error_Msg_Name_1 := Old_Name;
Error_Msg_N ("restriction identifier % is obsolescent?j?", N);
procedure Id_Case (S : String; Quotes : Boolean := True);
-- Given a string S, case it according to current identifier casing,
- -- except for SPARK (an acronym) which is set all upper case, and store
- -- in Error_Msg_String. Then append `~` to the message buffer to output
- -- the string unchanged surrounded in quotes. The quotes are suppressed
- -- if Quotes = False.
+ -- except for SPARK_05 (an acronym) which is set all upper case, and
+ -- store in Error_Msg_String. Then append `~` to the message buffer
+ -- to output the string unchanged surrounded in quotes. The quotes
+ -- are suppressed if Quotes = False.
--------------
-- Add_Char --
Name_Buffer (1 .. S'Last) := S;
Name_Len := S'Length;
- if R = SPARK then
+ if R = SPARK_05 then
Set_All_Upper_Case;
else
Set_Casing (Identifier_Casing (Get_Source_File_Index (Sloc (N))));
No_Wide_Characters => True,
Static_Priorities => True,
Static_Storage_Size => True,
- SPARK => True,
+ SPARK_05 => True,
others => False);
-- The following table records entries made by Restrictions pragmas
-- SPARK Restriction Control --
-------------------------------
- -- SPARK HIDE directives allow the effect of the SPARK restriction to be
+ -- SPARK HIDE directives allow the effect of the SPARK_05 restriction to be
-- turned off for a specified region of code, and the following tables are
-- the data structures used to keep track of these regions.
(Msg : String;
N : Node_Id;
Force : Boolean := False);
- -- Node N represents a construct not allowed in formal mode. If this is a
- -- source node, or if the restriction is forced (Force = True), and the
- -- SPARK restriction is set, then an error is issued on N. Msg is appended
- -- to the restriction failure message.
+ -- Node N represents a construct not allowed in formal mode. If this is
+ -- a source node, or if the restriction is forced (Force = True), and
+ -- the SPARK_05 restriction is set, then an error is issued on N. Msg
+ -- is appended to the restriction failure message.
procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id);
-- Same as Check_SPARK_Restriction except there is a continuation message
No_Elaboration_Code, -- GNAT
No_Obsolescent_Features, -- Ada 2005 AI-368
No_Wide_Characters, -- GNAT
- SPARK, -- GNAT
+ SPARK_05, -- GNAT
-- The following cases require a parameter value
No_Dynamic_Interrupts : Restriction_Id renames No_Dynamic_Attachment;
No_Requeue : Restriction_Id renames No_Requeue_Statements;
No_Task_Attributes : Restriction_Id renames No_Task_Attributes_Package;
+ SPARK : Restriction_Id renames SPARK_05;
subtype All_Restrictions is Restriction_Id range
Simple_Barriers .. Max_Storage_At_Blocking;
-- All restrictions (excluding only Not_A_Restriction_Id)
subtype All_Boolean_Restrictions is Restriction_Id range
- Simple_Barriers .. SPARK;
+ Simple_Barriers .. SPARK_05;
-- All restrictions which do not take a parameter
subtype Partition_Boolean_Restrictions is All_Boolean_Restrictions range
-- case of Boolean restrictions.
subtype Cunit_Boolean_Restrictions is All_Boolean_Restrictions range
- Immediate_Reclamation .. SPARK;
+ Immediate_Reclamation .. SPARK_05;
-- Boolean restrictions that are not checked for partition consistency
-- and that thus apply only to the current unit. Note that for these
-- restrictions, the compiler does not apply restrictions found in
-- Start of processing for Process_Restrictions_Or_Restriction_Warnings
begin
- -- Ignore all Restrictions pragma in CodePeer mode
+ -- Ignore all Restrictions pragmas in CodePeer mode
if CodePeer_Mode then
return;
Name_Semaphore : constant Name_Id := N + $;
Name_Short_Descriptor : constant Name_Id := N + $;
Name_Simple_Barriers : constant Name_Id := N + $;
+ Name_SPARK : constant Name_Id := N + $;
+ Name_SPARK_05 : constant Name_Id := N + $;
Name_Spec_File_Name : constant Name_Id := N + $;
Name_State : constant Name_Id := N + $;
Name_Statement_Assertions : constant Name_Id := N + $;