+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
-- Default_Expr_Function Node21
-- Discriminant_Constraint Elist21
-- Interface_Name Node21
+ -- Original_Access_Type Node21
-- Original_Array_Type Node21
-- Small_Value Ureal21
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));
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));
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");
-- 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
-- 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)
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;
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);
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);
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);
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.
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
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 --
-------------------------------
-- 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
projects / gcc.git / commitdiff