OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes]

Browse Source 
2011-08-04  Eric Botcazou  <ebotcazou@adacore.com>

	* bindgen.adb: Add comments.

2011-08-04  Yannick Moy  <moy@adacore.com>

	* 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  <dewar@adacore.com>

	* 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
This commit is contained in:
Arnaud Charlet 2011-08-04 10:50:25 +02:00
parent 39ade2f908
commit a4640a3936
17 changed files with 197 additions and 136 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
gcc/ada/ChangeLog
View File

@ -1,3 +1,20 @@
2011-08-04 Eric Botcazou <ebotcazou@adacore.com>
* bindgen.adb: Add comments.
2011-08-04 Yannick Moy <moy@adacore.com>
* 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 <dewar@adacore.com>
* 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 <quinot@adacore.com>
* s-pooloc.ads, s-pooglo.ads: Minor reformatting

6
gcc/ada/bindgen.adb
View File

@ -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 ("");

50
gcc/ada/einfo.adb
View File

@ -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));

16
gcc/ada/einfo.ads
View File

@ -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);

2
gcc/ada/exp_ch6.adb
View File

@ -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,

11
gcc/ada/exp_ch7.adb
View File

@ -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

10
gcc/ada/gnat1drv.adb
View File

@ -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;

12
gcc/ada/layout.adb
View File

@ -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;

8
gcc/ada/osint-c.ads
View File

@ -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

2
gcc/ada/s-pooloc.adb
View File

@ -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;

4
gcc/ada/sem_ch13.adb
View File

@ -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;

2
gcc/ada/sem_ch3.adb
View File

@ -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;

5
gcc/ada/sem_ch5.adb
View File

@ -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;

2
gcc/ada/sem_ch6.adb
View File

@ -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;

181
gcc/ada/sem_prag.adb
View File

@ -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;
Check_Arg_Is_Identifier (Arg2);
Check_Arg_Count (2);
if Chars (Get_Pragma_Arg (Arg2)) /= Name_On
and then Chars (Get_Pragma_Arg (Arg2)) /= Name_Off
then
Error_Pragma_Arg
("wrong second argument for pragma%", Arg2);
end if;
if Chars (Get_Pragma_Arg (Arg2)) = Name_On then
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
-- 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.
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;
Set_Formal_Proof_On (Cur_Subp);
else
Error_Pragma ("wrong placement for pragma%");
end if;
end;
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;
-- Second unanalyzed parameter is optional
Check_Arg_Count (2);
Check_Arg_Is_One_Of (Arg2, Name_On, Name_Off);
if No (Arg2) then
null;
else
Arg := Next (Arg2);
while Present (Arg) loop
Exp := Get_Pragma_Arg (Arg);
Analyze (Exp);
declare
Cur_Subp : constant Entity_Id := Current_Subprogram;
if Is_Entity_Name (Exp) then
null;
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
-- these violations.
-- 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, Standard_String);
end if;
elsif Is_Overloaded (Exp) then
Error_Pragma_Arg
("ambiguous argument for pragma%", Exp);
else
Resolve (Exp);
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;
Next (Arg);
end loop;
end if;
end;
-- We treat this as a Rep_Item to record it on the rep
-- item chain for easy location later on.
Record_Rep_Item (Cur_Subp, N);
else
Error_Pragma ("wrong placement for pragma%");
end if;
end;
-- Second parameter is optional, it is never analyzed
elsif No (Arg2) then
null;
-- Here if we have a second parameter
else
-- Second parameter must be identifier
Check_Arg_Is_Identifier (Arg2);
-- Process remaining parameters if any
Arg := Next (Arg2);
while Present (Arg) loop
Exp := Get_Pragma_Arg (Arg);
Analyze (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, Standard_String);
end if;
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;
------------

3
gcc/ada/sem_util.ads
View File

@ -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

2
gcc/ada/targparm.ads
View File

@ -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: