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

[multiple changes] 

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

	* sem_ch3.adb (Analyze_Object_Declaration): issue an error in formal
	mode on initialization expression which does not respect SPARK
	restrictions.
	* sem_util.adb, sem_util.ads (Is_SPARK_Initialization_Expr): determines
	if the tree referenced by its argument represents an initialization
	expression in SPARK, suitable for initializing an object in an object
	declaration.

2011-08-02  Javier Miranda  <miranda@adacore.com>

	* exp_ch9.adb (Expand_Access_Protected_Subprogram_Type): Link the
	internally generated access to subprogram with its associated protected
	subprogram type.
	* einfo.ads, einfo.adb (Original_Access_Type): New attribute.

From-SVN: r177139
This commit is contained in:
Arnaud Charlet 2011-08-02 14:44:24 +02:00
parent 15b682ca92
commit aa1e353a7a
7 changed files with 176 additions and 0 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-02 Yannick Moy <moy@adacore.com>
* sem_ch3.adb (Analyze_Object_Declaration): issue an error in formal
mode on initialization expression which does not respect SPARK
restrictions.
* sem_util.adb, sem_util.ads (Is_SPARK_Initialization_Expr): determines
if the tree referenced by its argument represents an initialization
expression in SPARK, suitable for initializing an object in an object
declaration.
2011-08-02 Javier Miranda <miranda@adacore.com>
* exp_ch9.adb (Expand_Access_Protected_Subprogram_Type): Link the
internally generated access to subprogram with its associated protected
subprogram type.
* einfo.ads, einfo.adb (Original_Access_Type): New attribute.
2011-08-02 Geert Bosch <bosch@adacore.com>
* cstand.adb (Register_Float_Type): Print information about type to

16
gcc/ada/einfo.adb
View File

@ -181,6 +181,7 @@ package body Einfo is
-- Default_Expr_Function Node21
-- Discriminant_Constraint Elist21
-- Interface_Name Node21
-- Original_Access_Type Node21
-- Original_Array_Type Node21
-- Small_Value Ureal21
@ -2353,6 +2354,12 @@ package body Einfo is
return Flag242 (Id);
end Optimize_Alignment_Time;
function Original_Access_Type (Id : E) return E is
begin
pragma Assert (Ekind (Id) = E_Access_Subprogram_Type);
return Node21 (Id);
end Original_Access_Type;
function Original_Array_Type (Id : E) return E is
begin
pragma Assert (Is_Array_Type (Id) or else Is_Modular_Integer_Type (Id));
@ -4852,6 +4859,12 @@ package body Einfo is
Set_Flag242 (Id, V);
end Set_Optimize_Alignment_Time;
procedure Set_Original_Access_Type (Id : E; V : E) is
begin
pragma Assert (Ekind (Id) = E_Access_Subprogram_Type);
Set_Node21 (Id, V);
end Set_Original_Access_Type;
procedure Set_Original_Array_Type (Id : E; V : E) is
begin
pragma Assert (Is_Array_Type (Id) or else Is_Modular_Integer_Type (Id));
@ -8332,6 +8345,9 @@ package body Einfo is
when Fixed_Point_Kind =>
Write_Str ("Small_Value");
when E_Access_Subprogram_Type =>
Write_Str ("Original_Access_Type");
when E_In_Parameter =>
Write_Str ("Default_Expr_Function");

11
gcc/ada/einfo.ads
View File

@ -3206,6 +3206,12 @@ package Einfo is
-- Optimize_Alignment (Off) mode applies to the type/object, then neither
-- of the flags Optimize_Alignment_Space/Optimize_Alignment_Time is set.
-- Original_Access_Type (Node21)
-- Present in E_Access_Subprogram_Type entities. Set only if the access
-- type was generated by the expander as part of processing an access
-- to protected subprogram type. Points to the access to protected
-- subprogram type.
-- Original_Array_Type (Node21)
-- Present in modular types and array types and subtypes. Set only
-- if the Is_Packed_Array_Type flag is set, indicating that the type
@ -4876,6 +4882,7 @@ package Einfo is
-- E_Access_Subprogram_Type
-- Equivalent_Type (Node18) (remote types only)
-- Directly_Designated_Type (Node20)
-- Original_Access_Type (Node21)
-- Needs_No_Actuals (Flag22)
-- Can_Use_Internal_Rep (Flag229)
-- (plus type attributes)
@ -6223,6 +6230,7 @@ package Einfo is
function OK_To_Reorder_Components (Id : E) return B;
function Optimize_Alignment_Space (Id : E) return B;
function Optimize_Alignment_Time (Id : E) return B;
function Original_Access_Type (Id : E) return E;
function Original_Array_Type (Id : E) return E;
function Original_Record_Component (Id : E) return E;
function Overlays_Constant (Id : E) return B;
@ -6812,6 +6820,7 @@ package Einfo is
procedure Set_OK_To_Reorder_Components (Id : E; V : B := True);
procedure Set_Optimize_Alignment_Space (Id : E; V : B := True);
procedure Set_Optimize_Alignment_Time (Id : E; V : B := True);
procedure Set_Original_Access_Type (Id : E; V : E);
procedure Set_Original_Array_Type (Id : E; V : E);
procedure Set_Original_Record_Component (Id : E; V : E);
procedure Set_Overlays_Constant (Id : E; V : B := True);
@ -7546,6 +7555,7 @@ package Einfo is
pragma Inline (OK_To_Reorder_Components);
pragma Inline (Optimize_Alignment_Space);
pragma Inline (Optimize_Alignment_Time);
pragma Inline (Original_Access_Type);
pragma Inline (Original_Array_Type);
pragma Inline (Original_Record_Component);
pragma Inline (Overlays_Constant);
@ -7943,6 +7953,7 @@ package Einfo is
pragma Inline (Set_OK_To_Rename);
pragma Inline (Set_Optimize_Alignment_Space);
pragma Inline (Set_Optimize_Alignment_Time);
pragma Inline (Set_Original_Access_Type);
pragma Inline (Set_Original_Array_Type);
pragma Inline (Set_Original_Record_Component);
pragma Inline (Set_Overlays_Constant);

