+2011-08-02 Robert Dewar <dewar@adacore.com>
+
+ * gnat_rm.texi: Minor reformatting.
+ * sem_prag.adb: Minor reformatting.
+
+2011-08-02 Tristan Gingold <gingold@adacore.com>
+
+ * vms_data.ads: Add VMS qualifier for -gnateP.
+
+2011-08-02 Robert Dewar <dewar@adacore.com>
+
+ * par-ch13.adb (P_Aspect_Specification): New meaning of Decl = Empty
+ * par-ch7.adb (P_Package): Proper placement of aspects for package
+ decl/instantiation.
+ * par-endh.adb (Check_End): Ad Is_Sloc parameter
+ (End_Statements): Add Is_Sloc parameterr
+ * par.adb (P_Aspect_Specification): New meaning of Decl = Empty
+ (Check_End): Ad Is_Sloc parameter
+ (End_Statements): Add Is_Sloc parameterr
+
+2011-08-02 Vincent Celier <celier@adacore.com>
+
+ * ug_words: Add VMS qualifier equivalent to -gnateP:
+ /SYMBOL_PREPROCESSING.
+
+2011-08-02 Jose Ruiz <ruiz@adacore.com>
+
+ * gnat-style.texi: For hexadecimal numeric literals the typical
+ grouping of digits is 4 to represent 2 bytes.
+ A procedure spec which is split into several lines is indented two
+ characters.
+
+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * exp_aggr.adb (Is_Others_Aggregate): move function to other unit.
+ * sem_aggr.adb, sem_aggr.ads (Is_Others_Aggregate): move function here
+ (Resolve_Aggregate): issue errors in formal modes when aggregate is not
+ properly qualified
+ (Resolve_Array_Aggregate): issue errors in formal modes on non-static
+ choice in array aggregate
+ (Resolve_Extension_Aggregate): issue errors in formal modes on subtype
+ mark as ancestor
+ (Resolve_Record_Aggregate): issue errors in formal modes on mixed
+ positional and named aggregate for record, or others in record
+ aggregate, or multiple choice in record aggregate
+ * sem_res.adb (Resolve_Logical_Op): issue errors in formal mode when
+ array operands to logical operations AND, OR and XOR do not have the
+ same static lower and higher bounds
+ * sem_ch5.adb, sinfo.ads: Correct typos in comments
+
2011-08-01 Robert Dewar <dewar@adacore.com>
* sem_util.ads, sem_util.adb, sem_ch6.adb (Last_Source_Statement):
with Rtsfind; use Rtsfind;
with Ttypes; use Ttypes;
with Sem; use Sem;
+with Sem_Aggr; use Sem_Aggr;
with Sem_Aux; use Sem_Aux;
with Sem_Ch3; use Sem_Ch3;
with Sem_Eval; use Sem_Eval;
Obj_Lo : Node_Id;
Obj_Hi : Node_Id;
- function Is_Others_Aggregate (Aggr : Node_Id) return Boolean;
- -- Aggregates that consist of a single Others choice are safe
- -- if the single expression is.
-
function Safe_Aggregate (Aggr : Node_Id) return Boolean;
-- Check recursively that each component of a (sub)aggregate does
-- not depend on the variable being assigned to.
-- Verify that an expression cannot depend on the variable being
-- assigned to. Room for improvement here (but less than before).
- -------------------------
- -- Is_Others_Aggregate --
- -------------------------
-
- function Is_Others_Aggregate (Aggr : Node_Id) return Boolean is
- begin
- return No (Expressions (Aggr))
- and then Nkind
- (First (Choices (First (Component_Associations (Aggr)))))
- = N_Others_Choice;
- end Is_Others_Aggregate;
-
--------------------
-- Safe_Aggregate --
--------------------
@smallexample
1_000_000
- 16#8000_000#
+ 16#8000_0000#
3.14159_26535_89793_23846
@end smallexample
@end itemize
@smallexample @c adanocomment
@group
procedure Set_Heading
- (Source : String;
- Count : Natural;
- Pad : Character := Space;
- Fill : Boolean := True);
+ (Source : String;
+ Count : Natural;
+ Pad : Character := Space;
+ Fill : Boolean := True);
@end group
@end smallexample
@end smallexample
@noindent
-A configuration pragma that establishes SPARK 95 mode for the unit to which
+This is a configuration pragma that establishes SPARK 95 mode
+for the unit to which
it applies, regardless of the mode set by the command line switches.
-In this mode, the compiler rejects constructs outside the SPARK 95 subset of
-Ada, which provides a useful initial filter for those projects developed in
-SPARK. Syntax and semantic error messages related to SPARK restrictions have
-the form:
+In this mode, the compiler rejects constructs not permitted by SPARK 95.
+Error messages related to SPARK restrictions have the form:
@code{(spark) error message}.
This is not a replacement for the semantic checks performed by the
SPARK Examiner tool, as the compiler only deals currently with code,
-not at all with SPARK annotations, so it may well be the case that code which
+not at all with SPARK annotations and does not guarantee catching all
+cases of constructs forbidden by SPARK 95.
+
+Thus it may well be the case that code which
passes the compiler in SPARK 95 mode is rejected by the SPARK Examiner,
e.g. due to the different visibility rules of the Examiner based on
-@code{inherit} SPARK annotations.
+SPARK @code{inherit} annotations.
+
+SPARK 95 mode can be useful in providing an initial filter for
+code developed using SPARK 95, or in examining legacy code to see how far
+it is from meeting SPARK 95 restrictions.
@node Pragma Static_Elaboration_Desired
@unnumberedsec Pragma Static_Elaboration_Desired
end if;
end loop;
- -- If aspects scanned, store them
+ -- Here if aspects present
if Is_Non_Empty_List (Aspects) then
- if Decl = Error then
+
+ -- If Decl is Empty, we just ignore the aspects (the caller in this
+ -- case has always issued an appropriate error message).
+
+ if Decl = Empty then
+ null;
+
+ -- If Decl is Error, we ignore the aspects, and issue a message
+
+ elsif Decl = Error then
Error_Msg ("aspect specifications not allowed here", Ptr);
+
+ -- Here aspects are allowed, and we store them
+
else
Set_Parent (Aspects, Decl);
Set_Aspect_Specifications (Decl, Aspects);
Name_Node : Node_Id;
Package_Sloc : Source_Ptr;
+ Aspect_Sloc : Source_Ptr := No_Location;
+ -- Save location of WITH for scanned aspects. Left set to No_Location
+ -- if no aspects scanned before the IS keyword.
+
+ Is_Sloc : Source_Ptr;
+ -- Save location of IS token for package declaration
+
Dummy_Node : constant Node_Id :=
New_Node (N_Package_Specification, Token_Ptr);
-- Dummy node to attach aspect specifications to until we properly
-- Generic package instantiation or package declaration
else
- P_Aspect_Specifications (Dummy_Node, Semicolon => False);
+ if Aspect_Specifications_Present then
+ Aspect_Sloc := Token_Ptr;
+ P_Aspect_Specifications (Dummy_Node, Semicolon => False);
+ end if;
+
+ Is_Sloc := Token_Ptr;
TF_Is;
-- Case of generic instantiation
("generic instantiation cannot appear here!");
end if;
+ if Aspect_Sloc /= No_Location then
+ Error_Msg
+ ("misplaced aspects for package instantiation",
+ Aspect_Sloc);
+ end if;
+
Scan; -- past NEW
Package_Node :=
Set_Name (Package_Node, P_Qualified_Simple_Name);
Set_Generic_Associations
(Package_Node, P_Generic_Actual_Part_Opt);
- P_Aspect_Specifications (Error);
+
+ if Aspect_Sloc /= No_Location
+ and then not Aspect_Specifications_Present
+ then
+ Error_Msg_SC ("\info: aspect specifications belong here");
+ Move_Aspects (From => Dummy_Node, To => Package_Node);
+ end if;
+
+ P_Aspect_Specifications (Package_Node);
Pop_Scope_Stack;
-- Case of package declaration or package specification
Discard_Junk_List (P_Sequence_Of_Statements (SS_None));
end if;
- End_Statements (Specification_Node);
+ End_Statements (Specification_Node, Empty, Is_Sloc);
+ Move_Aspects (From => Dummy_Node, To => Package_Node);
end if;
end if;
end if;
- Move_Aspects (From => Dummy_Node, To => Package_Node);
return Package_Node;
end P_Package;
-- Check_End --
---------------
- function Check_End (Decl : Node_Id := Empty) return Boolean is
+ function Check_End
+ (Decl : Node_Id := Empty;
+ Is_Loc : Source_Ptr := No_Location) return Boolean
+ is
Name_On_Separate_Line : Boolean;
-- Set True if the name on an END line is on a separate source line
-- from the END. This is highly suspicious, but is allowed. The point
if End_Type /= E_Record then
- -- Scan aspect specifications if permitted here
+ -- Scan aspect specifications
if Aspect_Specifications_Present then
+
+ -- Aspect specifications not allowed
+
if No (Decl) then
- P_Aspect_Specifications (Error);
+
+ -- Package declaration case
+
+ if Is_Loc /= No_Location then
+ Error_Msg_SC
+ ("misplaced aspects for package declaration");
+ Error_Msg
+ ("info: aspect specifications belong here", Is_Loc);
+ P_Aspect_Specifications (Empty);
+
+ -- Other cases where aspect specifications are not allowed
+
+ else
+ P_Aspect_Specifications (Error);
+ end if;
+
+ -- Aspect specifications allowed
+
else
P_Aspect_Specifications (Decl);
end if;
-- Error recovery: cannot raise Error_Resync;
procedure End_Statements
- (Parent : Node_Id := Empty;
- Decl : Node_Id := Empty)
+ (Parent : Node_Id := Empty;
+ Decl : Node_Id := Empty;
+ Is_Sloc : Source_Ptr := No_Location)
is
begin
-- This loop runs more than once in the case where Check_End rejects
-- the END sequence, as indicated by Check_End returning False.
loop
- if Check_End (Decl) then
+ if Check_End (Decl, Is_Sloc) then
if Present (Parent) then
Set_End_Label (Parent, End_Labl);
end if;
-- Semicolon is True, a terminating semicolon is also scanned. If this
-- argument is False, the scan pointer is left pointing past the aspects
-- and the caller must check for a proper terminator.
- -- left pointing past the aspects, presumably pointing to a terminator.
--
-- P_Aspect_Specification is called with the current token pointing to
-- either a WITH keyword starting an aspect specification, or an
-- the given declaration node. A list of aspects is built and stored for
-- this declaration node using a call to Set_Aspect_Specifications. If
-- no WITH keyword is present, then this call has no effect other than
- -- scanning out the terminator if it is a semicolon. If Decl is Error on
- -- entry, any scanned aspect specifications are ignored and a message is
- -- output saying aspect specifications not permitted here.
+ -- scanning out the terminator if it is a semicolon.
+
+ -- If Decl is Error on entry, any scanned aspect specifications are
+ -- ignored and a message is output saying aspect specifications not
+ -- permitted here. If Decl is Empty, then scanned aspect specifications
+ -- are also ignored, but no error message is given (this is used when
+ -- the caller has already taken care of the error message).
function P_Code_Statement (Subtype_Mark : Node_Id) return Node_Id;
-- Function to parse a code statement. The caller has scanned out
-- Routines for handling end lines, including scope recovery
package Endh is
- function Check_End (Decl : Node_Id := Empty) return Boolean;
+ function Check_End
+ (Decl : Node_Id := Empty;
+ Is_Loc : Source_Ptr := No_Location) return Boolean;
-- Called when an end sequence is required. In the absence of an error
-- situation, Token contains Tok_End on entry, but in a missing end
-- case, this may not be the case. Pop_End_Context is used to determine
--
-- If Decl is non-empty, then aspect specifications are permitted
-- following the end, and Decl is the declaration node with which
- -- these aspect specifications are to be associated.
+ -- these aspect specifications are to be associated. If Decl is empty,
+ -- then aspect specifications are not permitted and will generate an
+ -- error message.
+ --
+ -- Is_Loc is set to other than the default only for the case of a
+ -- package declaration. It points to the IS keyword of the declaration,
+ -- and is used to specialize the error messages for misplaced aspect
+ -- specifications in this case. Note that Decl is always Empty if Is_Loc
+ -- is set.
procedure End_Skip;
-- Skip past an end sequence. On entry Token contains Tok_End, and we
-- error messages while carrying this out.
procedure End_Statements
- (Parent : Node_Id := Empty;
- Decl : Node_Id := Empty);
+ (Parent : Node_Id := Empty;
+ Decl : Node_Id := Empty;
+ Is_Sloc : Source_Ptr := No_Location);
-- Called when an end is required or expected to terminate a sequence
-- of statements. The caller has already made an appropriate entry in
-- the Scope.Table to describe the expected form of the end. This can
-- If Decl is non-null, then it is a declaration node, and aspect
-- specifications are permitted after the end statement. These aspect
-- specifications, if present, are stored in this declaration node.
+ -- If Decl is null, then aspect specifications are not permitted after
+ -- the end statement.
+ --
+ -- In the case where Decl is null, Is_Sloc determines the handling. If
+ -- it is set to No_Location, then aspect specifications are ignored and
+ -- an error message is given. Is_Sloc is used in the package declaration
+ -- case to point to the IS, and is used to specialize the error emssages
+ -- issued in this case.
end Endh;
--------------
Set_Size_Known_At_Compile_Time (T);
end Check_Static_Discriminated_Subtype;
+ -------------------------
+ -- Is_Others_Aggregate --
+ -------------------------
+
+ function Is_Others_Aggregate (Aggr : Node_Id) return Boolean is
+ begin
+ return No (Expressions (Aggr))
+ and then
+ Nkind (First (Choices (First (Component_Associations (Aggr)))))
+ = N_Others_Choice;
+ end Is_Others_Aggregate;
+
--------------------------------
-- Make_String_Into_Aggregate --
--------------------------------
Error_Msg_N ("illegal context for aggregate", N);
end if;
+ if Formal_Verification_Mode and then Comes_From_Source (N) then
+
+ -- An unqualified aggregate is restricted in SPARK or ALFA to:
+ -- An 'aggregate item' inside an multi-dimensional aggregate
+ -- An expression being assigned to an unconstrained array, but only
+ -- if the aggregate specifies a value for OTHERS only.
+
+ if Nkind (Parent (N)) /= N_Qualified_Expression then
+ if Is_Array_Type (Etype (N)) then
+ if Nkind (Parent (N)) = N_Assignment_Statement
+ and then not Is_Constrained (Etype (Name (Parent (N))))
+ then
+ if not Is_Others_Aggregate (N) then
+ Error_Msg_F
+ ("|~~array aggregate should have only OTHERS", N);
+ end if;
+
+ elsif not (Nkind (Parent (N)) = N_Aggregate
+ and then Is_Array_Type (Etype (Parent (N)))
+ and then Number_Dimensions (Etype (Parent (N))) > 1)
+ then
+ Error_Msg_F ("|~~array aggregate should be qualified", N);
+ else
+ null;
+ end if;
+
+ elsif Is_Record_Type (Etype (N)) then
+ Error_Msg_F ("|~~record aggregate should be qualified", N);
+
+ -- The type of aggregate is neither array nor record, so an error
+ -- must have occurred during resolution. Do not report an
+ -- additional message here.
+
+ else
+ null;
+ end if;
+ end if;
+ end if;
+
-- If we can determine statically that the evaluation of the aggregate
-- raises Constraint_Error, then replace the aggregate with an
-- N_Raise_Constraint_Error node, but set the Etype to the right
-- bounds of the array aggregate are within range.
Set_Do_Range_Check (Choice, False);
+
+ -- In SPARK or ALFA, the choice must be static
+
+ if Formal_Verification_Mode
+ and then Comes_From_Source (Original_Node (Choice))
+ and then not Is_Static_Expression (Choice)
+ then
+ Error_Msg_F ("|~~choice should be static", Choice);
+ end if;
end if;
-- If we could not resolve the discrete choice stop here
Analyze (A);
Check_Parameterless_Call (A);
+ -- In SPARK or ALFA, the ancestor part cannot be a subtype mark
+
+ if Formal_Verification_Mode
+ and then Comes_From_Source (N)
+ and then Is_Entity_Name (A)
+ and then Is_Type (Entity (A))
+ then
+ Error_Msg_F ("|~~ancestor part cannot be a subtype mark", A);
+ end if;
+
if not Is_Tagged_Type (Typ) then
Error_Msg_N ("type of extension aggregate must be tagged", N);
return;
-- Start of processing for Resolve_Record_Aggregate
begin
+ -- A record aggregate is restricted in SPARK or ALFA:
+ -- Each named association can have only a single choice.
+ -- OTHERS cannot be used.
+ -- Positional and named associations cannot be mixed.
+
+ if Formal_Verification_Mode
+ and then Comes_From_Source (N)
+ and then Present (Component_Associations (N))
+ then
+ if Present (Expressions (N)) then
+ Error_Msg_F
+ ("|~~named association cannot follow positional association",
+ First (Choices (First (Component_Associations (N)))));
+ end if;
+
+ declare
+ Assoc : Node_Id;
+
+ begin
+ Assoc := First (Component_Associations (N));
+ while Present (Assoc) loop
+ if List_Length (Choices (Assoc)) > 1 then
+ Error_Msg_F
+ ("|~~component association in record aggregate must "
+ & "contain a single choice", Assoc);
+ end if;
+
+ if Nkind (First (Choices (Assoc))) = N_Others_Choice then
+ Error_Msg_F
+ ("|~~record aggregate cannot contain OTHERS", Assoc);
+ end if;
+
+ Assoc := Next (Assoc);
+ end loop;
+ end;
+ end if;
+
-- We may end up calling Duplicate_Subexpr on expressions that are
-- attached to New_Assoc_List. For this reason we need to attach it
-- to the tree by setting its parent pointer to N. This parent point
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2007, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2010, 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- --
procedure Resolve_Aggregate (N : Node_Id; Typ : Entity_Id);
procedure Resolve_Extension_Aggregate (N : Node_Id; Typ : Entity_Id);
+ function Is_Others_Aggregate (Aggr : Node_Id) return Boolean;
+ -- Returns True is aggregate Aggr consists of a single OTHERS choice
+
end Sem_Aggr;
Analyze_Choices (N, Exp_Type, Dont_Care, Others_Present);
- -- A case statement with a single "others" alternative is not allowed
+ -- A case statement with a single OTHERS alternative is not allowed
-- in SPARK or ALFA.
if Formal_Verification_Mode
else
Make_Inline (Subp);
+ -- For the pragma case, climb homonym chain. This is
+ -- what implements allowing the pragma in the renaming
+ -- case, with the result applying to the ancestors.
+
if not From_Aspect_Specification (N) then
while Present (Homonym (Subp))
and then Scope (Homonym (Subp)) = Current_Scope
Set_Etype (N, B_Typ);
Generate_Operator_Reference (N, B_Typ);
Eval_Logical_Op (N);
+
+ -- In SPARK or ALFA, logical operations AND, OR and XOR for arrays are
+ -- defined only when both operands have same static lower and higher
+ -- bounds.
+
+ if Formal_Verification_Mode
+ and then Comes_From_Source (Original_Node (N))
+ and then Is_Array_Type (Etype (N))
+ then
+ declare
+ L_Index : Node_Id;
+ R_Index : Node_Id;
+ L_Low : Node_Id;
+ L_High : Node_Id;
+ R_Low : Node_Id;
+ R_High : Node_Id;
+
+ L_Typ : constant Node_Id := Etype (Left_Opnd (N));
+ R_Typ : constant Node_Id := Etype (Right_Opnd (N));
+
+ begin
+ L_Index := First_Index (L_Typ);
+ R_Index := First_Index (R_Typ);
+
+ Get_Index_Bounds (L_Index, L_Low, L_High);
+ Get_Index_Bounds (R_Index, R_Low, R_High);
+
+ -- Another error is issued for constrained array types with
+ -- non-static bounds elsewhere, so only deal with different
+ -- constrained types, or unconstrained types.
+
+ if L_Typ /= R_Typ or else not Is_Constrained (L_Typ) then
+ if not Is_Static_Expression (L_Low)
+ or else not Is_Static_Expression (R_Low)
+ or else Expr_Value (L_Low) /= Expr_Value (R_Low)
+ then
+ Error_Msg_F ("|~~operation defined only when both operands "
+ & "have the same static lower bound", N);
+ end if;
+
+ if not Is_Static_Expression (L_High)
+ or else not Is_Static_Expression (R_High)
+ or else Expr_Value (L_High) /= Expr_Value (R_High)
+ then
+ Error_Msg_F ("|~~operation defined only when both operands "
+ & "have the same static higher bound", N);
+ end if;
+ end if;
+ end;
+ end if;
+
end Resolve_Logical_Op;
---------------------------
-gnateG ^ /GENERATE_PROCESSED_SOURCE
-gnatem ^ /MAPPING_FILE
-gnatep ^ /DATA_PREPROCESSING
+-gnateP ^ /CATEGORIZATION_WARNINGS
-gnateS ^ /SCO_OUTPUT
-gnatE ^ /CHECKS=ELABORATION
-gnatf ^ /REPORT_ERRORS=FULL
-- be sure that they are valid, and code is generated to allow for this
-- possibility. The use of /ASSUME_VALID will improve the code.
+ S_GCC_CategW : aliased constant S := "/CATEGORIZATION_WARNINGS " &
+ "-gnateP";
+ -- /NO_CATEGORIZATION_WARNINGS (D)
+ -- /CATEGORIZATION_WARNINGS
+ --
+ -- Use to tell the compiler to disable categorization dependency errors.
+ -- Ada requires that units that WITH one another have compatible
+ -- categories, for example a Pure unit cannot WITH a Preelaborate unit.
+ -- If this switch is used, these errors become warnings (which can be
+ -- ignored, or suppressed in the usual manner). This can be useful in
+ -- some specialized circumstances such as the temporary use of special
+ -- test software.
+
S_GCC_Checks : aliased constant S := "/CHECKS=" &
"FULL " &
"-gnato,!-gnatE,!-gnatp " &
S_GCC_Add 'Access,
S_GCC_Asm 'Access,
S_GCC_AValid 'Access,
+ S_GCC_CategW 'Access,
S_GCC_Checks 'Access,
S_GCC_ChecksX 'Access,
S_GCC_Compres 'Access,
projects / platform / upstream / linaro-gcc.git / commitdiff