From 7ff2d2343921f5baeba0b47983202a84852e2957 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 2 Aug 2011 10:16:45 +0200 Subject: [multiple changes] 2011-08-02 Yannick Moy * exp_ch6.adb (Expand_N_Subprogram_Declaration): issue error in formal mode on subprogram declaration outside of package specification, unless it is followed by a pragma Import * sem_ch3.adb (Access_Definition, Access_Subprogram_Declaration, Access_Type_Declaration): issue error in formal mode on access type (Analyze_Incomplete_Type_Decl): issue error in formal mode on incomplete type (Analyze_Object_Declaration): issue error in formal mode on object declaration which does not respect SPARK restrictions (Analyze_Subtype_Declaration): issue error in formal mode on subtype declaration which does not respect SPARK restrictions (Constrain_Decimal, Constrain_Float, Constrain_Ordinary_Fixed): issue error in formal mode on digits or delta constraint (Decimal_Fixed_Point_Type_Declaration): issue error in formal mode on decimal fixed point type (Derived_Type_Declaration): issue error in formal mode on derived type other than type extensions of tagged record types * sem_ch6.adb (Process_Formals): remove check in formal mode, redundant with check on access definition * sem_ch9.adb (Analyze_Protected_Definition): issue error in formal mode on protected definition. (Analyze_Task_Definition): issue error in formal mode on task definition 2011-08-02 Robert Dewar * make.adb, sem_ch8.adb, s-inmaop-vxworks.adb: Minor reformatting. From-SVN: r177093 --- gcc/ada/ChangeLog | 29 +++++++++ gcc/ada/exp_ch6.adb | 22 +++++++ gcc/ada/make.adb | 4 +- gcc/ada/s-inmaop-vxworks.adb | 2 +- gcc/ada/sem_ch3.adb | 148 ++++++++++++++++++++++++++++++++++++++++++- gcc/ada/sem_ch6.adb | 8 --- gcc/ada/sem_ch8.adb | 76 ++++++++++++---------- gcc/ada/sem_ch9.adb | 16 +++++ 8 files changed, 258 insertions(+), 47 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 5155a79..65fb0dc 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,32 @@ +2011-08-02 Yannick Moy + + * exp_ch6.adb (Expand_N_Subprogram_Declaration): issue error in formal + mode on subprogram declaration outside of package specification, unless + it is followed by a pragma Import + * sem_ch3.adb (Access_Definition, Access_Subprogram_Declaration, + Access_Type_Declaration): issue error in formal mode on access type + (Analyze_Incomplete_Type_Decl): issue error in formal mode on + incomplete type + (Analyze_Object_Declaration): issue error in formal mode on object + declaration which does not respect SPARK restrictions + (Analyze_Subtype_Declaration): issue error in formal mode on subtype + declaration which does not respect SPARK restrictions + (Constrain_Decimal, Constrain_Float, Constrain_Ordinary_Fixed): issue + error in formal mode on digits or delta constraint + (Decimal_Fixed_Point_Type_Declaration): issue error in formal mode on + decimal fixed point type + (Derived_Type_Declaration): issue error in formal mode on derived type + other than type extensions of tagged record types + * sem_ch6.adb (Process_Formals): remove check in formal mode, redundant + with check on access definition + * sem_ch9.adb (Analyze_Protected_Definition): issue error in formal + mode on protected definition. + (Analyze_Task_Definition): issue error in formal mode on task definition + +2011-08-02 Robert Dewar + + * make.adb, sem_ch8.adb, s-inmaop-vxworks.adb: Minor reformatting. + 2011-08-02 Javier Miranda * sem_ch6.adb (Can_Override_Operator): New function. diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 3f861f2..33e8bd1 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -5406,6 +5406,28 @@ package body Exp_Ch6 is Prot_Id : Entity_Id; begin + -- 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)) + and then Nkind (Next (N)) = N_Pragma + and then Get_Pragma_Id (Pragma_Name (Next (N))) = Pragma_Import + then + -- In SPARK or ALFA, subprogram declarations are also permitted in + -- declarative parts when immediately followed by a corresponding + -- pragma Import. We only check here that there is some pragma + -- Import. + + null; + else + Error_Msg_F ("|~~subprogram declaration is not allowed here", N); + end if; + end if; + -- Deal with case of protected subprogram. Do not generate protected -- operation if operation is flagged as eliminated. diff --git a/gcc/ada/make.adb b/gcc/ada/make.adb index 6051c79..4aac5b86 100644 --- a/gcc/ada/make.adb +++ b/gcc/ada/make.adb @@ -6066,8 +6066,8 @@ package body Make is end loop; for Index in 1 .. Library_Projs.Last loop - if - Library_Projs.Table (Index).Library_Kind = Static + if Library_Projs.Table + (Index).Library_Kind = Static then Linker_Switches.Increment_Last; Linker_Switches.Table (Linker_Switches.Last) := diff --git a/gcc/ada/s-inmaop-vxworks.adb b/gcc/ada/s-inmaop-vxworks.adb index fe3b741..5b60283 100755 --- a/gcc/ada/s-inmaop-vxworks.adb +++ b/gcc/ada/s-inmaop-vxworks.adb @@ -2,7 +2,7 @@ -- -- -- GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS -- -- -- --- SYSTEM.INTERRUPT_MANAGEMENT.OPERATIONS -- +-- SYSTEM.INTERRUPT_MANAGEMENT.OPERATIONS -- -- -- -- B o d y -- -- -- 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; ------------------------ diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 3dc7ee8..61ce6f6 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -8785,14 +8785,6 @@ package body Sem_Ch6 is Set_Etype (Formal, Formal_Type); Default := Expression (Param_Spec); - -- Access parameter is not allowed in SPARK or ALFA - - if Formal_Verification_Mode - and then Ekind (Formal_Type) = E_Anonymous_Access_Type - then - Error_Msg_F ("|~~access parameter is not allowed", Param_Spec); - end if; - if Present (Default) then -- Default expression is not allowed in SPARK or ALFA diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 32d4002..2472474 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -506,9 +506,12 @@ package body Sem_Ch8 is -- re-installing use clauses of parent units. N is the use_clause that -- names P (and possibly other packages). - procedure Use_One_Type (Id : Node_Id); + procedure Use_One_Type (Id : Node_Id; Installed : Boolean := False); -- Id is the subtype mark from a use type clause. This procedure makes - -- the primitive operators of the type potentially use-visible. + -- the primitive operators of the type potentially use-visible. The + -- boolean flag Installed indicates that the clause is being reinstalled + -- after previous analysis, and primitive operations are already chained + -- on the Used_Operations list of the clause. procedure Write_Info; -- Write debugging information on entities declared in current scope @@ -2693,11 +2696,8 @@ package body Sem_Ch8 is begin Mark := First (Subtype_Marks (N)); while Present (Mark) loop - if not In_Use (Entity (Mark)) - and then not Is_Potentially_Use_Visible (Entity (Mark)) - then - Set_In_Use (Base_Type (Entity (Mark))); - end if; + Use_One_Type (Mark, Installed => True); + Next (Mark); end loop; @@ -7565,7 +7565,7 @@ package body Sem_Ch8 is -- Use_One_Type -- ------------------ - procedure Use_One_Type (Id : Node_Id) is + procedure Use_One_Type (Id : Node_Id; Installed : Boolean := False) is Elmt : Elmt_Id; Is_Known_Used : Boolean; Op_List : Elist_Id; @@ -7719,40 +7719,46 @@ package body Sem_Ch8 is end if; Set_Current_Use_Clause (T, Parent (Id)); - Op_List := Collect_Primitive_Operations (T); -- Iterate over primitive operations of the type. If an operation is -- already use_visible, it is the result of a previous use_clause, - -- and already appears on the corresponding entity chain. + -- and already appears on the corresponding entity chain. If the + -- clause is being reinstalled, operations are already use-visible. - Elmt := First_Elmt (Op_List); - while Present (Elmt) loop - if (Nkind (Node (Elmt)) = N_Defining_Operator_Symbol - or else Chars (Node (Elmt)) in Any_Operator_Name) - and then not Is_Hidden (Node (Elmt)) - and then not Is_Potentially_Use_Visible (Node (Elmt)) - then - Set_Is_Potentially_Use_Visible (Node (Elmt)); - Append_Elmt (Node (Elmt), Used_Operations (Parent (Id))); + if Installed then + null; - elsif Ada_Version >= Ada_2012 - and then All_Present (Parent (Id)) - and then not Is_Hidden (Node (Elmt)) - and then not Is_Potentially_Use_Visible (Node (Elmt)) - then - Set_Is_Potentially_Use_Visible (Node (Elmt)); - Append_Elmt (Node (Elmt), Used_Operations (Parent (Id))); - end if; + else + Op_List := Collect_Primitive_Operations (T); + Elmt := First_Elmt (Op_List); + while Present (Elmt) loop + if (Nkind (Node (Elmt)) = N_Defining_Operator_Symbol + or else Chars (Node (Elmt)) in Any_Operator_Name) + and then not Is_Hidden (Node (Elmt)) + and then not Is_Potentially_Use_Visible (Node (Elmt)) + then + Set_Is_Potentially_Use_Visible (Node (Elmt)); + Append_Elmt (Node (Elmt), Used_Operations (Parent (Id))); - Next_Elmt (Elmt); - end loop; - end if; + elsif Ada_Version >= Ada_2012 + and then All_Present (Parent (Id)) + and then not Is_Hidden (Node (Elmt)) + and then not Is_Potentially_Use_Visible (Node (Elmt)) + then + Set_Is_Potentially_Use_Visible (Node (Elmt)); + Append_Elmt (Node (Elmt), Used_Operations (Parent (Id))); + end if; - if Ada_Version >= Ada_2012 - and then All_Present (Parent (Id)) - and then Is_Tagged_Type (T) - then - Use_Class_Wide_Operations (T); + Next_Elmt (Elmt); + end loop; + end if; + + if Ada_Version >= Ada_2012 + and then All_Present (Parent (Id)) + and then Is_Tagged_Type (T) + then + Use_Class_Wide_Operations (T); + end if; end if; -- If warning on redundant constructs, check for unnecessary WITH diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 0fb1ae6..9d1a84d 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -1158,6 +1158,14 @@ 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; Analyze_Declarations (Visible_Declarations (N)); @@ -2009,6 +2017,14 @@ 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; if Present (Visible_Declarations (N)) then -- cgit v1.1