+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * sem_res.adb (Resolve_Logical_Op): ensure N is a binary operator
+ before accessing operands.
+ * sem_util.adb (Is_SPARK_Initialization_Expr): follow original nodes to
+ decide whether an initialization expression respects SPARK rules, as
+ the plain node is the expanded one. This allows for more valid warnings
+ to be issued.
+ * gnat_rm.texi: Minor update.
+
+2011-08-02 Arnaud Charlet <charlet@adacore.com>
+
+ * sem_ch13.adb (Analyze_Enumeration_Representation_Clause): Revert
+ previous change.
+
+2011-08-02 Robert Dewar <dewar@adacore.com>
+
+ * sem_ch3.adb, sem_ch4.adb: Minor reformatting.
+
+2011-08-02 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch5.adb (Expand_Iterator_Loop): Reformatting. Wrap the original
+ loop statements and the element renaming declaration with a block when
+ the element type is controlled.
+
+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * sinfo.ads: Minor formatting.
+
+2011-08-02 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_aggr.adb (Add_Association): if the association has a box and no
+ expression, use the Sloc of the aggregate itself for the new
+ association.
+ * errout.adb (First_Node): Exclude nodes with no Sloc, and always use
+ the Original_Node.
+
2011-08-02 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch5.adb (Expand_Iterator_Loop): Code cleanup and refactoring.
function First_Node (C : Node_Id) return Node_Id is
L : constant Source_Ptr := Sloc (Original_Node (C));
+ Orig : constant Node_Id := Original_Node (C);
Sfile : constant Source_File_Index := Get_Source_File_Index (L);
Earliest : Node_Id;
Eloc : Source_Ptr;
if Loc < Eloc
and then Loc /= Standard_Location
+ and then Loc /= No_Location
and then Get_Source_File_Index (Loc) = Sfile
then
Earliest := Original_Node (N);
-- Start of processing for First_Node
begin
- if Nkind (C) in N_Subexpr then
- Earliest := Original_Node (C);
+ if Nkind (Orig) in N_Subexpr then
+ Earliest := Orig;
Eloc := Sloc (Earliest);
- Search_Tree_First (Original_Node (C));
+ Search_Tree_First (Orig);
return Earliest;
+
else
- return C;
+ return Orig;
end if;
end First_Node;
I_Spec : constant Node_Id := Iterator_Specification (Isc);
Id : constant Entity_Id := Defining_Identifier (I_Spec);
Loc : constant Source_Ptr := Sloc (N);
- Stats : constant List_Id := Statements (N);
Container : constant Node_Id := Name (I_Spec);
Container_Typ : constant Entity_Id := Etype (Container);
-
- Cursor : Entity_Id;
- New_Loop : Node_Id;
+ Cursor : Entity_Id;
+ New_Loop : Node_Id;
+ Stats : List_Id := Statements (N);
begin
-- Processing for arrays
-- Processing for containers
else
- -- In both cases these require a cursor of the proper type
+ -- The for loop is expanded into a while loop which uses a container
+ -- specific cursor to examine each element.
-- Cursor : Pack.Cursor := Container.First;
-- while Cursor /= Pack.No_Element loop
- -- Obj : Pack.Element_Type renames Element (Cursor);
- -- -- for the "of" form
+ -- declare
+ -- -- the block is added when Element_Type is controlled
- -- <original loop statements>
+ -- Obj : Pack.Element_Type := Element (Cursor);
+ -- -- for the "of" loop form
+ -- begin
+ -- <original loop statements>
+ -- end;
-- Pack.Next (Cursor);
-- end loop;
- -- with the obvious replacements if "reverse" is specified. Pack is
- -- the name of the package which instantiates the container.
+ -- If "reverse" is present, then the initialization of the cursor
+ -- uses Last and the step becomes Prev. Pack is the name of the
+ -- package which instantiates the container.
declare
Element_Type : constant Entity_Id := Etype (Id);
Pack : constant Entity_Id :=
Scope (Base_Type (Container_Typ));
+ Decl : Node_Id;
Cntr : Node_Id;
Name_Init : Name_Id;
Name_Step : Name_Id;
-- The code below only handles containers where Element is not a
-- primitive operation of the container. This excludes for now the
- -- Hi-Lite formal containers. Generate:
- --
- -- Id : Element_Type renames Container.Element (Cursor);
+ -- Hi-Lite formal containers.
if Of_Present (I_Spec) then
- Prepend_To (Stats,
+
+ -- Generate:
+ -- Id : Element_Type := Pack.Element (Cursor);
+
+ Decl :=
Make_Object_Renaming_Declaration (Loc,
Defining_Identifier => Id,
Subtype_Mark =>
- New_Occurrence_Of (Element_Type, Loc),
+ New_Reference_To (Element_Type, Loc),
Name =>
Make_Indexed_Component (Loc,
Prefix =>
Make_Selected_Component (Loc,
Prefix =>
- New_Occurrence_Of (Pack, Loc),
+ New_Reference_To (Pack, Loc),
Selector_Name =>
Make_Identifier (Loc, Chars => Name_Element)),
Expressions => New_List (
- New_Occurrence_Of (Cursor, Loc)))));
+ New_Reference_To (Cursor, Loc))));
+
+ -- When the container holds controlled objects, wrap the loop
+ -- statements and element renaming declaration with a block.
+ -- This ensures that the transient result of Element (Cursor)
+ -- is cleaned up after each iteration of the loop.
+
+ if Needs_Finalization (Element_Type) then
+
+ -- Generate:
+ -- declare
+ -- Id : Element_Type := Pack.Element (Cursor);
+ -- begin
+ -- <original loop statments>
+ -- end;
+
+ Stats := New_List (
+ Make_Block_Statement (Loc,
+ Declarations => New_List (Decl),
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Stats)));
+ else
+ Prepend_To (Stats, Decl);
+ end if;
end if;
-- Determine the advancement and initialization steps for the
Name =>
Make_Selected_Component (Loc,
Prefix =>
- New_Occurrence_Of (Pack, Loc),
+ New_Reference_To (Pack, Loc),
Selector_Name =>
Make_Identifier (Loc, Name_Step)),
Parameter_Associations => New_List (
- New_Occurrence_Of (Cursor, Loc))));
+ New_Reference_To (Cursor, Loc))));
-- Generate:
-- while Cursor /= Pack.No_Element loop
Condition =>
Make_Op_Ne (Loc,
Left_Opnd =>
- New_Occurrence_Of (Cursor, Loc),
+ New_Reference_To (Cursor, Loc),
Right_Opnd =>
Make_Selected_Component (Loc,
Prefix =>
- New_Occurrence_Of (Pack, Loc),
+ New_Reference_To (Pack, Loc),
Selector_Name =>
Make_Identifier (Loc, Name_No_Element)))),
Statements => Stats,
Object_Definition =>
Make_Selected_Component (Loc,
Prefix =>
- New_Occurrence_Of (Pack, Loc),
+ New_Reference_To (Pack, Loc),
Selector_Name =>
Make_Identifier (Loc, Name_Cursor)),
restrictions will be checked for constructs forbidden in SPARK 95.
Error messages related to SPARK restriction have the form:
-@code{(spark) error message}.
+@smallexample
+violation of restriction "Spark" at <file>
+ <error message>
+@end smallexample
This is not a replacement for the semantic checks performed by the
SPARK Examiner tool, as the compiler only deals currently with code,
end if;
if not Aggr_Resolved then
+
+ -- A parenthesized expression may have been intended as an
+ -- aggregate, leading to a type error when analyzing the
+ -- component. This can also happen for a nested component
+ -- (see Analyze_Aggr_Expr).
+
+ if Paren_Count (N) > 0 then
+ Error_Msg_N
+ ("positional aggregate cannot have one component", N);
+ end if;
+
Aggr_Subtyp := Any_Composite;
else
Aggr_Subtyp := Array_Aggr_Subtype (N, Typ);
("\if single-component aggregate is intended,"
& " write e.g. (1 ='> ...)", Expr);
end if;
+
return Failure;
end if;
end if;
return Failure;
end if;
+ if Others_Present
+ and then Nkind (Parent (N)) /= N_Component_Association
+ and then No (Expressions (N))
+ and then
+ Nkind (First (Choices (First (Component_Associations (N)))))
+ = N_Others_Choice
+ and then Is_Elementary_Type (Component_Typ)
+ and then False
+ then
+ declare
+ Assoc : constant Node_Id := First (Component_Associations (N));
+ begin
+ Rewrite (Assoc,
+ Make_Component_Association (Loc,
+ Choices =>
+ New_List (
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Occurrence_Of (Index_Typ, Loc),
+ Attribute_Name => Name_Range)),
+ Expression => Relocate_Node (Expression (Assoc))));
+ return Resolve_Array_Aggregate
+ (N, Index, Index_Constr, Component_Typ, Others_Allowed);
+ end;
+ end if;
+
-- Protect against cascaded errors
if Etype (Index_Typ) = Any_Type then
Assoc_List : List_Id;
Is_Box_Present : Boolean := False)
is
+ Loc : Source_Ptr;
Choice_List : constant List_Id := New_List;
New_Assoc : Node_Id;
begin
- Append (New_Occurrence_Of (Component, Sloc (Expr)), Choice_List);
+ -- If this is a box association the expression is missing, so
+ -- use the Sloc of the aggregate itself for the new association.
+
+ if Present (Expr) then
+ Loc := Sloc (Expr);
+ else
+ Loc := Sloc (N);
+ end if;
+
+ Append (New_Occurrence_Of (Component, Loc), Choice_List);
New_Assoc :=
- Make_Component_Association (Sloc (Expr),
+ Make_Component_Association (Loc,
Choices => Choice_List,
Expression => Expr,
Box_Present => Is_Box_Present);
-- Pointer to node for literal providing max value
begin
- if Ignore_Rep_Clauses or else CodePeer_Mode then
+ if Ignore_Rep_Clauses then
return;
end if;
if Nkind (Original_Node (N)) = N_Object_Declaration
and then Comes_From_Source (Original_Node (N))
- -- only call test if needed
+
+ -- Only call test if needed
+
and then (Formal_Verification_Mode
or else Restriction_Check_Required (SPARK))
and then not Is_SPARK_Initialization_Expr (E)
procedure Check_Mixed_Parameter_And_Named_Associations is
Actual : Node_Id;
Named_Seen : Boolean;
+
begin
- Actual := First (Actuals);
Named_Seen := False;
+
+ Actual := First (Actuals);
while Present (Actual) loop
case Nkind (Actual) is
when N_Parameter_Association =>
---------------------------
procedure Process_Function_Call is
- Actual : Node_Id;
+ Actual : Node_Id;
+
begin
Change_Node (N, N_Function_Call);
Set_Name (N, P);
-- bounds. Of course the types have to match, so only check if operands
-- are compatible and the node itself has no errors.
- declare
- Left_Typ : constant Node_Id := Etype (Left_Opnd (N));
- Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
- begin
- if Is_Array_Type (B_Typ)
- and then Nkind (N) in N_Binary_Op
- and then Base_Type (Left_Typ) = Base_Type (Right_Typ)
- and then Left_Typ /= Any_Composite -- or else Left_Opnd in error
- and then Right_Typ /= Any_Composite -- or else Right_Opnd in error
- and then not Matching_Static_Array_Bounds (Left_Typ, Right_Typ)
- then
- Check_Formal_Restriction
- ("array types should have matching static bounds", N);
- end if;
- end;
-
+ if Is_Array_Type (B_Typ)
+ and then Nkind (N) in N_Binary_Op
+ then
+ declare
+ Left_Typ : constant Node_Id := Etype (Left_Opnd (N));
+ Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
+ begin
+ if Base_Type (Left_Typ) = Base_Type (Right_Typ)
+ and then Left_Typ /= Any_Composite -- or Left_Opnd in error
+ and then Right_Typ /= Any_Composite -- or Right_Opnd in error
+ and then not Matching_Static_Array_Bounds (Left_Typ, Right_Typ)
+ then
+ Check_Formal_Restriction
+ ("array types should have matching static bounds", N);
+ end if;
+ end;
+ end if;
end Resolve_Logical_Op;
---------------------------
Is_Ok : Boolean;
Expr : Node_Id;
Comp_Assn : Node_Id;
+ Orig_N : constant Node_Id := Original_Node (N);
begin
Is_Ok := True;
- if not Comes_From_Source (N) then
+ if not Comes_From_Source (Orig_N) then
goto Done;
end if;
- pragma Assert (Nkind (N) in N_Subexpr);
+ pragma Assert (Nkind (Orig_N) in N_Subexpr);
- case Nkind (N) is
+ case Nkind (Orig_N) is
when N_Character_Literal |
N_Integer_Literal |
N_Real_Literal |
when N_Identifier |
N_Expanded_Name =>
- if Is_Entity_Name (N)
- and then Present (Entity (N)) -- needed in some cases
+ if Is_Entity_Name (Orig_N)
+ and then Present (Entity (Orig_N)) -- needed in some cases
then
- case Ekind (Entity (N)) is
+ case Ekind (Entity (Orig_N)) is
when E_Constant |
E_Enumeration_Literal |
E_Named_Integer |
E_Named_Real =>
null;
when others =>
- if Is_Type (Entity (N)) then
+ if Is_Type (Entity (Orig_N)) then
null;
else
Is_Ok := False;
when N_Qualified_Expression |
N_Type_Conversion =>
- Is_Ok := Is_SPARK_Initialization_Expr (Expression (N));
+ Is_Ok := Is_SPARK_Initialization_Expr (Expression (Orig_N));
when N_Unary_Op =>
- Is_Ok := Is_SPARK_Initialization_Expr (Right_Opnd (N));
+ Is_Ok := Is_SPARK_Initialization_Expr (Right_Opnd (Orig_N));
when N_Binary_Op |
N_Short_Circuit |
N_Membership_Test =>
- Is_Ok := Is_SPARK_Initialization_Expr (Left_Opnd (N))
- and then Is_SPARK_Initialization_Expr (Right_Opnd (N));
+ Is_Ok := Is_SPARK_Initialization_Expr (Left_Opnd (Orig_N))
+ and then Is_SPARK_Initialization_Expr (Right_Opnd (Orig_N));
when N_Aggregate |
N_Extension_Aggregate =>
- if Nkind (N) = N_Extension_Aggregate then
- Is_Ok := Is_SPARK_Initialization_Expr (Ancestor_Part (N));
+ if Nkind (Orig_N) = N_Extension_Aggregate then
+ Is_Ok := Is_SPARK_Initialization_Expr (Ancestor_Part (Orig_N));
end if;
- Expr := First (Expressions (N));
+ Expr := First (Expressions (Orig_N));
while Present (Expr) loop
if not Is_SPARK_Initialization_Expr (Expr) then
Is_Ok := False;
Next (Expr);
end loop;
- Comp_Assn := First (Component_Associations (N));
+ Comp_Assn := First (Component_Associations (Orig_N));
while Present (Comp_Assn) loop
Expr := Expression (Comp_Assn);
if Present (Expr) -- needed for box association
end loop;
when N_Attribute_Reference =>
- if Nkind (Prefix (N)) in N_Subexpr then
- Is_Ok := Is_SPARK_Initialization_Expr (Prefix (N));
+ if Nkind (Prefix (Orig_N)) in N_Subexpr then
+ Is_Ok := Is_SPARK_Initialization_Expr (Prefix (Orig_N));
end if;
- Expr := First (Expressions (N));
+ Expr := First (Expressions (Orig_N));
while Present (Expr) loop
if not Is_SPARK_Initialization_Expr (Expr) then
Is_Ok := False;
-- pragma has a local name argument (such as pragma Inline), it is
-- resolved to point to the specific entity affected by the pragma.
- --------------------------------------
+ --------------------------------------
-- 2.8 Pragma Argument Association --
--------------------------------------
-- True. So after semantic analysis, the Identifier is always set,
-- referencing an identifier whose entity has an Ekind of E_Loop.
- --------------------------
- -- 5.5 Iteration Scheme --
- --------------------------
+ ---------------------------
+ -- 5.5 Iteration Scheme --
+ ---------------------------
-- ITERATION_SCHEME ::=
-- while CONDITION
-- Loop_Parameter_Specification (Node4) (set to Empty if WHILE case)
---------------------------------------
- -- 5.5 Loop parameter specification --
+ -- 5.5 Loop Parameter Specification --
---------------------------------------
-- LOOP_PARAMETER_SPECIFICATION ::=
-- Reverse_Present (Flag15)
-- Discrete_Subtype_Definition (Node4)
- ----------------------------------
- -- 5.5.1 Iterator specification --
- ----------------------------------
+ -----------------------------------
+ -- 5.5.1 Iterator Specification --
+ -----------------------------------
-- ITERATOR_SPECIFICATION ::=
-- DEFINING_IDENTIFIER in [reverse] NAME
-- profile. Instead the information appears directly in the parent.
----------------------
- -- 6.1 Formal part --
+ -- 6.1 Formal Part --
----------------------
-- FORMAL_PART ::=
-- (PARAMETER_SPECIFICATION {; PARAMETER_SPECIFICATION})
----------------------------------
- -- 6.1 Parameter specification --
+ -- 6.1 Parameter Specification --
----------------------------------
-- PARAMETER_SPECIFICATION ::=