+2011-08-02 Pascal Obry <obry@adacore.com>
+
+ * prj-proc.adb, make.adb, makeutl.adb: Minor reformatting.
+
+2011-08-02 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch5.adb (Expand_Iterator_Loop): Code cleanup and reorganization.
+ Set the associated loop as the related expression of internally
+ generated cursors.
+ * exp_ch7.adb (Is_Container_Cursor): New routine.
+ (Wrap_Transient_Declaration): Supress the finalization of the list
+ controller when the declaration denotes a container cursor.
+
+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * opt.ads (SPARK_Mode): update comment, SPARK_Mode only set through
+ command line now.
+ * par-ch3.adb (P_Delta_Constraint): remove check in SPARK mode that the
+ expression is a simple expression. This check cannot be performed in
+ the semantics, so just drop it.
+ (P_Index_Or_Discriminant_Constraint): move check that the index or
+ discriminant is a subtype mark to Analyze_Subtype_Declaration in the
+ semantics. Other cases were previously checked in the semantics.
+ * par-ch4.adb (P_Name): move checks that a selector name is not
+ character literal or an operator symbol to Find_Selected_Component in
+ the semantics
+ * par-ch5.adb (Parse_Decls_Begin_End): move check that basic
+ declarations are not placed after later declarations in a separate
+ procedure in Sem_Util (possibly not the best choice?), to be used both
+ during parsing, for Ada 83 mode, and during semantic analysis, for
+ SPARK mode.
+ * par-endh.adb (Check_End): move check that end label is not missing
+ to Process_End_Label in the semantics
+ * par-prag.adb (Process_Restrictions_Or_Restriction_Warnings): remove
+ the special case for SPARK restriction
+ * par.adb: use and with Sem_Util, for use in Parse_Decls_Begin_End
+ * restrict.adb, restrict.ads (Check_Formal_Restriction): add a
+ parameter Force to issue the error message even on internal node (used
+ for generated end label). Call Check_Restriction to check when an error
+ must be issued. In SPARK mode, issue an error message even if the
+ restriction is not set.
+ (Check_Restriction): new procedure with an additional out parameter to
+ inform the caller that a message has been issued
+ * sem_aggr.adb: Minor modification of message
+ * sem_attr.adb (Analyze_Attribute): call Check_Formal_Restriction
+ instead of issuing an error message directly
+ * sem_ch3.adb (Analyze_Declarations): move here the check that basic
+ declarations are not placed after later declarations, by calling
+ Check_Later_Vs_Basic_Declarations
+ (Analyze_Subtype_Declaration): move here the check that an index or
+ discriminant constraint must be a subtype mark. Change the check that
+ a subtype of String must start at one so that it works on subtype marks.
+ * sem_ch4.adb (Analyze_Call): move here the check that a named
+ association cannot follow a positional one in a call
+ * sem_ch5.adb (Check_Unreachable_Code): call Check_Formal_Restriction
+ instead of issuing an error message directly
+ * sem_ch8.adb (Find_Selected_Component): move here the check that a
+ selector name is not a character literal or an operator symbol. Move
+ here the check that the prefix of an expanded name cannot be a
+ subprogram or a loop statement.
+ * sem_util.adb, sem_util.ads (Check_Later_Vs_Basic_Declarations): new
+ procedure called from parsing and semantics to check that basic
+ declarations are not placed after later declarations
+ (Process_End_Label): move here the check that end label is not missing
+
+2011-08-02 Arnaud Charlet <charlet@adacore.com>
+
+ * sem_ch13.adb (Analyze_Enumeration_Representation_Clause): Ignore enum
+ representation clause in codepeer mode, since it confuses CodePeer and
+ does not bring useful info.
+
+2011-08-02 Ed Falis <falis@adacore.com>
+
+ * init.c: initialize fp hw on MILS.
+
+2011-08-02 Ed Schonberg <schonberg@adacore.com>
+
+ * errout.adb (First_Node): for bodies, return the node itself (small
+ optimization). For other nodes, do not check source_unit if the node
+ comes from Standard.
+
2011-08-02 Robert Dewar <dewar@adacore.com>
* exp_ch3.adb: Minor comment additions.
-- best to just ignore this situation.
if Loc < Eloc
+ and then Loc /= Standard_Location
and then Get_Source_File_Index (Loc) = Sfile
then
Earliest := Original_Node (N);
-- Start of processing for First_Node
begin
- Earliest := Original_Node (C);
- Eloc := Sloc (Earliest);
- Search_Tree_First (Original_Node (C));
- return Earliest;
+ if Nkind (C) in N_Unit_Body
+ or else Nkind (C) in N_Proper_Body
+ then
+ return C;
+
+ else
+ Earliest := Original_Node (C);
+ Eloc := Sloc (Earliest);
+ Search_Tree_First (Original_Node (C));
+ return Earliest;
+ end if;
end First_Node;
----------------
-- with the obvious replacements if "reverse" is specified.
declare
- Element_Type : constant Entity_Id := Etype (Id);
- Pack : constant Entity_Id := Scope (Base_Type (Typ));
- Name_Init : Name_Id;
- Name_Step : Name_Id;
- Cond : Node_Id;
- Cursor_Decl : Node_Id;
- Renaming_Decl : Node_Id;
+ Element_Type : constant Entity_Id := Etype (Id);
+ Pack : constant Entity_Id := Scope (Base_Type (Typ));
+ Name_Init : Name_Id;
+ Name_Step : Name_Id;
begin
Stats := Statements (N);
Cursor := Id;
end if;
- if Reverse_Present (I_Spec) then
-
- -- Must verify that the container has a reverse iterator ???
+ -- Must verify that the container has a reverse iterator ???
+ if Reverse_Present (I_Spec) then
Name_Init := Name_Last;
Name_Step := Name_Previous;
-
else
Name_Init := Name_First;
Name_Step := Name_Next;
end if;
- -- C : Cursor_Type := Container.First;
-
- Cursor_Decl :=
- Make_Object_Declaration (Loc,
- Defining_Identifier => Cursor,
- Object_Definition =>
- Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (Pack, Loc),
- Selector_Name => Make_Identifier (Loc, Name_Cursor)),
- Expression =>
- Make_Selected_Component (Loc,
- Prefix => Relocate_Node (Container),
- Selector_Name => Make_Identifier (Loc, Name_Init)));
-
- Insert_Action (N, Cursor_Decl);
-
- -- while C /= No_Element loop
-
- Cond := Make_Op_Ne (Loc,
- Left_Opnd => New_Occurrence_Of (Cursor, Loc),
- Right_Opnd => Make_Selected_Component (Loc,
- Prefix => New_Occurrence_Of (Pack, Loc),
- Selector_Name =>
- Make_Identifier (Loc, Name_No_Element)));
+ -- 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);
if Of_Present (I_Spec) then
-
- -- Id : Element_Type renames Container.Element (Cursor);
-
- -- 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.
-
- Renaming_Decl :=
+ Prepend_To (Stats,
Make_Object_Renaming_Declaration (Loc,
Defining_Identifier => Id,
Subtype_Mark =>
Selector_Name =>
Make_Identifier (Loc, Chars => Name_Element)),
Expressions =>
- New_List (New_Occurrence_Of (Cursor, Loc))));
-
- Prepend (Renaming_Decl, Stats);
+ New_List (New_Occurrence_Of (Cursor, Loc)))));
end if;
-- For both iterator forms, add call to step operation (Next or
Parameter_Associations =>
New_List (New_Occurrence_Of (Cursor, Loc))));
- New_Loop := Make_Loop_Statement (Loc,
- Iteration_Scheme =>
- Make_Iteration_Scheme (Loc, Condition => Cond),
- Statements => Stats,
- End_Label => Empty);
+ -- Generate:
+ -- while Cursor /= No_Element loop
+ -- <Stats>
+ -- end loop;
+
+ New_Loop :=
+ Make_Loop_Statement (Loc,
+ Iteration_Scheme =>
+ Make_Iteration_Scheme (Loc,
+ Condition =>
+ Make_Op_Ne (Loc,
+ Left_Opnd =>
+ New_Occurrence_Of (Cursor, Loc),
+ Right_Opnd =>
+ Make_Selected_Component (Loc,
+ Prefix =>
+ New_Occurrence_Of (Pack, Loc),
+ Selector_Name =>
+ Make_Identifier (Loc, Name_No_Element)))),
+ Statements => Stats,
+ End_Label => Empty);
+
+ -- When the cursor is internally generated, associate it with the
+ -- loop statement.
+
+ if Of_Present (I_Spec) then
+ Set_Ekind (Cursor, E_Variable);
+ Set_Related_Expression (Cursor, New_Loop);
+ end if;
+
+ -- Create the declaration of the cursor and insert it before the
+ -- source loop. Generate:
+ --
+ -- C : Cursor_Type := Container.First;
+
+ Insert_Action (N,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Cursor,
+ Object_Definition =>
+ Make_Selected_Component (Loc,
+ Prefix => New_Occurrence_Of (Pack, Loc),
+ Selector_Name => Make_Identifier (Loc, Name_Cursor)),
+ Expression =>
+ Make_Selected_Component (Loc,
+ Prefix => Relocate_Node (Container),
+ Selector_Name => Make_Identifier (Loc, Name_Init))));
-- If the range of iteration is given by a function call that
-- returns a container, the finalization actions have been saved
if Present (Len_Ref) then
Action :=
Make_Implicit_If_Statement (N,
- Condition => Make_Op_Gt (Loc,
- Left_Opnd => Len_Ref,
- Right_Opnd => Make_Integer_Literal (Loc, 0)),
+ Condition =>
+ Make_Op_Gt (Loc,
+ Left_Opnd => Len_Ref,
+ Right_Opnd => Make_Integer_Literal (Loc, 0)),
Then_Statements => New_List (Action));
end if;
-- Finalize_One (_v2);
procedure Wrap_Transient_Declaration (N : Node_Id) is
- S : Entity_Id;
- LC : Entity_Id := Empty;
- Nodes : List_Id;
Loc : constant Source_Ptr := Sloc (N);
- First_Decl_Loc : Source_Ptr;
+ Next_N : constant Node_Id := Next (N);
Enclosing_S : Entity_Id;
+ First_Decl_Loc : Source_Ptr;
+ LC : Entity_Id := Empty;
+ Nodes : List_Id;
+ S : Entity_Id;
Uses_SS : Boolean;
- Next_N : constant Node_Id := Next (N);
+
+ function Is_Container_Cursor (Decl : Node_Id) return Boolean;
+ -- Determine whether object declaration Decl is a cursor used to iterate
+ -- over an Ada 2005/12 container.
+
+ -------------------------
+ -- Is_Container_Cursor --
+ -------------------------
+
+ function Is_Container_Cursor (Decl : Node_Id) return Boolean is
+ Def_Id : constant Entity_Id := Defining_Identifier (Decl);
+ Expr : constant Node_Id := Expression (Decl);
+
+ begin
+ -- A cursor declaration appears in the following form:
+ --
+ -- Index : Pack.Cursor := First (...);
+
+ return
+ Chars (Etype (Def_Id)) = Name_Cursor
+ and then Present (Expr)
+ and then Nkind (Expr) = N_Function_Call
+ and then Chars (Name (Expr)) = Name_First
+ and then
+ (Nkind (Parent (Decl)) = N_Expression_With_Actions
+ or else
+ Nkind (Related_Expression (Def_Id)) = N_Loop_Statement);
+ end Is_Container_Cursor;
+
+ -- Start of processing for Wrap_Transient_Declaration
begin
S := Current_Scope;
then
null;
+ -- The declaration of a container cursor is a special context where
+ -- the finalization of the list controller needs to be supressed. In
+ -- the following simplified example:
+ --
+ -- LC : Simple_List_Controller;
+ -- Temp : Ptr_Typ := Container_Creator_Function'Reference;
+ -- Deep_Tag_Attach (Temp, LC);
+ -- Obj : Pack.Cursor := First (Temp.all);
+ -- Finalize (LC);
+ -- <execute the loop>
+ --
+ -- the finalization of the list controller destroys the contents of
+ -- container Temp, and as a result Obj points to nothing. Note that
+ -- Temp will be finalized by the finalization list of the enclosing
+ -- scope.
+
+ elsif Ada_Version >= Ada_2012
+ and then Is_Container_Cursor (N)
+ then
+ null;
+
+ -- Finalize the list controller
+
else
Nodes :=
Make_Final_Call
to get correct Ada semantics. Note that for AE653 vThreads, the HW
overflow settings are an OS configuration issue. The instructions
below have no effect. */
-#if defined (_ARCH_PPC) && !defined (_SOFT_FLOAT) && !defined (VTHREADS)
+#if defined (_ARCH_PPC) && !defined (_SOFT_FLOAT) && (!defined (VTHREADS) || defined (__VXWORKSMILS__))
#if defined (__SPE__)
{
const unsigned long spefscr_mask = 0xfffffff3;
else
declare
Parent_Directory : constant String :=
- Get_Name_String (Project.Directory.Display_Name);
+ Get_Name_String
+ (Project.Directory.Display_Name);
begin
return Parent_Directory & Path_Name;
declare
ALI_Path_Name : constant String :=
- Name_Buffer (1 .. Name_Len);
+ Name_Buffer (1 .. Name_Len);
begin
if Is_Regular_File
-- belong to the ALFA subset of Ada. Set by debuf flag -gnatd.F.
SPARK_Mode : Boolean := False;
- -- Reject constructs not allowed by SPARK. Set by flag -gnatd.D or
- -- by pragma SPARK_95.
+ -- Reject constructs not allowed by SPARK. Set by flag -gnatd.D.
private
Expr_Node := P_Expression;
Check_Simple_Expression_In_Ada_83 (Expr_Node);
- if Expr_Form = EF_Non_Simple then
- Check_Formal_Restriction
- ("this expression must be parenthesized", Expr_Node);
- end if;
-
Set_Delta_Expression (Constraint_Node, Expr_Node);
if Token = Tok_Range then
Expr_Node := P_Expression_Or_Range_Attribute;
- if Expr_Form /= EF_Simple_Name
- and then Formal_Verification_Mode
- then
- Error_Msg_SC ("|~~subtype mark required");
- end if;
-
if Expr_Form = EF_Range_Attr then
Append (Expr_Node, Constr_List);
-- designator.
if Token not in Token_Class_Desig then
-
- -- Selector name cannot be a character literal in SPARK
-
- if SPARK_Mode and then Token = Tok_Char_Literal then
- Error_Msg_SC ("|~~character literal cannot be prefixed");
- end if;
-
goto Scan_Name_Extension_Dot;
else
- -- Selector name cannot be an operator symbol in SPARK
-
- if SPARK_Mode and then Token = Tok_Operator_Symbol then
- Error_Msg_SC ("|~~operator symbol cannot be prefixed");
- end if;
-
Prefix_Node := Name_Node;
Name_Node := New_Node (N_Selected_Component, Prev_Token_Ptr);
Set_Prefix (Name_Node, Prefix_Node);
-- Test for => (allow := as error substitute)
if Token = Tok_Arrow or else Token = Tok_Colon_Equal then
- if SPARK_Mode then
- Error_Msg_SP ("|~~no mixing of positional and named "
- & "parameter association");
- end if;
-
Restore_Scan_State (Scan_State); -- to Id
goto LP_State_Call;
procedure Parse_Decls_Begin_End (Parent : Node_Id) is
Body_Decl : Node_Id;
- Body_Sloc : Source_Ptr;
Decls : List_Id;
- Decl : Node_Id;
Parent_Nkind : Node_Kind;
Spec_Node : Node_Id;
HSS : Node_Id;
begin
Decls := P_Declarative_Part;
- -- Check for misplacement of later vs basic declarations in Ada 83.
- -- The same is true for the SPARK mode: although SPARK 95 removes
- -- the distinction between initial and later declarative items,
- -- the distinction remains in the Examiner. (JB01-005)
- -- Note that the Examiner does not count package declarations in later
- -- declarative items.
-
- if Ada_Version = Ada_83 or else SPARK_Mode then
- Decl := First (Decls);
-
- -- Loop through sequence of basic declarative items
-
- Outer : while Present (Decl) loop
- if Nkind (Decl) /= N_Subprogram_Body
- and then Nkind (Decl) /= N_Package_Body
- and then Nkind (Decl) /= N_Task_Body
- and then Nkind (Decl) not in N_Body_Stub
- then
- Next (Decl);
-
- -- Once a body is encountered, we only allow later declarative
- -- items. The inner loop checks the rest of the list.
-
- else
- Body_Sloc := Sloc (Decl);
-
- Inner : while Present (Decl) loop
- if (Nkind (Decl) not in N_Later_Decl_Item
- or else (SPARK_Mode
- and then
- Nkind (Decl) = N_Package_Declaration))
- and then Nkind (Decl) /= N_Pragma
- then
- if Ada_Version = Ada_83 then
- Error_Msg_Sloc := Body_Sloc;
- Error_Msg_N
- ("(Ada 83) decl cannot appear after body#", Decl);
- else
- pragma Assert (SPARK_Mode);
- Error_Msg_Sloc := Body_Sloc;
- Error_Msg_F
- ("|~~decl cannot appear after body#", Decl);
- end if;
- end if;
-
- Next (Decl);
- end loop Inner;
- end if;
- end loop Outer;
+ if Ada_Version = Ada_83 then
+ Check_Later_Vs_Basic_Declarations (Decls, During_Parsing => True);
end if;
-- Here is where we deal with the case of IS used instead of semicolon.
Set_Comes_From_Source (End_Labl, False);
End_Labl_Present := False;
- -- In SPARK mode, no missing label is allowed
-
- if SPARK_Mode
- and then End_Type = E_Name
- and then Explicit_Start_Label (Scope.Last)
- then
- Error_Msg_Node_1 := Scope.Table (Scope.Last).Labl;
- Error_Msg_SP -- CODEFIX
- ("|~~`END &` required");
- end if;
-
-- Do style check for missing label
if Style_Check
procedure Process_Restrictions_Or_Restriction_Warnings;
-- Common processing for Restrictions and Restriction_Warnings pragmas.
- -- This routine only processes the cases of No_Obsolescent_Features and
- -- SPARK, which are the only restrictions that have syntactic effects. No
- -- general error checking is done, since this will be done in Sem_Prag. The
- -- other case processed is pragma Restrictions No_Dependence, since
- -- otherwise this is done too late.
+ -- This routine only processes the case of No_Obsolescent_Features, which
+ -- is the only restriction that has syntactic effects. No general error
+ -- checking is done, since this will be done in Sem_Prag. The other case
+ -- processed is pragma Restrictions No_Dependence, since otherwise this is
+ -- done too late.
----------
-- Arg1 --
Set_Restriction (No_Obsolescent_Features, Pragma_Node);
Restriction_Warnings (No_Obsolescent_Features) :=
Prag_Id = Pragma_Restriction_Warnings;
- when SPARK =>
- SPARK_Mode := True;
- Set_Error_Msg_Lang ("spark");
- Formal_Verification_Mode := True;
when others =>
null;
end case;
with Restrict; use Restrict;
with Scans; use Scans;
with Scn; use Scn;
+with Sem_Util; use Sem_Util;
with Sinput; use Sinput;
with Sinput.L; use Sinput.L;
with Sinfo; use Sinfo;
Virtual_Prefix
then
Project.Virtual := True;
-
end if;
Project.Path.Display_Name :=
-- Check_Formal_Restriction --
------------------------------
- procedure Check_Formal_Restriction (Msg : String; N : Node_Id) is
+ procedure Check_Formal_Restriction
+ (Msg : String;
+ N : Node_Id;
+ Force : Boolean := False)
+ is
+ Msg_Issued : Boolean;
+ Save_Error_Msg_Sloc : Source_Ptr;
begin
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- then
- Error_Msg_F ("|~~" & Msg, N);
+ if Force or else Comes_From_Source (Original_Node (N)) then
+
+ -- Since the call to Restriction_Msg from Check_Restriction may set
+ -- Error_Msg_Sloc to the location of the pragma restriction, save and
+ -- restore the previous value of the global variable around the call.
+
+ -- ??? N in call to Check_Restriction should be First_Node (N), but
+ -- this causes an exception to be raised when analyzing osint.adb.
+ -- To be modified.
+
+ Save_Error_Msg_Sloc := Error_Msg_Sloc;
+ Check_Restriction (Msg_Issued, SPARK, N); -- N -> First_Node (N)
+ Error_Msg_Sloc := Save_Error_Msg_Sloc;
+
+ if Msg_Issued then
+ Error_Msg_F ("\\| " & Msg, N);
+ elsif SPARK_Mode then
+ Error_Msg_F ("|~~" & Msg, N);
+ end if;
end if;
end Check_Formal_Restriction;
procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id) is
+ Msg_Issued : Boolean;
+ Save_Error_Msg_Sloc : Source_Ptr;
begin
pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- then
- Error_Msg_F ("|~~" & Msg1, N);
- Error_Msg_F (Msg2, N);
+ if Comes_From_Source (Original_Node (N)) then
+
+ -- Since the call to Restriction_Msg from Check_Restriction may set
+ -- Error_Msg_Sloc to the location of the pragma restriction, save and
+ -- 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));
+ Error_Msg_Sloc := Save_Error_Msg_Sloc;
+
+ if Msg_Issued then
+ Error_Msg_F ("\\| " & Msg1, N);
+ Error_Msg_F (Msg2, N);
+ elsif SPARK_Mode then
+ Error_Msg_F ("|~~" & Msg1, N);
+ Error_Msg_F (Msg2, N);
+ end if;
end if;
end Check_Formal_Restriction;
(R : Restriction_Id;
N : Node_Id;
V : Uint := Uint_Minus_1)
+ is
+ Msg_Issued : Boolean;
+ pragma Unreferenced (Msg_Issued);
+ begin
+ Check_Restriction (Msg_Issued, R, N, V);
+ end Check_Restriction;
+
+ procedure Check_Restriction
+ (Msg_Issued : out Boolean;
+ R : Restriction_Id;
+ N : Node_Id;
+ V : Uint := Uint_Minus_1)
is
VV : Integer;
-- V converted to integer form. If V is greater than Integer'Last,
-- Start of processing for Check_Restriction
begin
+ Msg_Issued := False;
+
-- In CodePeer mode, we do not want to check for any restriction, or set
-- additional restrictions other than those already set in gnat1drv.adb
-- so that we have consistency between each compilation.
and then Restrictions.Value (R) = 0)
or else Restrictions.Count (R) > Restrictions.Value (R)
then
+ Msg_Issued := True;
Restriction_Msg (R, N);
end if;
end Check_Restriction;
-- If a restriction exists post error message at the given node.
procedure Check_Restriction
- (R : Restriction_Id;
- N : Node_Id;
- V : Uint := Uint_Minus_1);
+ (Msg_Issued : out Boolean;
+ R : Restriction_Id;
+ N : Node_Id;
+ V : Uint := Uint_Minus_1);
-- Checks that the given restriction is not set, and if it is set, an
- -- appropriate message is posted on the given node. Also records the
+ -- appropriate message is posted on the given node, in which case
+ -- Msg_Issued is set to True (and False otherwise). Also records the
-- violation in the appropriate internal arrays. Note that it is mandatory
-- to always use this routine to check if a restriction is violated. Such
-- checks must never be done directly by the caller, since otherwise
-- indicates the exact count for the violation. If the exact count is not
-- known, V is left at its default of -1 which indicates an unknown count.
+ procedure Check_Restriction
+ (R : Restriction_Id;
+ N : Node_Id;
+ V : Uint := Uint_Minus_1);
+ -- Wrapper on Check_Restriction with Msg_Issued, with the out-parameter
+ -- being ignored here.
+
procedure Check_Restriction_No_Dependence (U : Node_Id; Err : Node_Id);
-- Called when a dependence on a unit is created (either implicitly, or by
-- an explicit WITH clause). U is a node for the unit involved, and Err
-- an elaboration routine. If elaboration code is not allowed, an error
-- message is posted on the node given as argument.
- procedure Check_Formal_Restriction (Msg : String; N : Node_Id);
+ procedure Check_Formal_Restriction
+ (Msg : String;
+ N : Node_Id;
+ Force : Boolean := False);
-- Node N represents a construct not allowed in formal mode. If this is a
- -- source node, then an error is issued on N (using Err_Msg_F), prepending
- -- "|~~" (error not serious, language prepended). Call has no effect if
- -- not in formal mode, or if N does not come originally from source.
+ -- 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.
procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id);
-- Same as Check_Formal_Restriction except there is a continuation message
if Present (Expressions (N)) then
Check_Formal_Restriction
- ("named association cannot follow positional association",
+ ("named association cannot follow positional one",
First (Choices (First (Component_Associations (N)))));
end if;
-- In SPARK or ALFA, attributes of private types are only allowed if
-- the full type declaration is visible.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- and then Is_Entity_Name (P)
+ if Is_Entity_Name (P)
+ and then Present (Entity (P)) -- needed in some cases
and then Is_Type (Entity (P))
and then Is_Private_Type (P_Type)
and then not In_Open_Scopes (Scope (P_Type))
and then not In_Spec_Expression
then
- Error_Msg_FE
- ("|~~invisible attribute of}", N, First_Subtype (P_Type));
+ Error_Msg_Node_1 := First_Subtype (P_Type);
+ Check_Formal_Restriction ("invisible attribute of}", N);
end if;
-- Remaining processing depends on attribute
-- Pointer to node for literal providing max value
begin
- if Ignore_Rep_Clauses then
+ if Ignore_Rep_Clauses or else CodePeer_Mode then
return;
end if;
Enter_Name (Id);
if Present (Typ) then
- if Nkind (Typ) /= N_Identifier then
+ if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then
Check_Formal_Restriction ("subtype mark required", Typ);
end if;
-- Start of processing for Analyze_Declarations
begin
+ if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+ Check_Later_Vs_Basic_Declarations (L, During_Parsing => False);
+ end if;
+
D := First (L);
while Present (D) loop
-- mark and shall not be unconstrained. (The only exception to this
-- is the admission of declarations of constants of type String.)
- if not Nkind_In (Object_Definition (N), N_Identifier,
- N_Expanded_Name)
+ if not
+ Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name)
then
Check_Formal_Restriction
- ("subtype mark expected", Object_Definition (N));
+ ("subtype mark required", Object_Definition (N));
elsif Is_Array_Type (T)
and then not Is_Constrained (T)
if Nkind (Original_Node (N)) = N_Object_Declaration
and then Comes_From_Source (Original_Node (N))
- and then Formal_Verification_Mode -- 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)
then
Check_Formal_Restriction
("subtype of Boolean cannot have constraint", N);
end if;
- -- String subtype must have a lower bound of 1 in SPARK/ALFA. Note that
- -- we do not need to test for the non-static case here, since that was
- -- already taken care of in Process_Range_Expr_In_Decl.
-
- if Base_Type (T) = Standard_String
- and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
- then
+ if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then
declare
- Cstr : constant Node_Id := Constraint (Subtype_Indication (N));
- Drange : Node_Id;
- Low : Node_Id;
+ Cstr : constant Node_Id := Constraint (Subtype_Indication (N));
+ One_Cstr : Node_Id;
+ Low : Node_Id;
+ High : Node_Id;
begin
- if Nkind (Cstr) = N_Index_Or_Discriminant_Constraint
- and then List_Length (Constraints (Cstr)) = 1
- then
- Drange := First (Constraints (Cstr));
+ if Nkind (Cstr) = N_Index_Or_Discriminant_Constraint then
+ One_Cstr := First (Constraints (Cstr));
+ while Present (One_Cstr) loop
- if Nkind (Drange) = N_Range then
- Low := Low_Bound (Drange);
+ -- Index or discriminant constraint in SPARK or ALFA must be
+ -- a subtype mark.
- if Is_OK_Static_Expression (Low)
- and then Expr_Value (Low) /= 1
+ if not
+ Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name)
then
Check_Formal_Restriction
- ("String subtype must have lower bound of 1", N);
+ ("subtype mark required", One_Cstr);
+
+ -- String subtype must have a lower bound of 1 in SPARK.
+ -- Note that we do not need to test for the non-static case
+ -- here, since that was already taken care of in
+ -- Process_Range_Expr_In_Decl.
+
+ elsif Base_Type (T) = Standard_String then
+ Get_Index_Bounds (One_Cstr, Low, High);
+
+ if Is_OK_Static_Expression (Low)
+ and then Expr_Value (Low) /= 1
+ then
+ Check_Formal_Restriction
+ ("String subtype must have lower bound of 1", N);
+ end if;
end if;
- end if;
+
+ Next (One_Cstr);
+ end loop;
end if;
end;
end if;
-- as prefix.
if No (T) then
- Related_Id := Defining_Identifier (P);
+ Related_Id := Defining_Identifier (P);
else
Related_Id := T;
end if;
Nb_Index := 1;
while Present (Index) loop
- if Nkind (Index) /= N_Identifier then
+ if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then
Check_Formal_Restriction ("subtype mark required", Index);
end if;
-- Process subtype indication if one is present
if Present (Component_Typ) then
- if Nkind (Component_Typ) /= N_Identifier then
+ if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
Check_Formal_Restriction ("subtype mark required", Component_Typ);
end if;
-- Flag indicates whether an interpretation of the prefix is a
-- parameterless call that returns an access_to_subprogram.
+ procedure Check_Mixed_Parameter_And_Named_Associations;
+ -- Check that parameter and named associations are not mixed. This is
+ -- a restriction in SPARK mode.
+
function Name_Denotes_Function return Boolean;
-- If the type of the name is an access to subprogram, this may be the
-- type of a name, or the return type of the function being called. If
procedure No_Interpretation;
-- Output error message when no valid interpretation exists
+ --------------------------------------------------
+ -- Check_Mixed_Parameter_And_Named_Associations --
+ --------------------------------------------------
+
+ procedure Check_Mixed_Parameter_And_Named_Associations is
+ Actual : Node_Id;
+ Named_Seen : Boolean;
+ begin
+ Actual := First (Actuals);
+ Named_Seen := False;
+ while Present (Actual) loop
+ case Nkind (Actual) is
+ when N_Parameter_Association =>
+ if Named_Seen then
+ Check_Formal_Restriction
+ ("named association cannot follow positional one",
+ Actual);
+ exit;
+ end if;
+ when others =>
+ Named_Seen := True;
+ end case;
+
+ Next (Actual);
+ end loop;
+ end Check_Mixed_Parameter_And_Named_Associations;
+
---------------------------
-- Name_Denotes_Function --
---------------------------
-- Start of processing for Analyze_Call
begin
+ if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+ Check_Mixed_Parameter_And_Named_Associations;
+ end if;
+
-- Initialize the type of the result of the call to the error type,
-- which will be reset if the type is successfully resolved.
---------------------------
procedure Process_Function_Call is
- Actual : Node_Id;
-
+ Actual : Node_Id;
begin
Change_Node (N, N_Function_Call);
Set_Name (N, P);
with Nmake; use Nmake;
with Opt; use Opt;
with Restrict; use Restrict;
+with Rident; use Rident;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
----------------------------
procedure Check_Unreachable_Code (N : Node_Id) is
- Error_Loc : Source_Ptr;
- P : Node_Id;
+ Error_Node : Node_Id;
+ P : Node_Id;
begin
if Is_List_Member (N)
-- someone could branch to the label, so we just ignore it, unless
-- we are in formal mode where goto statements are not allowed.
- if Nkind (Nxt) = N_Label and then not Formal_Verification_Mode then
+ if Nkind (Nxt) = N_Label
+ and then not (Formal_Verification_Mode
+ or else Restriction_Check_Required (SPARK))
+ then
return;
-- Otherwise see if we have a real statement following us
-- at removing warnings in deleted code, and this is one
-- warning we would prefer NOT to have removed.
- Error_Loc := Sloc (Nxt);
+ Error_Node := Nxt;
-- If we have unreachable code, analyze and remove the
-- unreachable code, since it is useless and we don't
-- Now issue the warning (or error in formal mode)
- if Formal_Verification_Mode then
- Error_Msg
- ("|~~unreachable code is not allowed", Error_Loc);
+ if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+ Check_Formal_Restriction
+ ("unreachable code is not allowed", Error_Node);
else
- Error_Msg ("?unreachable code!", Error_Loc);
+ Error_Msg ("?unreachable code!", Sloc (Error_Node));
end if;
end if;
if Nkind (P) = N_Error then
return;
+ end if;
+
+ -- Selector name cannot be a character literal or an operator symbol in
+ -- SPARK.
+
+ if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+ if Nkind (Selector_Name (N)) = N_Character_Literal then
+ Check_Formal_Restriction
+ ("character literal cannot be prefixed", N);
+ elsif Nkind (Selector_Name (N)) = N_Operator_Symbol then
+ Check_Formal_Restriction ("operator symbol cannot be prefixed", N);
+ end if;
+ end if;
-- If the selector already has an entity, the node has been constructed
-- in the course of expansion, and is known to be valid. Do not verify
-- that it is defined for the type (it may be a private component used
-- in the expansion of record equality).
- elsif Present (Entity (Selector_Name (N))) then
+ if Present (Entity (Selector_Name (N))) then
if No (Etype (N))
or else Etype (N) = Any_Type
then
-- Selector name is restricted in SPARK
- if SPARK_Mode then
+ if SPARK_Mode or else Restriction_Check_Required (SPARK) then
if Is_Subprogram (P_Name) then
- Error_Msg_F
- ("|~~prefix of expanded name cannot be a subprogram", P);
+ Check_Formal_Restriction
+ ("prefix of expanded name cannot be a subprogram", P);
elsif Ekind (P_Name) = E_Loop then
- Error_Msg_F
- ("|~~prefix of expanded name cannot be a loop statement", P);
+ Check_Formal_Restriction
+ ("prefix of expanded name cannot be a loop statement", P);
end if;
end if;
with Output; use Output;
with Opt; use Opt;
with Restrict; use Restrict;
+with Rident; use Rident;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
end if;
end Cannot_Raise_Constraint_Error;
+ ---------------------------------------
+ -- Check_Later_Vs_Basic_Declarations --
+ ---------------------------------------
+
+ procedure Check_Later_Vs_Basic_Declarations
+ (Decls : List_Id;
+ During_Parsing : Boolean)
+ is
+ Body_Sloc : Source_Ptr;
+ Decl : Node_Id;
+ begin
+ Decl := First (Decls);
+
+ -- Loop through sequence of basic declarative items
+
+ Outer : while Present (Decl) loop
+ if Nkind (Decl) /= N_Subprogram_Body
+ and then Nkind (Decl) /= N_Package_Body
+ and then Nkind (Decl) /= N_Task_Body
+ and then Nkind (Decl) not in N_Body_Stub
+ then
+ Next (Decl);
+
+ -- Once a body is encountered, we only allow later declarative
+ -- items. The inner loop checks the rest of the list.
+
+ else
+ Body_Sloc := Sloc (Decl);
+
+ Inner : while Present (Decl) loop
+ if (Nkind (Decl) not in N_Later_Decl_Item
+ or else (not During_Parsing
+ and then
+ Nkind (Decl) = N_Package_Declaration))
+ and then Nkind (Decl) /= N_Pragma
+ then
+ if During_Parsing then
+ if Ada_Version = Ada_83 then
+ Error_Msg_Sloc := Body_Sloc;
+ Error_Msg_N
+ ("(Ada 83) decl cannot appear after body#", Decl);
+ end if;
+ else
+ Error_Msg_Sloc := Body_Sloc;
+ Check_Formal_Restriction
+ ("decl cannot appear after body#", Decl);
+ end if;
+ end if;
+
+ Next (Decl);
+ end loop Inner;
+ end if;
+ end loop Outer;
+ end Check_Later_Vs_Basic_Declarations;
+
-----------------------------------------
-- Check_Dynamically_Tagged_Expression --
-----------------------------------------
procedure Process_End_Label
(N : Node_Id;
Typ : Character;
- Ent : Entity_Id)
+ Ent : Entity_Id)
is
Loc : Source_Ptr;
Nam : Node_Id;
Get_Decoded_Name_String (Chars (Endl));
Set_Sloc (Endl, Sloc (Endl) + Source_Ptr (Name_Len));
+
+ else
+ -- In SPARK mode, no missing label is allowed for packages and
+ -- subprogram bodies. Detect those cases by testing whether
+ -- Process_End_Label was called for a body (Typ = 't') or a package.
+
+ if (SPARK_Mode or else Restriction_Check_Required (SPARK))
+ and then (Typ = 't' or else Ekind (Ent) = E_Package)
+ then
+ Error_Msg_Node_1 := Endl;
+ Check_Formal_Restriction ("`END &` required", Endl, Force => True);
+ end if;
end if;
-- Now generate the e/t reference
-- not necessarily mean that CE could be raised, but a response of True
-- means that for sure CE cannot be raised.
+ procedure Check_Later_Vs_Basic_Declarations
+ (Decls : List_Id;
+ During_Parsing : Boolean);
+ -- If During_Parsing is True, check for misplacement of later vs basic
+ -- declarations in Ada 83. If During_Parsing is False, and the SPARK
+ -- restriction is set, do the same: although SPARK 95 removes the
+ -- distinction between initial and later declarative items, the distinction
+ -- remains in the Examiner (JB01-005). Note that the Examiner does not
+ -- count package declarations in later declarative items.
+
procedure Check_Dynamically_Tagged_Expression
(Expr : Node_Id;
Typ : Entity_Id;
projects / gcc.git / commitdiff