6
gcc/ada/exp_ch9.adb
View File

@ -5067,6 +5067,12 @@ package body Exp_Ch9 is
Insert_After (N, Decl1);
Analyze (Decl1);
-- Associate the access to subprogram with its original access to
-- protected subprogram type. Needed by the backend to know that this
-- type corresponds with an access to protected subprogram type.
Set_Original_Access_Type (D_T2, T);
-- Create Equivalent_Type, a record with two components for an access to
-- object and an access to subprogram.

9
gcc/ada/sem_ch3.adb
View File

@ -3168,6 +3168,15 @@ package body Sem_Ch3 is
Apply_Scalar_Range_Check (E, T);
Apply_Static_Length_Check (E, T);
if Nkind (Original_Node (N)) = N_Object_Declaration
and then Comes_From_Source (Original_Node (N))
and then Formal_Verification_Mode -- only call test if needed
and then not Is_SPARK_Initialization_Expr (E)
then
Check_Formal_Restriction
("initialization expression is not appropriate", E);
end if;
end if;
-- If the No_Streams restriction is set, check that the type of the

112
gcc/ada/sem_util.adb
View File

@ -7368,6 +7368,118 @@ package body Sem_Util is
end if;
end Is_Selector_Name;
----------------------------------
-- Is_SPARK_Initialization_Expr --
----------------------------------
function Is_SPARK_Initialization_Expr (N : Node_Id) return Boolean is
Is_Ok : Boolean;
Expr, Comp_Assn, Choice : Node_Id;
begin
Is_Ok := True;
pragma Assert (Nkind (N) in N_Subexpr);
case Nkind (N) is
when N_Character_Literal |
N_Integer_Literal |
N_Real_Literal |
N_String_Literal |
N_Expanded_Name |
N_Membership_Test =>
null;
when N_Identifier =>
if Is_Entity_Name (N)
and then Present (Entity (N)) -- needed in some cases
then
case Ekind (Entity (N)) is
when E_Constant |
E_Enumeration_Literal |
E_Named_Integer |
E_Named_Real =>
null;
when others =>
Is_Ok := False;
end case;
end if;
when N_Qualified_Expression |
N_Type_Conversion =>
Is_Ok := Is_SPARK_Initialization_Expr (Expression (N));
when N_Unary_Op =>
Is_Ok := Is_SPARK_Initialization_Expr (Right_Opnd (N));
when N_Binary_Op | N_Short_Circuit =>
Is_Ok := Is_SPARK_Initialization_Expr (Left_Opnd (N))
and then Is_SPARK_Initialization_Expr (Right_Opnd (N));
when N_Aggregate |
N_Extension_Aggregate =>
if Nkind (N) = N_Extension_Aggregate then
Is_Ok := Is_SPARK_Initialization_Expr (Ancestor_Part (N));
end if;
Expr := First (Expressions (N));
while Present (Expr) loop
if not Is_SPARK_Initialization_Expr (Expr) then
Is_Ok := False;
goto Done;
end if;
Next (Expr);
end loop;
Comp_Assn := First (Component_Associations (N));
while Present (Comp_Assn) loop
Choice := First (Choices (Comp_Assn));
while Present (Choice) loop
if Nkind (Choice) in N_Subexpr
and then not Is_SPARK_Initialization_Expr (Choice)
then
Is_Ok := False;
goto Done;
end if;
Next (Choice);
end loop;
Expr := Expression (Comp_Assn);
if Present (Expr) -- needed for box association
and then not Is_SPARK_Initialization_Expr (Expr)
then
Is_Ok := False;
goto Done;
end if;
Next (Comp_Assn);
end loop;
when N_Attribute_Reference =>
if Nkind (Prefix (N)) in N_Subexpr then
Is_Ok := Is_SPARK_Initialization_Expr (Prefix (N));
end if;
Expr := First (Expressions (N));
while Present (Expr) loop
if not Is_SPARK_Initialization_Expr (Expr) then
Is_Ok := False;
goto Done;
end if;
Next (Expr);
end loop;
when others =>
Is_Ok := False;
end case;
<<Done>>
return Is_Ok;
end Is_SPARK_Initialization_Expr;
-------------------------------
-- Is_SPARK_Object_Reference --
-------------------------------

5
gcc/ada/sem_util.ads
View File

@ -828,6 +828,11 @@ package Sem_Util is
-- represent use of the N_Identifier node for a true identifier, when
-- normally such nodes represent a direct name.
function Is_SPARK_Initialization_Expr (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an initialization
-- expression in SPARK, suitable for initializing an object in an object
-- declaration.
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an object in SPARK