From aa1e353a7a34599e90bf9b62b3a463914e242a6c Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 2 Aug 2011 14:44:24 +0200 Subject: [PATCH] [multiple changes] 2011-08-02 Yannick Moy * 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 * 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 --- gcc/ada/ChangeLog | 17 +++++++ gcc/ada/einfo.adb | 16 +++++++ gcc/ada/einfo.ads | 11 +++++ gcc/ada/exp_ch9.adb | 6 +++ gcc/ada/sem_ch3.adb | 9 ++++ gcc/ada/sem_util.adb | 112 +++++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_util.ads | 5 ++ 7 files changed, 176 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 500a0a278d5..f478f3c2007 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,20 @@ +2011-08-02 Yannick Moy + + * 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 + + * 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 * cstand.adb (Register_Float_Type): Print information about type to diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index eb217d49d59..42217f5420f 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -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"); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index e69704d86ab..0366dbeb604 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -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); diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 0312187f1a8..6a15dd532e5 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -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. diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 337ff456c00..5e937249b58 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 91cc8121d60..feddff824e5 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -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; + + <> + return Is_Ok; + end Is_SPARK_Initialization_Expr; + ------------------------------- -- Is_SPARK_Object_Reference -- ------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 715fc1b0499..6803dfb9b66 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -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 -- 2.30.2