From: Arnaud Charlet Date: Thu, 4 Aug 2011 08:50:25 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a4640a3936bb760801ca5d2d44152a3424a8facb;p=gcc.git [multiple changes] 2011-08-04 Eric Botcazou * bindgen.adb: Add comments. 2011-08-04 Yannick Moy * einfo.adb, einfo.ads: Free Flag254 and make Formal_Proof_On a synthesized flag. * sem_prag.adb (Analyze_Pragma): record the pragma Annotate (Formal_Proof, On/Off) in the Rep_Item list of the current subprogram. 2011-08-04 Robert Dewar * exp_ch7.adb, exp_ch6.adb, sem_ch3.adb, layout.adb, sem_ch5.adb, osint-c.ads, sem_util.ads, gnat1drv.adb, targparm.ads, sem_ch6.adb, sem_ch13.adb, s-pooloc.adb: Minor reformatting. From-SVN: r177334 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 5fe886421a3..179b12e61c4 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,20 @@ +2011-08-04 Eric Botcazou + + * bindgen.adb: Add comments. + +2011-08-04 Yannick Moy + + * einfo.adb, einfo.ads: Free Flag254 and make Formal_Proof_On a + synthesized flag. + * sem_prag.adb (Analyze_Pragma): record the pragma Annotate + (Formal_Proof, On/Off) in the Rep_Item list of the current subprogram. + +2011-08-04 Robert Dewar + + * exp_ch7.adb, exp_ch6.adb, sem_ch3.adb, layout.adb, sem_ch5.adb, + osint-c.ads, sem_util.ads, gnat1drv.adb, targparm.ads, sem_ch6.adb, + sem_ch13.adb, s-pooloc.adb: Minor reformatting. + 2011-08-04 Thomas Quinot * s-pooloc.ads, s-pooglo.ads: Minor reformatting diff --git a/gcc/ada/bindgen.adb b/gcc/ada/bindgen.adb index 353e91da584..a4e7ccae87e 100644 --- a/gcc/ada/bindgen.adb +++ b/gcc/ada/bindgen.adb @@ -3097,6 +3097,9 @@ package body Bindgen is WBI (""); end if; + -- The B.1 (39) implementation advice says that the adainit/adafinal + -- routines should be idempotent. Generate a flag to ensure that. + WBI (" Is_Elaborated : Boolean := False;"); WBI (""); @@ -3323,6 +3326,9 @@ package body Bindgen is WBI (""); end if; + -- The B.1 (39) implementation advice says that the adainit/adafinal + -- routines should be idempotent. Generate a flag to ensure that. + WBI ("static char is_elaborated = 0;"); WBI (""); diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index be0081684dc..84163c67c8d 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -522,7 +522,7 @@ package body Einfo is -- Body_Is_In_ALFA Flag251 -- Is_Processed_Transient Flag252 -- Is_Postcondition_Proc Flag253 - -- Formal_Proof_On Flag254 + -- (unused) Flag254 ----------------------- -- Local subprograms -- @@ -1126,12 +1126,6 @@ package body Einfo is return Node6 (Id); end First_Rep_Item; - function Formal_Proof_On (Id : E) return B is - begin - pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id)); - return Flag254 (Id); - end Formal_Proof_On; - function Freeze_Node (Id : E) return N is begin return Node7 (Id); @@ -3612,12 +3606,6 @@ package body Einfo is Set_Uint10 (Id, UI_From_Int (F'Pos (V))); end Set_Float_Rep; - procedure Set_Formal_Proof_On (Id : E; V : B := True) is - begin - pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id)); - Set_Flag254 (Id, V); - end Set_Formal_Proof_On; - procedure Set_Freeze_Node (Id : E; V : N) is begin Set_Node7 (Id, V); @@ -5911,6 +5899,41 @@ package body Einfo is end if; end First_Formal_With_Extras; + --------------------- + -- Formal_Proof_On -- + --------------------- + + function Formal_Proof_On (Id : E) return B is + N : Node_Id; + Arg1 : Node_Id; + Arg2 : Node_Id; + + begin + pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id)); + + N := First_Rep_Item (Id); + while Present (N) loop + if Nkind (N) = N_Pragma + and then Get_Pragma_Id (Pragma_Name (N)) = Pragma_Annotate + and then Present (Pragma_Argument_Associations (N)) + and then List_Length (Pragma_Argument_Associations (N)) = 2 + then + Arg1 := First (Pragma_Argument_Associations (N)); + Arg2 := Next (Arg1); + + if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof + and then Chars (Get_Pragma_Arg (Arg2)) = Name_On + then + return True; + end if; + end if; + + Next_Rep_Item (N); + end loop; + + return False; + end Formal_Proof_On; + ------------------------------------- -- Get_Attribute_Definition_Clause -- ------------------------------------- @@ -7442,7 +7465,6 @@ package body Einfo is W ("Entry_Accepted", Flag152 (Id)); W ("Can_Use_Internal_Rep", Flag229 (Id)); W ("Finalize_Storage_Only", Flag158 (Id)); - W ("Formal_Proof_On", Flag254 (Id)); W ("From_With_Type", Flag159 (Id)); W ("Has_Aliased_Components", Flag135 (Id)); W ("Has_Alignment_Clause", Flag46 (Id)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 84fd79d3657..49e22fb01f9 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -1272,10 +1272,10 @@ package Einfo is -- Float_Rep_Kind. Together with the Digits_Value uniquely defines -- the floating-point representation to be used. --- Formal_Proof_On (Flag254) --- Present in subprogram and generic subprogram entities. Set on for --- subprograms whose body contains an Annotate pragma which forces formal --- proof on this body. +-- Formal_Proof_On (synthesized) +-- Applies to subprogram and generic subprogram entities. Returns True if +-- the Rep_Item chain for the subprogram has a pragma Annotate which +-- forces formal proof on the subprogram's body. -- Freeze_Node (Node7) -- Present in all entities. If there is an associated freeze node for @@ -5250,7 +5250,6 @@ package Einfo is -- Delay_Cleanups (Flag114) -- Delay_Subprogram_Descriptors (Flag50) -- Discard_Names (Flag88) - -- Formal_Proof_On (Flag254) -- Has_Completion (Flag26) -- Has_Controlling_Result (Flag98) -- Has_Invariants (Flag232) @@ -5397,7 +5396,6 @@ package Einfo is -- Is_Primitive (Flag218) -- Is_Thunk (Flag225) -- Default_Expressions_Processed (Flag108) - -- Formal_Proof_On (Flag254) -- Aren't there more flags and fields? seems like this list should be -- more similar to the E_Function list, which is much longer ??? @@ -5518,7 +5516,6 @@ package Einfo is -- Delay_Cleanups (Flag114) -- Delay_Subprogram_Descriptors (Flag50) -- Discard_Names (Flag88) - -- Formal_Proof_On (Flag254) -- Has_Completion (Flag26) -- Has_Invariants (Flag232) -- Has_Master_Entity (Flag21) @@ -6076,7 +6073,6 @@ package Einfo is function First_Private_Entity (Id : E) return E; function First_Rep_Item (Id : E) return N; function Float_Rep (Id : E) return F; - function Formal_Proof_On (Id : E) return B; function Freeze_Node (Id : E) return N; function From_With_Type (Id : E) return B; function Full_View (Id : E) return E; @@ -6453,6 +6449,7 @@ package Einfo is function First_Component_Or_Discriminant (Id : E) return E; function First_Formal (Id : E) return E; function First_Formal_With_Extras (Id : E) return E; + function Formal_Proof_On (Id : E) return B; function Has_Attach_Handler (Id : E) return B; function Has_Entries (Id : E) return B; function Has_Foreign_Convention (Id : E) return B; @@ -6666,7 +6663,6 @@ package Einfo is procedure Set_First_Private_Entity (Id : E; V : E); procedure Set_First_Rep_Item (Id : E; V : N); procedure Set_Float_Rep (Id : E; V : F); - procedure Set_Formal_Proof_On (Id : E; V : B := True); procedure Set_Freeze_Node (Id : E; V : N); procedure Set_From_With_Type (Id : E; V : B := True); procedure Set_Full_View (Id : E; V : E); @@ -7364,7 +7360,6 @@ package Einfo is pragma Inline (First_Optional_Parameter); pragma Inline (First_Private_Entity); pragma Inline (First_Rep_Item); - pragma Inline (Formal_Proof_On); pragma Inline (Freeze_Node); pragma Inline (From_With_Type); pragma Inline (Full_View); @@ -7809,7 +7804,6 @@ package Einfo is pragma Inline (Set_First_Optional_Parameter); pragma Inline (Set_First_Private_Entity); pragma Inline (Set_First_Rep_Item); - pragma Inline (Set_Formal_Proof_On); pragma Inline (Set_Freeze_Node); pragma Inline (Set_From_With_Type); pragma Inline (Set_Full_View); diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 1d9544dd9f3..ca449fae78b 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -7188,7 +7188,7 @@ package body Exp_Ch6 is null; -- Do not generate the call to Make_Set_Finalize_Address_Ptr for - -- CodePeer compilations becase Finalize_Address is never built. + -- CodePeer compilations because Finalize_Address is never built. elsif not CodePeer_Mode then Insert_Action (Allocator, diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 21a1ffea63a..abe960b3a06 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -2817,6 +2817,10 @@ package body Exp_Ch7 is -- order to detect this scenario, save the state of entry into the -- finalization code. + -- No need to do this for VM case, since VM version of Ada.Exceptions + -- does not include routine Raise_From_Controlled_Operation which is the + -- the sole user of flag Abort. + if Abort_Allowed and then VM_Target = No_VM then @@ -2871,9 +2875,7 @@ package body Exp_Ch7 is Attribute_Name => Name_Identity))); end; - -- No abort or .NET/JVM. The VM version of Ada.Exceptions does not - -- include routine Raise_From_Controlled_Operation which is the sole - -- user of flag Abort. + -- No abort or .NET/JVM else A_Expr := New_Reference_To (Standard_False, Loc); @@ -7131,8 +7133,9 @@ package body Exp_Ch7 is Utyp := Underlying_Type (Root_Type (Base_Type (Typ))); Ref := Unchecked_Convert_To (Utyp, Ref); + -- The following is to prevent problems with UC see 1.156 RH ??? + Set_Assignment_OK (Ref); - -- To prevent problems with UC see 1.156 RH ??? end if; -- If the underlying_type is a subtype, then we are dealing with the diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index dcff866229b..eabf1123d4a 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -1048,15 +1048,17 @@ begin Write_ALI (Object => (Back_End_Mode = Generate_Object)); if not Compilation_Errors then + -- In case of ada backends, we need to make sure that the generated - -- object file has a timestamp greater than the ALI file. - -- We do this to make gnatmake happy when checking the ALI and obj - -- timestamps, where it expects the object file being written after - -- the ali file. + -- object file has a timestamp greater than the ALI file. We do this + -- to make gnatmake happy when checking the ALI and obj timestamps, + -- where it expects the object file being written after the ali file. + -- Gnatmake's assumption is true for gcc platforms where the gcc -- wrapper needs to call the assembler after calling gnat1, but is -- not true for ada backends, where the object files are created -- directly by gnat1 (so are created before the ali file). + Back_End.Gen_Or_Update_Object_File; end if; diff --git a/gcc/ada/layout.adb b/gcc/ada/layout.adb index 7ae89b53f27..09d3ce1ac8d 100644 --- a/gcc/ada/layout.adb +++ b/gcc/ada/layout.adb @@ -1280,8 +1280,8 @@ package body Layout is end; end if; - -- Now set the dynamic size (the Value_Size is always the same - -- as the Object_Size for arrays whose length is dynamic). + -- Now set the dynamic size (the Value_Size is always the same as the + -- Object_Size for arrays whose length is dynamic). -- ??? If Size.Status = Dynamic, Vtyp will not have been set. -- The added initialization sets it to Empty now, but is this @@ -1305,6 +1305,7 @@ package body Layout is Lo : Node_Id; Hi : Node_Id; Res : Boolean := False; + begin -- Loop to process array indexes @@ -1323,9 +1324,10 @@ package body Layout is Hi := Type_High_Bound (Ityp); if (Nkind (Lo) = N_Identifier - and then Ekind (Entity (Lo)) = E_Discriminant) - or else (Nkind (Hi) = N_Identifier - and then Ekind (Entity (Hi)) = E_Discriminant) + and then Ekind (Entity (Lo)) = E_Discriminant) + or else + (Nkind (Hi) = N_Identifier + and then Ekind (Entity (Hi)) = E_Discriminant) then Res := True; end if; diff --git a/gcc/ada/osint-c.ads b/gcc/ada/osint-c.ads index e8bc57a8ad1..2faef5ed787 100644 --- a/gcc/ada/osint-c.ads +++ b/gcc/ada/osint-c.ads @@ -117,10 +117,10 @@ package Osint.C is -- above for a discussion of how library information files are stored. procedure Set_Library_Info_Name; - -- Sets a default ALI file name from the main compiler source name. - -- This is used by Create_Output_Library_Info, and by the version of - -- Read_Library_Info that takes a default file name. The name is in - -- Name_Buffer (with length in Name_Len) on return from the call. + -- Sets a default ALI file name from the main compiler source name. Used by + -- Create_Output_Library_Info, and by the version of Read_Library_Info that + -- takes a default file name. The name is in Name_Buffer (with length in + -- Name_Len) on return from the call. procedure Create_Output_Library_Info; -- Creates the output library information file for the source file which diff --git a/gcc/ada/s-pooloc.adb b/gcc/ada/s-pooloc.adb index 2a161f49de3..ebada306114 100644 --- a/gcc/ada/s-pooloc.adb +++ b/gcc/ada/s-pooloc.adb @@ -112,6 +112,8 @@ package body System.Pool_Local is if Prev (Allocated).all = Null_Address then Pool.First := Next (Allocated).all; + -- Comment needed + if Pool.First /= Null_Address then Prev (Pool.First).all := Null_Address; end if; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 3bb1d524996..c9f78fae525 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -440,14 +440,14 @@ package body Sem_Ch13 is Error_Msg_Uint_1 := SSU; Error_Msg_F ("\and is not a multiple of Storage_Unit (^) " - & "('R'M 13.4.1(10))", + & "(RM 13.4.1(10))", First_Bit (CC)); else Error_Msg_Uint_1 := Fbit; Error_Msg_F ("\and first bit (^) is non-zero " - & "('R'M 13.4.1(10))", + & "(RM 13.4.1(10))", First_Bit (CC)); end if; end if; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 401436db2b8..4cf4c0b6b10 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -15302,7 +15302,7 @@ package body Sem_Ch3 is elsif No (Real_Range_Specification (Def)) then Error_Msg_Uint_1 := Max_Digs_Val; Error_Msg_N ("types with more than ^ digits need range spec " - & "('R'M 3.5.7(6))", Digs); + & "(RM 3.5.7(6))", Digs); end if; end; end if; diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index b9c03c02932..8936daa531f 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -2098,8 +2098,9 @@ package body Sem_Ch5 is -- elements of a container using the OF syntax. if Is_In_ALFA (Etype (Id)) - and then (No (Iterator_Specification (N)) - or else not Of_Present (Iterator_Specification (N))) + and then + (No (Iterator_Specification (N)) + or else not Of_Present (Iterator_Specification (N))) then Set_Is_In_ALFA (Id); end if; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 4eaaaa6ab9b..64a7eac5e6e 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -6273,7 +6273,7 @@ package body Sem_Ch6 is Obj_Decl, Typ); Error_Msg_N ("\an equality operator cannot be declared after this " - & "point ('R'M 4.5.2 (9.8)) (Ada 2012))?", Obj_Decl); + & "point (RM 4.5.2 (9.8)) (Ada 2012))?", Obj_Decl); exit; end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index e9923157b14..dac7df81461 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -6091,103 +6091,118 @@ package body Sem_Prag is -- external tool and a tool-specific function. These arguments are -- not analyzed. - when Pragma_Annotate => Annotate : begin + -- The following is a special form used in conjunction with the + -- ALFA subset of Ada: + + -- pragma Annotate (Formal_Proof, MODE); + -- MODE ::= On | Off + + -- This pragma either forces (mode On) or disables (mode Off) + -- formal verification of the subprogram in which it is added. When + -- formal verification is forced, all violations of the the ALFA + -- subset of Ada present in the subprogram are reported as errors + -- to the user. + + when Pragma_Annotate => Annotate : declare + Arg : Node_Id; + Exp : Node_Id; + + begin GNAT_Pragma; Check_At_Least_N_Arguments (1); Check_Arg_Is_Identifier (Arg1); Check_No_Identifiers; Store_Note (N); - declare - Arg : Node_Id; - Exp : Node_Id; + -- Special processing for Formal_Proof case - begin - if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then - if No (Arg2) then - Error_Pragma_Arg - ("missing second argument for pragma%", Arg1); - end if; + if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then + if No (Arg2) then + Error_Pragma_Arg + ("missing second argument for pragma%", Arg1); + end if; - Check_Arg_Is_Identifier (Arg2); - Check_Arg_Count (2); + Check_Arg_Count (2); + Check_Arg_Is_One_Of (Arg2, Name_On, Name_Off); - if Chars (Get_Pragma_Arg (Arg2)) /= Name_On - and then Chars (Get_Pragma_Arg (Arg2)) /= Name_Off + declare + Cur_Subp : constant Entity_Id := Current_Subprogram; + + begin + if Present (Cur_Subp) + and then (Is_Subprogram (Cur_Subp) + or else Is_Generic_Subprogram (Cur_Subp)) then - Error_Pragma_Arg - ("wrong second argument for pragma%", Arg2); - end if; + -- Notify user if some ALFA violation occurred before + -- this point in Cur_Subp. These violations are not + -- precisly located, but this is better than ignoring + -- these violations. + + if Chars (Get_Pragma_Arg (Arg2)) = Name_On + and then (not Is_In_ALFA (Cur_Subp) + or else not Body_Is_In_ALFA (Cur_Subp)) + then + Error_Pragma + ("pragma% is placed after violation" + & " of 'A'L'F'A"); + end if; - if Chars (Get_Pragma_Arg (Arg2)) = Name_On then - declare - Cur_Subp : constant Entity_Id := Current_Subprogram; + -- We treat this as a Rep_Item to record it on the rep + -- item chain for easy location later on. - begin - if Present (Cur_Subp) - and then (Is_Subprogram (Cur_Subp) - or else Is_Generic_Subprogram (Cur_Subp)) - then - -- Notify user if some ALFA violation occurred - -- before this point in Cur_Subp. These violations - -- are not precisly located, but this is better - -- than ignoring them. + Record_Rep_Item (Cur_Subp, N); - if not Is_In_ALFA (Cur_Subp) - or else not Body_Is_In_ALFA (Cur_Subp) - then - Error_Pragma - ("pragma% is placed after violation" - & " of 'A'L'F'A"); - end if; + else + Error_Pragma ("wrong placement for pragma%"); + end if; + end; - Set_Formal_Proof_On (Cur_Subp); + -- Second parameter is optional, it is never analyzed - else - Error_Pragma ("wrong placement for pragma%"); - end if; - end; - end if; - end if; + elsif No (Arg2) then + null; - -- Second unanalyzed parameter is optional + -- Here if we have a second parameter - if No (Arg2) then - null; - else - Arg := Next (Arg2); - while Present (Arg) loop - Exp := Get_Pragma_Arg (Arg); - Analyze (Exp); + else + -- Second parameter must be identifier - if Is_Entity_Name (Exp) then - null; + Check_Arg_Is_Identifier (Arg2); - -- For string literals, we assume Standard_String as the - -- type, unless the string contains wide or wide_wide - -- characters. + -- Process remaining parameters if any - elsif Nkind (Exp) = N_String_Literal then - if Has_Wide_Wide_Character (Exp) then - Resolve (Exp, Standard_Wide_Wide_String); - elsif Has_Wide_Character (Exp) then - Resolve (Exp, Standard_Wide_String); - else - Resolve (Exp, Standard_String); - end if; + Arg := Next (Arg2); + while Present (Arg) loop + Exp := Get_Pragma_Arg (Arg); + Analyze (Exp); - elsif Is_Overloaded (Exp) then - Error_Pragma_Arg - ("ambiguous argument for pragma%", Exp); + if Is_Entity_Name (Exp) then + null; + + -- For string literals, we assume Standard_String as the + -- type, unless the string contains wide or wide_wide + -- characters. + elsif Nkind (Exp) = N_String_Literal then + if Has_Wide_Wide_Character (Exp) then + Resolve (Exp, Standard_Wide_Wide_String); + elsif Has_Wide_Character (Exp) then + Resolve (Exp, Standard_Wide_String); else - Resolve (Exp); + Resolve (Exp, Standard_String); end if; - Next (Arg); - end loop; - end if; - end; + elsif Is_Overloaded (Exp) then + Error_Pragma_Arg + ("ambiguous argument for pragma%", Exp); + + else + Resolve (Exp); + end if; + + Next (Arg); + end loop; + end if; end Annotate; ------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index e8773a44a28..62b75670654 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -291,8 +291,7 @@ package Sem_Util is -- specification, and calls to the subprogram, from being in ALFA. -- If the subprogram being marked as not in ALFA is annotated with - -- Formal_Proof being On, then an error is issued with message Msg on node - -- N. + -- Formal_Proof On, then an error is issued with message Msg on node N. function Defining_Entity (N : Node_Id) return Entity_Id; -- Given a declaration N, returns the associated defining entity. If the diff --git a/gcc/ada/targparm.ads b/gcc/ada/targparm.ads index 7db350be24c..fa6e25ede9f 100644 --- a/gcc/ada/targparm.ads +++ b/gcc/ada/targparm.ads @@ -26,8 +26,6 @@ -- This package obtains parameters from the target runtime version of System, -- to indicate parameters relevant to the target environment. --- Is it right for this to be modified GPL??? - -- Conceptually, these parameters could be obtained using rtsfind, but -- we do not do this for four reasons: