Skip to content

R
riscv-gcc-1
Commit fe5d3068 by Yannick Moy Committed by Arnaud Charlet
Options

errout.adb, errout.ads (Check_Formal_Restriction): new procedure which issues an… 

errout.adb, errout.ads (Check_Formal_Restriction): new procedure which issues an error in formal mode if...

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.

From-SVN: r177099
parent b60a3f26
Showing with 263 additions and 432 deletions
gcc/ada/ChangeLog
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
......
gcc/ada/errout.adb
......@@ -224,6 +224,19 @@ package body Errout is
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 --
------------------------
......
gcc/ada/errout.ads
......@@ -740,6 +740,13 @@ package Errout is
-- 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.
......
gcc/ada/exp_ch6.adb
......@@ -5409,11 +5409,12 @@ package body Exp_Ch6 is
-- 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
......@@ -5424,7 +5425,8 @@ package body Exp_Ch6 is
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;
......
gcc/ada/sem_aggr.adb
......@@ -1097,42 +1097,39 @@ package body Sem_Aggr is
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;
......@@ -1785,11 +1782,9 @@ package body Sem_Aggr is
-- 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;
......@@ -2434,12 +2429,11 @@ package body Sem_Aggr is
-- 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
......@@ -3114,37 +3108,35 @@ package body Sem_Aggr is
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;
......
gcc/ada/sem_attr.adb
......@@ -2067,6 +2067,7 @@ package body Sem_Attr is
-- 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)
......
gcc/ada/sem_ch11.adb
......@@ -443,14 +443,7 @@ package body Sem_Ch11 is
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
......@@ -617,15 +610,7 @@ package body Sem_Ch11 is
-- 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);
......
gcc/ada/sem_ch4.adb
......@@ -369,13 +369,7 @@ package body Sem_Ch4 is
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
......@@ -1475,13 +1469,7 @@ package body Sem_Ch4 is
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);
......@@ -1681,13 +1669,7 @@ package body Sem_Ch4 is
-- 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);
......@@ -2569,13 +2551,7 @@ package body Sem_Ch4 is
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;
......@@ -3261,13 +3237,7 @@ package body Sem_Ch4 is
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);
......@@ -4295,13 +4265,7 @@ package body Sem_Ch4 is
-- 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);
......
gcc/ada/sem_ch5.adb
......@@ -806,13 +806,7 @@ package body Sem_Ch5 is
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
......@@ -1104,12 +1098,11 @@ package body Sem_Ch5 is
-- 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
......@@ -1183,16 +1176,14 @@ package body Sem_Ch5 is
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;
......@@ -1229,36 +1220,36 @@ package body Sem_Ch5 is
-- 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;
......@@ -1286,11 +1277,7 @@ package body Sem_Ch5 is
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
......@@ -1872,11 +1859,9 @@ package body Sem_Ch5 is
-- 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
......
gcc/ada/sem_ch6.adb
......@@ -227,13 +227,7 @@ package body Sem_Ch6 is
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);
......@@ -607,22 +601,17 @@ package body Sem_Ch6 is
-- 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:
......@@ -1404,12 +1393,8 @@ package body Sem_Ch6 is
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
......@@ -1441,12 +1426,11 @@ package body Sem_Ch6 is
-- 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;
......@@ -1851,24 +1835,7 @@ package body Sem_Ch6 is
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
......@@ -1882,11 +1849,37 @@ package body Sem_Ch6 is
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
......@@ -1897,16 +1890,9 @@ package body Sem_Ch6 is
-- 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;
......@@ -2844,11 +2830,10 @@ package body Sem_Ch6 is
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
......@@ -3092,11 +3077,8 @@ package body Sem_Ch6 is
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
......@@ -8525,12 +8507,8 @@ package body Sem_Ch6 is
-- 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
......@@ -8791,13 +8769,9 @@ package body Sem_Ch6 is
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
......
gcc/ada/sem_ch8.adb
......@@ -529,13 +529,7 @@ package body Sem_Ch8 is
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);
......@@ -628,18 +622,12 @@ package body Sem_Ch8 is
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
......@@ -726,18 +714,12 @@ package body Sem_Ch8 is
-- 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);
......@@ -2567,14 +2549,7 @@ package body Sem_Ch8 is
-- 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);
......
gcc/ada/sem_ch9.adb
......@@ -100,15 +100,9 @@ package body Sem_Ch9 is
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);
......@@ -177,15 +171,8 @@ package body Sem_Ch9 is
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.
......@@ -415,15 +402,8 @@ package body Sem_Ch9 is
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);
......@@ -468,16 +448,9 @@ package body Sem_Ch9 is
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
......@@ -572,16 +545,9 @@ package body Sem_Ch9 is
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);
......@@ -597,15 +563,8 @@ package body Sem_Ch9 is
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);
......@@ -891,15 +850,8 @@ package body Sem_Ch9 is
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));
......@@ -1161,15 +1113,8 @@ package body Sem_Ch9 is
-- 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))
......@@ -1362,17 +1307,10 @@ package body Sem_Ch9 is
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
......@@ -1643,16 +1581,9 @@ package body Sem_Ch9 is
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
......@@ -2028,15 +1959,8 @@ package body Sem_Ch9 is
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));
......@@ -2195,16 +2119,9 @@ package body Sem_Ch9 is
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
......
gcc/ada/sem_res.adb
......@@ -3560,9 +3560,7 @@ package body Sem_Res is
-- 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
......@@ -3577,8 +3575,9 @@ package body Sem_Res is
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;
......@@ -4827,15 +4826,14 @@ package body Sem_Res is
-- 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
......@@ -5842,18 +5840,16 @@ package body Sem_Res is
-- 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
......@@ -6703,14 +6699,12 @@ package body Sem_Res is
-- 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
......@@ -7239,13 +7233,12 @@ package body Sem_Res is
-- 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;
......@@ -7495,10 +7488,9 @@ package body Sem_Res is
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;
......@@ -7609,25 +7601,23 @@ package body Sem_Res is
-- 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);
......@@ -7898,13 +7888,12 @@ package body Sem_Res is
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,
......@@ -9024,13 +9013,12 @@ package body Sem_Res is
-- 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
......
gcc/ada/sem_util.adb
......@@ -3202,7 +3202,7 @@ package body Sem_Util is
-- 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
......@@ -3234,7 +3234,7 @@ package body Sem_Util is
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
......@@ -8030,6 +8030,14 @@ package body Sem_Util is
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);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment