+2011-08-01 Yannick Moy <moy@adacore.com>
+
+ * sem_util.ads, sem_util.adb, par.adb, par_util.adb
+ (Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move
+ procedures out of these packages.
+ * errout.ads, errout.adb
+ (Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move
+ procedures in of this package
+ (Formal_Error_Msg_NE): new procedure for wrapper on Error_Msg_NE
+ * par-ch5.adb (Parse_Decls_Begin_End): issue syntax error in SPARK mode
+ on misplaced later vs initial declarations, like in Ada 83
+ * sem_attr.adb (Processing for Analyze_Attribute): issue error in
+ formal mode on attribute of private type whose full type declaration
+ is not visible
+ * sem_ch3.adb (Analyze_Declarations): issue error in formal mode on a
+ package declaration inside a package specification
+ (Analyze_Full_Type_Declaration): issue error in formal mode on
+ controlled type or discriminant type
+ * sem_ch6.adb (Analyze_Subprogram_Specification): only issue error on
+ user-defined operator means that it should come from the source
+ (New_Overloaded_Entity): issue error in formal mode on overloaded
+ entity.
+ * sem_ch6.ads, sem_ch13.ads: typos in comments.
+
+2011-08-01 Thomas Quinot <quinot@adacore.com>
+
+ * atree.adb: Minor reformatting.
+ * checks.adb: Minor reformatting.
+
2011-08-01 Vincent Celier <celier@adacore.com>
* s-parame-vms-ia64.ads: Fix typo in comment
Nodes.Table (New_Id).Link := Empty_List_Or_Node;
Nodes.Table (New_Id).In_List := False;
- -- If the original is marked as a rewrite insertion, then unmark
- -- the copy, since we inserted the original, not the copy.
+ -- If the original is marked as a rewrite insertion, then unmark the
+ -- copy, since we inserted the original, not the copy.
Nodes.Table (New_Id).Rewrite_Ins := False;
pragma Debug (New_Node_Debugging_Output (New_Id));
-- Clear Is_Overloaded since we cannot have semantic interpretations
- -- of this new node
+ -- of this new node.
if Nkind (Source) in N_Subexpr then
Set_Is_Overloaded (New_Id, False);
function Entity_Of_Prefix return Entity_Id;
-- Returns the entity of the prefix of N (or Empty if not found)
+ ----------------------
+ -- Entity_Of_Prefix --
+ ----------------------
+
function Entity_Of_Prefix return Entity_Id is
P : Node_Id := Prefix (N);
begin
A_Ent : constant Entity_Id := Entity_Of_Prefix;
Sub : Node_Id;
+ -- Start of processing for Generate_Index_Checks
+
begin
-- Ignore call if the prefix is not an array since we have a serious
-- error in the sources. Ignore it also if index checks are suppressed
-- Generate a raise of constraint error with the appropriate reason and
-- a condition of the form:
- -- Base_Type(Sub) not in array'range (subscript)
+ -- Base_Type (Sub) not in Array'Range (Subscript)
-- Note that the reason we generate the conversion to the base type here
-- is that we definitely want the range check to take place, even if it
Duplicate_Subexpr_Move_Checks (Sub)),
Right_Opnd =>
Make_Attribute_Reference (Loc,
- Prefix => New_Reference_To (Etype (A), Loc),
+ Prefix => New_Reference_To (Etype (A), Loc),
Attribute_Name => Name_Range)),
Reason => CE_Index_Check_Failed));
end if;
then
Range_N :=
Make_Attribute_Reference (Loc,
- Prefix => New_Reference_To (Etype (A_Idx), Loc),
+ Prefix =>
+ New_Reference_To (Etype (A_Idx), Loc),
Attribute_Name => Name_Range);
-- For arrays with non-constant bounds we cannot generate
return S;
end First_Sloc;
+ ----------------------
+ -- Formal_Error_Msg --
+ ----------------------
+
+ procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr) is
+ begin
+ pragma Assert (Formal_Verification_Mode);
+ Error_Msg ("(" & Formal_Language & ") " & Msg, Flag_Location);
+ end Formal_Error_Msg;
+
+ ------------------------
+ -- Formal_Error_Msg_N --
+ ------------------------
+
+ procedure Formal_Error_Msg_N (Msg : String; N : Node_Id) is
+ begin
+ pragma Assert (Formal_Verification_Mode);
+ Error_Msg_N ("(" & Formal_Language & ") " & Msg, N);
+ end Formal_Error_Msg_N;
+
+ -------------------------
+ -- Formal_Error_Msg_NE --
+ -------------------------
+
+ procedure Formal_Error_Msg_NE
+ (Msg : String;
+ N : Node_Or_Entity_Id;
+ E : Node_Or_Entity_Id) is
+ begin
+ pragma Assert (Formal_Verification_Mode);
+ Error_Msg_NE ("(" & Formal_Language & ") " & Msg, N, E);
+ end Formal_Error_Msg_NE;
+
+ -------------------------
+ -- Formal_Error_Msg_SP --
+ -------------------------
+
+ procedure Formal_Error_Msg_SP (Msg : String) is
+ begin
+ pragma Assert (Formal_Verification_Mode);
+ Error_Msg_SP ("(" & Formal_Language & ") " & Msg);
+ end Formal_Error_Msg_SP;
+
----------------
-- Initialize --
----------------
-- where the expression is parenthesized, an attempt is made to include
-- the parentheses (i.e. to return the location of the initial paren).
+ procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr);
+ -- Wrapper on Error_Msg which adds a prefix to Msg giving the name of
+ -- the formal language analyzed (spark or alfa)
+
+ procedure Formal_Error_Msg_N (Msg : String; N : Node_Id);
+ -- Wrapper on Error_Msg_N which adds a prefix to Msg giving the name of
+ -- the formal language analyzed (spark or alfa)
+
+ procedure Formal_Error_Msg_NE
+ (Msg : String;
+ N : Node_Or_Entity_Id;
+ E : Node_Or_Entity_Id);
+ -- Wrapper on Error_Msg_NE which adds a prefix to Msg giving the name of
+ -- the formal language analyzed (spark or alfa)
+
+ procedure Formal_Error_Msg_SP (Msg : String);
+ -- Wrapper on Error_Msg_SP which adds a prefix to Msg giving the name of
+ -- the formal language analyzed (spark or alfa)
+
procedure Purge_Messages (From : Source_Ptr; To : Source_Ptr)
renames Erroutc.Purge_Messages;
-- All error messages whose location is in the range From .. To (not
begin
Decls := P_Declarative_Part;
- -- Check for misplacement of later vs basic declarations in Ada 83
+ -- 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)
- if Ada_Version = Ada_83 then
+ if Ada_Version = Ada_83 or else SPARK_Mode then
Decl := First (Decls);
-- Loop through sequence of basic declarative items
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;
+ Formal_Error_Msg_N
+ ("decl cannot appear after body#", Decl);
end if;
end if;
null;
end Discard_Junk_Node;
- -------------------------
- -- Formal_Error_Msg_SP --
- -------------------------
-
- procedure Formal_Error_Msg_SP (Msg : String) is
- begin
- pragma Assert (Formal_Verification_Mode);
- Error_Msg_SP ("(" & Formal_Language & ") " & Msg);
- end Formal_Error_Msg_SP;
-
------------
-- Ignore --
------------
-- the argument. A typical use is to skip by some junk that is not
-- expected in the current context.
- procedure Formal_Error_Msg_SP (Msg : String);
- -- Wrapper on Errout.Error_Msg_SP which adds a prefix to Msg giving
- -- the name of the formal language analyzed (spark or alfa)
-
procedure Ignore (T : Token_Type);
-- If current token matches T, then give an error message and skip
-- past it, otherwise the call has no effect at all. T may be any
end if;
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 Is_Entity_Name (P)
+ 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
+ Formal_Error_Msg_NE
+ ("invisible attribute of}", N, First_Subtype (P_Type));
+ end if;
+
-- Remaining processing depends on attribute
case Attr_Id is
(N : Node_Id;
E : Entity_Id;
L : List_Id);
- -- This procedure is called to analyze aspect specifications for node N. E
- -- is the corresponding entity declared by the declaration node N, and L is
- -- the list of aspect specifications for this node. If L is No_List, the
+ -- This procedure is called to analyze aspect specifications for node N.
+ -- E is the corresponding entity declared by the declaration node N, and L
+ -- is the list of aspect specifications for this node. If L is No_List, the
-- call is ignored. Note that we can't use a simpler interface of just
-- passing the node N, since the analysis of the node may cause it to be
-- rewritten to a node not permitting aspect specifications.
D := First (L);
while Present (D) loop
+ -- Package specification cannot contain a package declaration in
+ -- SPARK or ALFA
+
+ if Formal_Verification_Mode
+ and then Nkind (D) = N_Package_Declaration
+ and then Nkind (Parent (L)) = N_Package_Specification
+ then
+ Formal_Error_Msg_N ("package specification cannot contain "
+ & "a package declaration", D);
+ end if;
+
-- Complete analysis of declaration
Analyze (D);
return;
end if;
+ if Formal_Verification_Mode then
+
+ -- Controlled type is not allowed in SPARK and ALFA
+
+ if Is_Visibly_Controlled (T) then
+ Formal_Error_Msg_N ("controlled type is not allowed", N);
+ end if;
+
+ -- Discriminant type is not allowed in SPARK and ALFA
+
+ if Present (Discriminant_Specifications (N)) then
+ Formal_Error_Msg_N ("discriminant type is not allowed", N);
+ end if;
+ end if;
+
-- Some common processing for all types
Set_Depends_On_Private (T, Has_Private_Component (T));
-- User-defined operator is not allowed in SPARK or ALFA
if Formal_Verification_Mode
+ and then Comes_From_Source (N)
and then Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
then
Formal_Error_Msg_N ("user-defined operator is not allowed", N);
Check_Overriding_Indicator
(S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
+ -- Overloading is not allowed in SPARK or ALFA
+
+ if Formal_Verification_Mode
+ and then Comes_From_Source (S)
+ then
+ Error_Msg_Sloc := Sloc (Homonym (S));
+ Formal_Error_Msg_N ("overloading not allowed with entity#", S);
+ end if;
+
-- If S is a derived operation for an untagged type then by
-- definition it's not a dispatching operation (even if the parent
-- operation was dispatching), so we don't call
-- Process new overloaded entity. Overloaded entities are created by
-- enumeration type declarations, subprogram specifications, entry
-- declarations, and (implicitly) by type derivations. Derived_Type non-
- -- Empty indicates that this is subprogram derived for that type.
+ -- Empty indicates that this is a subprogram derived for that type.
procedure Process_Formals (T : List_Id; Related_Nod : Node_Id);
-- Enter the formals in the scope of the subprogram or entry, and
-- Copyright (C) 1992-2011, 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- --
+-- terms of the GNU Genconflieral Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
end if;
end First_Actual;
- ----------------------
- -- Formal_Error_Msg --
- ----------------------
-
- procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr) is
- begin
- pragma Assert (Formal_Verification_Mode);
- Error_Msg ("(" & Formal_Language & ") " & Msg, Flag_Location);
- end Formal_Error_Msg;
-
- ------------------------
- -- Formal_Error_Msg_N --
- ------------------------
-
- procedure Formal_Error_Msg_N (Msg : String; N : Node_Id) is
- begin
- pragma Assert (Formal_Verification_Mode);
- Error_Msg_N ("(" & Formal_Language & ") " & Msg, N);
- end Formal_Error_Msg_N;
-
-----------------------
-- Gather_Components --
-----------------------
-- is always the expression (not the N_Parameter_Association nodes,
-- even if named association is used).
- procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr);
- -- Wrapper on Errout.Error_Msg which adds a prefix to Msg giving
- -- the name of the formal language analyzed (spark or alfa)
-
- procedure Formal_Error_Msg_N (Msg : String; N : Node_Id);
- -- Wrapper on Errout.Error_Msg_N which adds a prefix to Msg giving
- -- the name of the formal language analyzed (spark or alfa)
-
procedure Gather_Components
(Typ : Entity_Id;
Comp_List : Node_Id;
projects / platform / upstream / gcc.git / commitdiff