diff options
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 20 | ||||
| -rw-r--r-- | gcc/ada/errout.adb | 13 | ||||
| -rw-r--r-- | gcc/ada/errout.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/exp_ch6.adb | 14 | ||||
| -rw-r--r-- | gcc/ada/sem_aggr.adb | 98 | ||||
| -rw-r--r-- | gcc/ada/sem_attr.adb | 1 | ||||
| -rw-r--r-- | gcc/ada/sem_ch11.adb | 19 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 202 | ||||
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 48 | ||||
| -rw-r--r-- | gcc/ada/sem_ch5.adb | 81 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 126 | ||||
| -rw-r--r-- | gcc/ada/sem_ch8.adb | 37 | ||||
| -rw-r--r-- | gcc/ada/sem_ch9.adb | 119 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 100 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 12 |
15 files changed, 328 insertions, 569 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8003041ea09..19849b307e3 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,23 @@ +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 diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index 59babb14581..dcc1159cffe 100644 --- a/gcc/ada/errout.adb +++ b/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 -- ------------------------ diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads index 57b8efe0abb..933f58dad5e 100644 --- a/gcc/ada/errout.ads +++ b/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. diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 33e8bd157ec..b922297a531 100644 --- a/gcc/ada/exp_ch6.adb +++ b/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; diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 3800008954a..1b934946256 100644 --- a/gcc/ada/sem_aggr.adb +++ b/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; diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index f2556a7f2a4..aadcb04be52 100644 --- a/gcc/ada/sem_attr.adb +++ b/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) diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index 35d55599d7c..26ac6d0c209 100644 --- a/gcc/ada/sem_ch11.adb +++ b/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); diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 2d2a545ae4c..e468e1d7c40 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -715,15 +715,7 @@ package body Sem_Ch3 is 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))) @@ -1037,13 +1029,7 @@ package body Sem_Ch3 is -- 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 @@ -1297,13 +1283,7 @@ package body Sem_Ch3 is 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 @@ -2058,12 +2038,11 @@ package body Sem_Ch3 is -- 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 @@ -2281,10 +2260,16 @@ package body Sem_Ch3 is 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 @@ -2386,19 +2371,10 @@ package body Sem_Ch3 is 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 @@ -2507,15 +2483,7 @@ package body Sem_Ch3 is 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)); @@ -3054,33 +3022,30 @@ package body Sem_Ch3 is -- 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 @@ -4029,12 +3994,11 @@ package body Sem_Ch3 is -- 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 @@ -4047,17 +4011,13 @@ package body Sem_Ch3 is -- 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); @@ -11254,15 +11214,7 @@ package body Sem_Ch3 is 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); @@ -11491,16 +11443,7 @@ package body Sem_Ch3 is 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 @@ -11721,16 +11664,8 @@ package body Sem_Ch3 is -- 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 @@ -12387,17 +12322,8 @@ package body Sem_Ch3 is 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 @@ -14143,17 +14069,21 @@ package body Sem_Ch3 is 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 @@ -14349,10 +14279,8 @@ package body Sem_Ch3 is -- 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; diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 8b737ab1f9f..4d179d0ebe5 100644 --- a/gcc/ada/sem_ch4.adb +++ b/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); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index a6d4e4ab6f6..7d960c82b3a 100644 --- a/gcc/ada/sem_ch5.adb +++ b/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 diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 8d0edcc2128..260edc2faa2 100644 --- a/gcc/ada/sem_ch6.adb +++ b/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 diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index a883c4d19f6..de3b9ff3ec7 100644 --- a/gcc/ada/sem_ch8.adb +++ b/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); diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 280c0e91fcb..09214b87ad3 100644 --- a/gcc/ada/sem_ch9.adb +++ b/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 diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index d40ad9b2b6e..cc88f4315dc 100644 --- a/gcc/ada/sem_res.adb +++ b/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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 78348d4d151..e69b0946edc 100644 --- a/gcc/ada/sem_util.adb +++ b/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); |
