+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * errout.adb, errout.ads (Check_Formal_Restriction): new procedure
+ which issues an error in formal mode if its argument node is originally
+ from source
+ * sem_ch3.adb (Analyze_Full_Type_Declaration): move test that a type
+ has a discriminant specification so that it does not include the case
+ of derived types
+ (Derived_Type_Declaration): move here the test that a derived type has a
+ discriminant specification
+ * sem_aggr.adb (Resolve_Record_Aggregate): test the presence of the
+ first element of a component association before accessing its choices
+ (presence of component association is not enough)
+ * exp_ch6.adb (Expand_N_Subprogram_Declaration): test if a subprogram
+ declaration is a library item before accessing the next element in a
+ list, as library items are not member of lists
+ * sem_attr.adb, sem_ch11.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb,
+ sem_ch8.adb, sem_ch9.adb, sem_res.adb, sem_util.adb: use
+ Check_Formal_Restriction whenever possible.
+
2011-08-02 Ed Schonberg <schonberg@adacore.com>
* sem_ch3.adb (Find_Type_Of_Object): In ASIS mode, create an itype
end if;
end Change_Error_Text;
+ ------------------------------
+ -- Check_Formal_Restriction --
+ ------------------------------
+
+ procedure Check_Formal_Restriction (Msg : String; N : Node_Id) is
+ begin
+ if Formal_Verification_Mode
+ and then Comes_From_Source (Original_Node (N))
+ then
+ Error_Msg_F ("|~~" & Msg, N);
+ end if;
+ end Check_Formal_Restriction;
+
------------------------
-- Compilation_Errors --
------------------------
-- the given text. This text may contain insertion characters in the
-- usual manner, and need not be the same length as the original text.
+ procedure Check_Formal_Restriction (Msg : String; N : Node_Id);
+ -- Provides a wrappper on Error_Msg_F which prepends the special characters
+ -- "|~~" (error not serious, language prepended) provided:
+ -- * the current mode is formal verification.
+ -- * the node N comes originally from source.
+ -- Otherwise, does nothing.
+
function First_Node (C : Node_Id) return Node_Id;
-- Given a construct C, finds the first node in the construct, i.e. the
-- one with the lowest Sloc value. This is useful in placing error msgs.
-- In SPARK or ALFA, subprogram declarations are only allowed in
-- package specifications.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- and then Nkind (Parent (N)) /= N_Package_Specification
- then
- if Present (Next (N))
+ if Nkind (Parent (N)) /= N_Package_Specification then
+ if Nkind (Parent (N)) = N_Compilation_Unit then
+ Check_Formal_Restriction
+ ("subprogram declaration is not a library item", N);
+
+ elsif Present (Next (N))
and then Nkind (Next (N)) = N_Pragma
and then Get_Pragma_Id (Pragma_Name (Next (N))) = Pragma_Import
then
null;
else
- Error_Msg_F ("|~~subprogram declaration is not allowed here", N);
+ Check_Formal_Restriction
+ ("subprogram declaration is not allowed here", N);
end if;
end if;
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;
+ -- An unqualified aggregate is restricted in SPARK or ALFA to:
+ -- * an 'aggregate item' inside an aggregate for a multi-dimensional
+ -- array.
+ -- * 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
+ Check_Formal_Restriction
+ ("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
+ Check_Formal_Restriction
+ ("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);
+ elsif Is_Record_Type (Etype (N)) then
+ Check_Formal_Restriction
+ ("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;
-- 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);
+ if not Is_Static_Expression (Choice) then
+ Check_Formal_Restriction
+ ("choice should be static", Choice);
end if;
end if;
-- 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)
+ if Is_Entity_Name (A)
and then Is_Type (Entity (A))
then
- Error_Msg_F ("|~~ancestor part cannot be a subtype mark", A);
+ Check_Formal_Restriction
+ ("ancestor part cannot be a subtype mark", A);
end if;
if not Is_Tagged_Type (Typ) then
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.
+ -- * 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))
+ if Present (Component_Associations (N))
+ and then Present (First (Component_Associations (N)))
then
+
if Present (Expressions (N)) then
- Error_Msg_F
- ("|~~named association cannot follow positional association",
+ Check_Formal_Restriction
+ ("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 "
+ Check_Formal_Restriction
+ ("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);
+ Check_Formal_Restriction
+ ("record aggregate cannot contain OTHERS", Assoc);
end if;
-
Assoc := Next (Assoc);
end loop;
end;
-- the full type declaration is visible
if Formal_Verification_Mode
+ and then Comes_From_Source (Original_Node (N))
and then Is_Entity_Name (P)
and then Is_Type (Entity (P))
and then Is_Private_Type (P_Type)
P : Node_Id;
begin
- -- Raise statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~raise statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
+ Check_Formal_Restriction ("raise statement is not allowed", N);
Check_Unreachable_Code (N);
-- Check exception restrictions on the original source
-- Start of processing for Analyze_Raise_xxx_Error
begin
- -- Source-code raise statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (N)
- then
- Error_Msg_F ("|~~raise statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("raise statement is not allowed", N);
if No (Etype (N)) then
Set_Etype (N, Standard_Void_Type);
Enclosing_Prot_Type : Entity_Id := Empty;
begin
- -- Access type is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (N)
- then
- Error_Msg_F ("|~~access type is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("access type is not allowed", N);
if Is_Entry (Current_Scope)
and then Is_Task_Type (Etype (Scope (Current_Scope)))
-- Start of processing for Access_Subprogram_Declaration
begin
- -- Access type is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (T_Def)
- then
- Error_Msg_F ("|~~access type is not allowed", T_Def);
- end if;
+ Check_Formal_Restriction ("access type is not allowed", T_Def);
-- Associate the Itype node with the inner full-type declaration or
-- subprogram spec or entry body. This is required to handle nested
S : constant Node_Id := Subtype_Indication (Def);
P : constant Node_Id := Parent (Def);
begin
- -- Access type is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (Def)
- then
- Error_Msg_F ("|~~access type is not allowed", Def);
- end if;
+ Check_Formal_Restriction ("access type is not allowed", Def);
-- Check for permissible use of incomplete type
-- Package specification cannot contain a package declaration in
-- SPARK or ALFA.
- if Formal_Verification_Mode
- and then Nkind (D) = N_Package_Declaration
+ if Nkind (D) = N_Package_Declaration
and then Nkind (Parent (L)) = N_Package_Specification
then
- Error_Msg_F ("|~~package specification cannot contain "
- & "a package declaration", D);
+ Check_Formal_Restriction ("package specification cannot contain "
+ & "a package declaration", D);
end if;
-- Complete analysis of declaration
when N_Derived_Type_Definition =>
null;
- -- For record types, discriminants are allowed
+ -- For record types, discriminants are allowed, unless we are in
+ -- SPARK or ALFA.
when N_Record_Definition =>
- null;
+ if Present (Discriminant_Specifications (N)) then
+ Check_Formal_Restriction
+ ("discriminant type is not allowed",
+ Defining_Identifier
+ (First (Discriminant_Specifications (N))));
+ end if;
when others =>
if Present (Discriminant_Specifications (N)) then
return;
end if;
- if Formal_Verification_Mode then
+ -- Controlled type is not allowed in SPARK and ALFA
- -- Controlled type is not allowed in SPARK and ALFA
-
- if Is_Visibly_Controlled (T) then
- Error_Msg_F ("|~~controlled type is not allowed", N);
- end if;
-
- -- Discriminant type is not allowed in SPARK and ALFA
-
- if Present (Discriminant_Specifications (N)) then
- Error_Msg_F ("|~~discriminant type is not allowed", N);
- end if;
+ if Is_Visibly_Controlled (T) then
+ Check_Formal_Restriction ("controlled type is not allowed", N);
end if;
-- Some common processing for all types
T : Entity_Id;
begin
- -- Incomplete type is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- then
- Error_Msg_F ("|~~incomplete type is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("incomplete type is not allowed", N);
Generate_Definition (Defining_Identifier (N));
-- is considered, so that the Object_Definition node is still the same
-- as in source code.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- then
- -- In SPARK or ALFA, the nominal subtype shall be given by a subtype
- -- mark and shall not be unconstrained. (The only exception to this
- -- is the admission of declarations of constants of type String.)
+ -- In SPARK or ALFA, the nominal subtype shall be given by a subtype
+ -- 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)
- then
- Error_Msg_F ("|~~subtype mark expected", Object_Definition (N));
- elsif Is_Array_Type (T)
- and then not Is_Constrained (T)
- and then T /= Standard_String
- then
- Error_Msg_F ("|~~subtype mark of constrained type expected",
- Object_Definition (N));
- else
- null;
- end if;
+ if not Nkind_In (Object_Definition (N),
+ N_Identifier,
+ N_Expanded_Name)
+ then
+ Check_Formal_Restriction
+ ("subtype mark expected", Object_Definition (N));
+ elsif Is_Array_Type (T)
+ and then not Is_Constrained (T)
+ and then T /= Standard_String
+ then
+ Check_Formal_Restriction ("subtype mark of constrained type expected",
+ Object_Definition (N));
+ else
+ null;
+ end if;
- -- There are no aliased objects in SPARK or ALFA
+ -- There are no aliased objects in SPARK or ALFA
- if Aliased_Present (N) then
- Error_Msg_F ("|~~aliased object is not allowed", N);
- end if;
+ if Aliased_Present (N) then
+ Check_Formal_Restriction ("aliased object is not allowed", N);
end if;
-- Process initialization expression if present and not in error
-- Subtype of Boolean is not allowed to have a constraint in SPARK or
-- ALFA.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- and then Is_Boolean_Type (T)
+ if Is_Boolean_Type (T)
and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
then
- Error_Msg_F ("|~~subtype of Boolean cannot have constraint", N);
+ Check_Formal_Restriction
+ ("subtype of Boolean cannot have constraint", N);
end if;
-- In the case where there is no constraint given in the subtype
-- Subtype of unconstrained array without constraint is not allowed
-- in SPARK or ALFA.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- and then Is_Array_Type (T)
+ if Is_Array_Type (T)
and then not Is_Constrained (T)
then
- Error_Msg_F
- ("|~~subtype of unconstrained array must have constraint", N);
+ Check_Formal_Restriction
+ ("subtype of unconstrained array must have constraint", N);
end if;
- -- Proceed with analysis
-
case Ekind (T) is
when Array_Kind =>
Set_Ekind (Id, E_Array_Subtype);
else
pragma Assert (Nkind (C) = N_Digits_Constraint);
- -- Digits constraint is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (S))
- then
- Error_Msg_F ("|~~digits constraint is not allowed", S);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("digits constraint is not allowed", S);
Digits_Expr := Digits_Expression (C);
Analyze_And_Resolve (Digits_Expr, Any_Integer);
if Nkind (C) = N_Digits_Constraint then
- -- Digits constraint is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (S))
- then
- Error_Msg_F ("|~~digits constraint is not allowed", S);
- end if;
-
- -- Proceed with analysis
-
+ Check_Formal_Restriction ("digits constraint is not allowed", S);
Check_Restriction (No_Obsolescent_Features, C);
if Warn_On_Obsolescent_Feature then
-- Delta constraint present
if Nkind (C) = N_Delta_Constraint then
- -- Delta constraint is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (S))
- then
- Error_Msg_F ("|~~delta constraint is not allowed", S);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("delta constraint is not allowed", S);
Check_Restriction (No_Obsolescent_Features, C);
if Warn_On_Obsolescent_Feature then
Bound_Val : Ureal;
begin
- -- Decimal fixed point type is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (Def))
- then
- Error_Msg_F
- ("|~~decimal fixed point type is not allowed", Def);
- end if;
-
- -- Proceed with analysis
-
+ Check_Formal_Restriction
+ ("decimal fixed point type is not allowed", Def);
Check_Restriction (No_Fixed_Point, Def);
-- Create implicit base type
end if;
-- Only composite types other than array types are allowed to have
+ -- discriminants. In SPARK in ALFA, no types are allowed to have
-- discriminants.
- if Present (Discriminant_Specifications (N))
- and then (Is_Elementary_Type (Parent_Type)
- or else Is_Array_Type (Parent_Type))
- and then not Error_Posted (N)
- then
- Error_Msg_N
- ("elementary or array type cannot have discriminants",
- Defining_Identifier (First (Discriminant_Specifications (N))));
- Set_Has_Discriminants (T, False);
+ if Present (Discriminant_Specifications (N)) then
+ if (Is_Elementary_Type (Parent_Type)
+ or else Is_Array_Type (Parent_Type))
+ and then not Error_Posted (N)
+ then
+ Error_Msg_N
+ ("elementary or array type cannot have discriminants",
+ Defining_Identifier (First (Discriminant_Specifications (N))));
+ Set_Has_Discriminants (T, False);
+ else
+ Check_Formal_Restriction ("discriminant type is not allowed", N);
+ end if;
end if;
-- In Ada 83, a derived type defined in a package specification cannot
-- In SPARK or ALFA, there are no derived type definitions other than
-- type extensions of tagged record types.
- if Formal_Verification_Mode
- and then No (Extension)
- then
- Error_Msg_F ("|~~derived type is not allowed", N);
+ if No (Extension) then
+ Check_Formal_Restriction ("derived type is not allowed", N);
end if;
end Derived_Type_Declaration;
C : Node_Id;
begin
- -- Allocator is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~allocator is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("allocator is not allowed", N);
-- Deal with allocator restrictions
return;
end if;
- -- Conditional expression is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~conditional expression is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("conditional expression is not allowed", N);
Else_Expr := Next (Then_Expr);
-- Start of processing for Analyze_Explicit_Dereference
begin
- -- Explicit dereference is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~explicit dereference is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("explicit dereference is not allowed", N);
Analyze (P);
Set_Etype (N, Any_Type);
procedure Analyze_Null (N : Node_Id) is
begin
- -- Null is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~null is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("null is not allowed", N);
Set_Etype (N, Any_Access);
end Analyze_Null;
Iterator : Node_Id;
begin
- -- Quantified expression is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~quantified expression is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("quantified expression is not allowed", N);
Set_Etype (Ent, Standard_Void_Type);
Set_Parent (Ent, N);
-- Start of processing for Analyze_Slice
begin
- -- Slice is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~slice is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("slice is not allowed", N);
Analyze (P);
Analyze (D);
HSS : constant Node_Id := Handled_Statement_Sequence (N);
begin
- -- Block statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode
- and then Comes_From_Source (N)
- then
- Error_Msg_F ("|~~block statement is not allowed", N);
- end if;
+ Check_Formal_Restriction ("block statement is not allowed", N);
-- If no handled statement sequence is present, things are really
-- messed up, and we just return immediately (this is a defence
-- A case statement with a single OTHERS alternative is not allowed
-- in SPARK or ALFA.
- if Formal_Verification_Mode
- and then Others_Present
+ if Others_Present
and then List_Length (Alternatives (N)) = 1
then
- Error_Msg_F
- ("|~~OTHERS as unique case alternative is not allowed", N);
+ Check_Formal_Restriction
+ ("OTHERS as unique case alternative is not allowed", N);
end if;
if Exp_Type = Universal_Integer and then not Others_Present then
if not In_Open_Scopes (U_Name) or else Ekind (U_Name) /= E_Loop then
Error_Msg_N ("invalid loop name in exit statement", N);
return;
- elsif Formal_Verification_Mode
- and then Has_Loop_In_Inner_Open_Scopes (U_Name)
- then
- Error_Msg_F
- ("|~~exit label must name the closest enclosing loop", N);
- return;
else
+ if Has_Loop_In_Inner_Open_Scopes (U_Name) then
+ Check_Formal_Restriction
+ ("exit label must name the closest enclosing loop", N);
+ end if;
+
Set_Has_Exit (U_Name);
end if;
-
else
U_Name := Empty;
end if;
-- In formal mode, verify that the exit statement respects the SPARK
-- restrictions.
- if Formal_Verification_Mode then
- if Present (Cond) then
- if Nkind (Parent (N)) /= N_Loop_Statement then
- Error_Msg_F
- ("|~~exit with when clause must be directly in loop", N);
- end if;
+ if Present (Cond) then
+ if Nkind (Parent (N)) /= N_Loop_Statement then
+ Check_Formal_Restriction
+ ("exit with when clause must be directly in loop", N);
+ end if;
- else
- if Nkind (Parent (N)) /= N_If_Statement then
- if Nkind (Parent (N)) = N_Elsif_Part then
- Error_Msg_F ("|~~exit must be in IF without ELSIF", N);
- else
- Error_Msg_F ("|~~exit must be directly in IF", N);
- end if;
+ else
+ if Nkind (Parent (N)) /= N_If_Statement then
+ if Nkind (Parent (N)) = N_Elsif_Part then
+ Check_Formal_Restriction
+ ("exit must be in IF without ELSIF", N);
+ else
+ Check_Formal_Restriction ("exit must be directly in IF", N);
+ end if;
- elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
- Error_Msg_F ("|~~exit must be in IF directly in loop", N);
+ elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
+ Check_Formal_Restriction
+ ("exit must be in IF directly in loop", N);
-- First test the presence of ELSE, so that an exit in an ELSE
-- leads to an error mentioning the ELSE.
- elsif Present (Else_Statements (Parent (N))) then
- Error_Msg_F ("|~~exit must be in IF without ELSE", N);
+ elsif Present (Else_Statements (Parent (N))) then
+ Check_Formal_Restriction ("exit must be in IF without ELSE", N);
-- An exit in an ELSIF does not reach here, as it would have been
-- detected in the case (Nkind (Parent (N)) /= N_If_Statement).
- elsif Present (Elsif_Parts (Parent (N))) then
- Error_Msg_F ("|~~exit must be in IF without ELSIF", N);
- end if;
+ elsif Present (Elsif_Parts (Parent (N))) then
+ Check_Formal_Restriction ("exit must be in IF without ELSIF", N);
end if;
end if;
Label_Ent : Entity_Id;
begin
- -- Goto statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~goto statement is not allowed", N);
- end if;
+ Check_Formal_Restriction ("goto statement is not allowed", N);
-- Actual semantic checks
-- Loop parameter specification must include subtype mark in
-- SPARK or ALFA.
- if Formal_Verification_Mode
- and then Nkind (DS) = N_Range
- then
- Error_Msg_F ("|~~loop parameter specification must "
- & "include subtype mark", N);
+ if Nkind (DS) = N_Range then
+ Check_Formal_Restriction ("loop parameter specification "
+ & "must include subtype mark", N);
end if;
-- Now analyze the subtype definition. If it is a range, create
Scop : constant Entity_Id := Current_Scope;
begin
- -- Abstract subprogram is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~abstract subprogram is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("abstract subprogram is not allowed", N);
Generate_Definition (Designator);
Set_Is_Abstract_Subprogram (Designator);
-- The only RETURN allowed in SPARK or ALFA is as the last statement
-- of the function.
- if Formal_Verification_Mode
- and then Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements
+ if Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements
and then
(Nkind (Parent (Parent (N))) /= N_Subprogram_Body
or else Present (Next (N)))
then
- Error_Msg_F
- ("|~~RETURN should be the last statement in function", N);
+ Check_Formal_Restriction
+ ("RETURN should be the last statement in function", N);
end if;
else
- -- Extended return is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~extended RETURN is not allowed", N);
- end if;
+ Check_Formal_Restriction ("extended RETURN is not allowed", N);
-- Analyze parts specific to extended_return_statement:
if Result_Definition (N) /= Error then
if Nkind (Result_Definition (N)) = N_Access_Definition then
- -- Access result is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F
- ("|~~access result is not allowed", Result_Definition (N));
- end if;
+ Check_Formal_Restriction
+ ("access result is not allowed", Result_Definition (N));
-- Ada 2005 (AI-254): Handle anonymous access to subprograms
-- Unconstrained array as result is not allowed in SPARK or ALFA
- if Formal_Verification_Mode
- and then Is_Array_Type (Typ)
+ if Is_Array_Type (Typ)
and then not Is_Constrained (Typ)
then
- Error_Msg_F
- ("|~~returning an unconstrained array is not allowed",
+ Check_Formal_Restriction
+ ("returning an unconstrained array is not allowed",
Result_Definition (N));
end if;
Id := Body_Id;
end if;
- -- In formal mode, the last statement of a function should be a
- -- return statement.
-
- if Formal_Verification_Mode then
- declare
- Stat : constant Node_Id := Last_Source_Statement (HSS);
- begin
- if Present (Stat)
- and then not Nkind_In (Stat,
- N_Simple_Return_Statement,
- N_Extended_Return_Statement)
- then
- Error_Msg_F ("|~~last statement in function should "
- & "be RETURN", Stat);
- end if;
- end;
-
- elsif Return_Present (Id) then
+ if Return_Present (Id) then
Check_Returns (HSS, 'F', Missing_Ret);
if Missing_Ret then
Error_Msg_N ("missing RETURN statement in function body", N);
end if;
- -- In formal mode, verify that a procedure has no return
+ -- If procedure with No_Return, check returns
- elsif Formal_Verification_Mode
- and then Nkind (Body_Spec) = N_Procedure_Specification
+ elsif Nkind (Body_Spec) = N_Procedure_Specification
+ and then Present (Spec_Id)
+ and then No_Return (Spec_Id)
then
+ Check_Returns (HSS, 'P', Missing_Ret, Spec_Id);
+ end if;
+
+ -- Special checks in formal mode
+
+ if Nkind (Body_Spec) = N_Function_Specification then
+ -- In formal mode, the last statement of a function should be a
+ -- return statement.
+
+ declare
+ Stat : constant Node_Id := Last_Source_Statement (HSS);
+ begin
+ if Present (Stat)
+ and then not Nkind_In (Stat,
+ N_Simple_Return_Statement,
+ N_Extended_Return_Statement)
+ then
+ Check_Formal_Restriction
+ ("last statement in function should be RETURN", Stat);
+ end if;
+ end;
+
+ -- In formal mode, verify that a procedure has no return
+
+ elsif Nkind (Body_Spec) = N_Procedure_Specification then
if Present (Spec_Id) then
Id := Spec_Id;
else
-- borrow the Check_Returns procedure here ???
if Return_Present (Id) then
- Error_Msg_F ("|~~procedure should not have RETURN", N);
+ Check_Formal_Restriction
+ ("procedure should not have RETURN", N);
end if;
-
- -- If procedure with No_Return, check returns
-
- elsif Nkind (Body_Spec) = N_Procedure_Specification
- and then Present (Spec_Id)
- and then No_Return (Spec_Id)
- then
- Check_Returns (HSS, 'P', Missing_Ret, Spec_Id);
end if;
end Check_Missing_Return;
begin
-- Null procedures are not allowed in SPARK or ALFA
- if Formal_Verification_Mode
- and then Nkind (Specification (N)) = N_Procedure_Specification
+ if Nkind (Specification (N)) = N_Procedure_Specification
and then Null_Present (Specification (N))
then
- Error_Msg_F ("|~~null procedure not allowed", N);
+ Check_Formal_Restriction ("null procedure is not allowed", N);
end if;
-- For a null procedure, capture the profile before analysis, for
begin
-- 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
- Error_Msg_F ("|~~user-defined operator is not allowed", N);
+ if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol then
+ Check_Formal_Restriction ("user-defined operator is not allowed", N);
end if;
-- Proceed with analysis
-- 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));
- Error_Msg_F ("|~~overloading not allowed with entity#", S);
- end if;
+ Error_Msg_Sloc := Sloc (Homonym (S));
+ Check_Formal_Restriction ("overloading not allowed with entity#", S);
-- If S is a derived operation for an untagged type then by
-- definition it's not a dispatching operation (even if the parent
Default := Expression (Param_Spec);
if Present (Default) then
- -- Default expression is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~default expression is not allowed", Default);
- end if;
- -- Proceed with analysis
+ Check_Formal_Restriction
+ ("default expression is not allowed", Default);
if Out_Present (Param_Spec) then
Error_Msg_N
Nam : constant Node_Id := Name (N);
begin
- -- Exception renaming is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~exception renaming is not allowed", N);
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("exception renaming is not allowed", N);
Enter_Name (Id);
Analyze (Nam);
Inst : Boolean := False; -- prevent junk warning
begin
- -- Generic renaming is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~generic renaming is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
if Name (N) = Error then
return;
end if;
+ Check_Formal_Restriction ("generic renaming is not allowed", N);
+
Generate_Definition (New_P);
if Current_Scope /= Standard_Standard then
-- Start of processing for Analyze_Object_Renaming
begin
- -- Object renaming is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~object renaming is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
if Nam = Error then
return;
end if;
+ Check_Formal_Restriction ("object renaming is not allowed", N);
+
Set_Is_Pure (Id, Is_Pure (Current_Scope));
Enter_Name (Id);
-- Start of processing for Analyze_Use_Package
begin
- -- Use package is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~use clause is not allowed", N);
- return;
- end if;
-
- -- Proceed with analysis
+ Check_Formal_Restriction ("use clause is not allowed", N);
Set_Hidden_By_Use_Clause (N, No_Elist);
T_Name : Node_Id;
begin
- -- Abort statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~abort statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_Formal_Restriction ("abort statement is not allowed", N);
+
T_Name := First (Names (N));
while Present (T_Name) loop
Analyze (T_Name);
Task_Nam : Entity_Id;
begin
- -- Accept statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~accept statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_Formal_Restriction ("accept statement is not allowed", N);
-- Entry name is initialized to Any_Id. It should get reset to the
-- matching entry entity. An error is signalled if it is not reset.
Trigger : Node_Id;
begin
- -- Select statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~select statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_Formal_Restriction ("select statement is not allowed", N);
Check_Restriction (Max_Asynchronous_Select_Nesting, N);
Check_Restriction (No_Select_Statements, N);
Is_Disp_Select : Boolean := False;
begin
- -- Select statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~select statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
- Check_Restriction (No_Select_Statements, N);
Tasking_Used := True;
+ Check_Formal_Restriction ("select statement is not allowed", N);
+ Check_Restriction (No_Select_Statements, N);
-- Ada 2005 (AI-345): The trigger may be a dispatching call
procedure Analyze_Delay_Relative (N : Node_Id) is
E : constant Node_Id := Expression (N);
begin
- -- Delay statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~delay statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
- Check_Restriction (No_Relative_Delay, N);
Tasking_Used := True;
+ Check_Formal_Restriction ("delay statement is not allowed", N);
+ Check_Restriction (No_Relative_Delay, N);
Check_Restriction (No_Delay, N);
Check_Potentially_Blocking_Operation (N);
Analyze_And_Resolve (E, Standard_Duration);
Typ : Entity_Id;
begin
- -- Delay statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~delay statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_Formal_Restriction ("delay statement is not allowed", N);
Check_Restriction (No_Delay, N);
Check_Potentially_Blocking_Operation (N);
Analyze (E);
Call : constant Node_Id := Entry_Call_Statement (N);
begin
- -- Entry call is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~entry call is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_Formal_Restriction ("entry call is not allowed", N);
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
-- Start of processing for Analyze_Protected_Definition
begin
- -- Protected definition is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~protected definition is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_Formal_Restriction ("protected definition is not allowed", N);
Analyze_Declarations (Visible_Declarations (N));
if Present (Private_Declarations (N))
Outer_Ent : Entity_Id;
begin
- -- Requeue statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~requeue statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
+ Tasking_Used := True;
+ Check_Formal_Restriction ("requeue statement is not allowed", N);
Check_Restriction (No_Requeue_Statements, N);
Check_Unreachable_Code (N);
- Tasking_Used := True;
Enclosing := Empty;
for J in reverse 0 .. Scope_Stack.Last loop
Alt_Count : Uint := Uint_0;
begin
- -- Select statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~select statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
- Check_Restriction (No_Select_Statements, N);
Tasking_Used := True;
+ Check_Formal_Restriction ("select statement is not allowed", N);
+ Check_Restriction (No_Select_Statements, N);
-- Loop to analyze alternatives
L : Entity_Id;
begin
- -- Task definition is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~task definition is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_Formal_Restriction ("task definition is not allowed", N);
if Present (Visible_Declarations (N)) then
Analyze_Declarations (Visible_Declarations (N));
Is_Disp_Select : Boolean := False;
begin
- -- Select statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~select statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
- Check_Restriction (No_Select_Statements, N);
Tasking_Used := True;
+ Check_Formal_Restriction ("select statement is not allowed", N);
+ Check_Restriction (No_Select_Statements, N);
-- Ada 2005 (AI-345): The trigger may be a dispatching call
-- In SPARK or ALFA, the only view conversions are those involving
-- ancestor conversion of an extended type.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (A))
- and then Nkind (A) = N_Type_Conversion
+ if Nkind (A) = N_Type_Conversion
and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
then
declare
and then not Is_Class_Wide_Type (Operand_Typ)
and then Is_Ancestor (Target_Typ, Operand_Typ))
then
- Error_Msg_F ("|~~ancestor conversion is the only "
- & "permitted view conversion", A);
+ Check_Formal_Restriction
+ ("ancestor conversion is the only permitted view "
+ & "conversion", A);
end if;
end;
end if;
-- fixed point types shall be qualified or explicitly converted to
-- identify the result type.
- if Formal_Verification_Mode
- and then (Is_Fixed_Point_Type (Etype (L))
- or else Is_Fixed_Point_Type (Etype (R)))
+ if (Is_Fixed_Point_Type (Etype (L))
+ or else Is_Fixed_Point_Type (Etype (R)))
and then Nkind_In (N, N_Op_Multiply, N_Op_Divide)
and then
not Nkind_In (Parent (N), N_Qualified_Expression, N_Type_Conversion)
then
- Error_Msg_F
- ("|~~operation should be qualified or explicitly converted", N);
+ Check_Formal_Restriction
+ ("operation should be qualified or explicitly converted", N);
end if;
-- Set overflow and division checking bit. Much cleverer code needed
-- In SPARK or ALFA, ordering operators <, <=, >, >= are not defined
-- for Boolean types or array types except String.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
+ if Is_Boolean_Type (T) then
+ Check_Formal_Restriction
+ ("comparison is not defined on Boolean type", N);
+ elsif Is_Array_Type (T)
+ and then Base_Type (T) /= Standard_String
then
- if Is_Boolean_Type (T) then
- Error_Msg_F ("|~~comparison is not defined on Boolean type", N);
- elsif Is_Array_Type (T)
- and then Base_Type (T) /= Standard_String
- then
- Error_Msg_F
- ("|~~comparison is not defined on array types " &
- "other than String", N);
- end if;
+ Check_Formal_Restriction
+ ("comparison is not defined on array types other than String", N);
+ else
+ null;
end if;
-- Check comparison on unordered enumeration
-- other than String are only defined when, for each index position,
-- the operands have equal static bounds.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- and then Is_Array_Type (T)
+ if Is_Array_Type (T)
and then Base_Type (T) /= Standard_String
and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
then
- Error_Msg_F
- ("|~~array types should have matching static bounds", N);
+ Check_Formal_Restriction
+ ("array types should have matching static bounds", N);
end if;
-- If the unique type is a class-wide type then it will be expanded
-- 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 (B_Typ)
+ if Is_Array_Type (B_Typ)
and then not Matching_Static_Array_Bounds (Etype (Left_Opnd (N)),
Etype (Right_Opnd (N)))
then
- Error_Msg_F ("|~~array types should have matching static bounds", N);
+ Check_Formal_Restriction
+ ("array types should have matching static bounds", N);
end if;
end Resolve_Logical_Op;
NN := Parent (NN);
end loop;
- if Formal_Verification_Mode
- and then Base_Type (Etype (N)) /= Standard_String
- then
- Error_Msg_F ("|~~result of concatenation should have type String", N);
+ if Base_Type (Etype (N)) /= Standard_String then
+ Check_Formal_Restriction
+ ("result of concatenation should have type String", N);
end if;
end Resolve_Op_Concat;
-- Resolve_Op_Concat_Arg call it separately on each final operand, past
-- concatenation operations.
- if Formal_Verification_Mode then
- if Is_Character_Type (Etype (Arg)) then
- if not Is_Static_Expression (Arg) then
- Error_Msg_F ("|~~character operand for concatenation should be "
- & "static", N);
- end if;
+ if Is_Character_Type (Etype (Arg)) then
+ if not Is_Static_Expression (Arg) then
+ Check_Formal_Restriction
+ ("character operand for concatenation should be static", N);
+ end if;
- elsif Is_String_Type (Etype (Arg)) then
- if Nkind (Arg) /= N_String_Literal then
- Error_Msg_F ("|~~string operand for concatenation should be "
- & "a literal", N);
- end if;
+ elsif Is_String_Type (Etype (Arg)) then
+ if Nkind (Arg) /= N_String_Literal then
+ Check_Formal_Restriction
+ ("string operand for concatenation should be a literal", N);
+ end if;
-- Do not issue error on an operand that is neither a character nor
-- a string, as the error is issued in Resolve_Op_Concat.
- else
- null;
- end if;
+ else
+ null;
end if;
Check_Unset_Reference (Arg);
begin
Resolve (Expr, Target_Typ);
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- and then Is_Array_Type (Target_Typ)
+ if Is_Array_Type (Target_Typ)
and then Is_Array_Type (Etype (Expr))
and then not Matching_Static_Array_Bounds (Target_Typ, Etype (Expr))
then
- Error_Msg_F ("|~~array types should have matching static bounds", N);
+ Check_Formal_Restriction
+ ("array types should have matching static bounds", N);
end if;
-- A qualified expression requires an exact match of the type,
-- In SPARK or ALFA, a type conversion between array types should be
-- restricted to types which have matching static bounds.
- if Formal_Verification_Mode
- and then Comes_From_Source (Original_Node (N))
- and then Is_Array_Type (Target_Typ)
+ if Is_Array_Type (Target_Typ)
and then Is_Array_Type (Operand_Typ)
and then not Matching_Static_Array_Bounds (Target_Typ, Operand_Typ)
then
- Error_Msg_F ("|~~array types should have matching static bounds", N);
+ Check_Formal_Restriction
+ ("array types should have matching static bounds", N);
end if;
-- Note: we do the Eval_Type_Conversion call before applying the
-- Declaring a homonym is not allowed in SPARK or ALFA ...
- if Formal_Verification_Mode and then Present (C)
+ if Present (C)
-- ... unless the new declaration is in a subprogram, and the visible
-- declaration is a variable declaration or a parameter specification
and then Comes_From_Source (C)
then
Error_Msg_Sloc := Sloc (C);
- Error_Msg_F ("|~~redeclaration of identifier &#", Def_Id);
+ Check_Formal_Restriction ("redeclaration of identifier &#", Def_Id);
end if;
-- Warn if new entity hides an old one
L_Index := First_Index (L_Typ);
R_Index := First_Index (R_Typ);
+ -- There may not be an index available even if the type is constrained,
+ -- see for example 0100-C23 when this function is called from
+ -- Resolve_Qualified_Expression. Temporarily return False in that case.
+
+ if No (L_Index) or else No (R_Index) then
+ return False;
+ end if;
+
for Indx in 1 .. L_Ndims loop
Get_Index_Bounds (L_Index, L_Low, L_High);
Get_Index_Bounds (R_Index, R_Low, R_High);
projects / gcc.git / commitdiff