diff options
Diffstat (limited to 'gcc/ada/sem_ch3.adb')
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 148 |
1 files changed, 147 insertions, 1 deletions
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 52ff613..04919c0 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -716,6 +716,16 @@ 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 + if Is_Entry (Current_Scope) and then Is_Task_Type (Etype (Scope (Current_Scope))) then @@ -1028,6 +1038,14 @@ 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; + -- Associate the Itype node with the inner full-type declaration or -- subprogram spec or entry body. This is required to handle nested -- anonymous declarations. For example: @@ -1280,6 +1298,14 @@ 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 for permissible use of incomplete type if Nkind (S) /= N_Subtype_Indication then @@ -2477,6 +2503,16 @@ 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 + Generate_Definition (Defining_Identifier (N)); -- Process an incomplete declaration. The identifier must not have been @@ -2805,7 +2841,7 @@ package body Sem_Ch3 is -- There are three kinds of implicit types generated by an -- object declaration: - -- 1. Those for generated by the original Object Definition + -- 1. Those generated by the original Object Definition -- 2. Those generated by the Expression @@ -3010,6 +3046,39 @@ package body Sem_Ch3 is Act_T := T; + -- These checks should be performed before the initialization expression + -- 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.) + + 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; + + -- 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; + end if; + -- Process initialization expression if present and not in error if Present (E) and then E /= Error then @@ -3949,6 +4018,17 @@ package body Sem_Ch3 is Set_Has_Delayed_Freeze (Id); end if; + -- 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) + and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication + then + Error_Msg_F ("|~~subtype of Boolean cannot have constraint", N); + end if; + -- In the case where there is no constraint given in the subtype -- indication, Process_Subtype just returns the Subtype_Mark, so its -- semantic attributes must be established here. @@ -3956,6 +4036,20 @@ package body Sem_Ch3 is if Nkind (Subtype_Indication (N)) /= N_Subtype_Indication then Set_Etype (Id, Base_Type (T)); + -- 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) + and then not Is_Constrained (T) + then + Error_Msg_F + ("|~~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); @@ -11149,6 +11243,17 @@ 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 + Digits_Expr := Digits_Expression (C); Analyze_And_Resolve (Digits_Expr, Any_Integer); @@ -11375,6 +11480,17 @@ package body Sem_Ch3 is -- Digits constraint present 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_Restriction (No_Obsolescent_Features, C); if Warn_On_Obsolescent_Feature then @@ -11595,6 +11711,16 @@ 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_Restriction (No_Obsolescent_Features, C); if Warn_On_Obsolescent_Feature then @@ -12251,6 +12377,17 @@ 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_Restriction (No_Fixed_Point, Def); -- Create implicit base type @@ -14198,6 +14335,15 @@ package body Sem_Ch3 is end if; end if; end if; + + -- 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); + end if; end Derived_Type_Declaration; ------------------------ |