+2015-11-18 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * atree.adb (Elist11): New routine.
+ (Set_Elist11): New routine.
+ * atree.ads (Elist11): New routine.
+ (Set_Elist11): New routine.
+ * atree.h: Define Elist11.
+ * contracts.adb (Analyze_Object_Contract): Verify the legality
+ of all references to a variable given that the variable is a
+ constituent of a single protected/task type.
+ * einfo.adb: Part_Of_References now utilizes Elist11.
+ (Part_Of_References): New routine.
+ (Set_Part_Of_References): New routine.
+ (Write_Field11_Name): Add output for Part_Of_References.
+ * einfo.ads New attribute Part_Of_References along with usage
+ in entities.
+ (Part_Of_References): New routine along with
+ pragma Inline.
+ (Set_Part_Of_References): New routine along with pragma Inline.
+ * sem_prag.adb (Analyze_Constituent): Record a possible
+ reference to a concurrent constituent.
+ (Analyze_Global_Item): Record a possible reference to a concurrent
+ constituent.
+ (Analyze_Input_Output): Record a possible reference to a
+ concurrent constituent.
+ * sem_res.adb (Resolve_Entity_Name): Record a possible reference
+ to a concurrent constituent.
+ * sem_util.adb (Check_Part_Of_Reference): New routine.
+ (Record_Possible_Part_Of_Reference): New routine.
+ * sem_util.ads (Check_Part_Of_Reference): New routine.
+ (Record_Possible_Part_Of_Reference): New routine.
+
+2015-11-18 Ed Schonberg <schonberg@adacore.com>
+
+ * checks.adb (Apply_Arithmetic_Overflow_Minimized_Eliminated):
+ An if_expression is the proper place to apply the overflow
+ minimization procedure if its context is not an enclosing
+ arithmetic expression.
+
2015-11-18 Arnaud Charlet <charlet@adacore.com>
* gnat_ugn/gnat_project_manager.rst,
end if;
end Elist10;
+ function Elist11 (N : Node_Id) return Elist_Id is
+ pragma Assert (Nkind (N) in N_Entity);
+ Value : constant Union_Id := Nodes.Table (N + 1).Field11;
+ begin
+ if Value = 0 then
+ return No_Elist;
+ else
+ return Elist_Id (Value);
+ end if;
+ end Elist11;
+
function Elist13 (N : Node_Id) return Elist_Id is
pragma Assert (Nkind (N) in N_Entity);
Value : constant Union_Id := Nodes.Table (N + 2).Field6;
Nodes.Table (N + 1).Field10 := Union_Id (Val);
end Set_Elist10;
+ procedure Set_Elist11 (N : Node_Id; Val : Elist_Id) is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ Nodes.Table (N + 1).Field11 := Union_Id (Val);
+ end Set_Elist11;
+
procedure Set_Elist13 (N : Node_Id; Val : Elist_Id) is
begin
pragma Assert (Nkind (N) in N_Entity);
function Elist10 (N : Node_Id) return Elist_Id;
pragma Inline (Elist10);
+ function Elist11 (N : Node_Id) return Elist_Id;
+ pragma Inline (Elist11);
+
function Elist13 (N : Node_Id) return Elist_Id;
pragma Inline (Elist13);
procedure Set_Elist10 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist10);
+ procedure Set_Elist11 (N : Node_Id; Val : Elist_Id);
+ pragma Inline (Set_Elist11);
+
procedure Set_Elist13 (N : Node_Id; Val : Elist_Id);
pragma Inline (Set_Elist13);
#define Elist8(N) Field8 (N)
#define Elist9(N) Field9 (N)
#define Elist10(N) Field10 (N)
+#define Elist11(N) Field11 (N)
#define Elist13(N) Field13 (N)
#define Elist15(N) Field15 (N)
#define Elist16(N) Field16 (N)
or else (Nkind (P) = N_Range
and then Nkind (Parent (P)) in N_Membership_Test)
then
- return;
+ -- If_Expressions and Case_Expressions are treated as arithmetic
+ -- ops, but if they appear in an assignment or similar contexts
+ -- there is no overflow check that starts from that parent node,
+ -- so apply check now.
+
+ if Nkind_In (P, N_If_Expression, N_Case_Expression)
+ and then not Is_Signed_Integer_Arithmetic_Op (Parent (P))
+ then
+ null;
+ else
+ return;
+ end if;
end if;
-- Otherwise, we have a top level arithmetic operation node, and this
Analyze_And_Resolve (Op);
end;
- -- Here we know the result is Long_Long_Integer'Base, of that it has
+ -- Here we know the result is Long_Long_Integer'Base, or that it has
-- been rewritten because the parent operation is a conversion. See
-- Apply_Arithmetic_Overflow_Strict.Conversion_Optimization.
Items : Node_Id;
Mode : SPARK_Mode_Type;
Prag : Node_Id;
+ Ref_Elmt : Elmt_Id;
Restore_Mode : Boolean := False;
Seen : Boolean := False;
if Present (Prag) then
Analyze_Part_Of_In_Decl_Part (Prag);
+ -- The variable is a constituent of a single protected/task type
+ -- and behaves as a component of the type. Verify that references
+ -- to the variable occur within the definition or body of the type
+ -- (SPARK RM 9.3).
+
+ if Present (Encapsulating_State (Obj_Id))
+ and then Is_Single_Concurrent_Object
+ (Encapsulating_State (Obj_Id))
+ and then Present (Part_Of_References (Obj_Id))
+ then
+ Ref_Elmt := First_Elmt (Part_Of_References (Obj_Id));
+ while Present (Ref_Elmt) loop
+ Check_Part_Of_Reference (Obj_Id, Node (Ref_Elmt));
+ Next_Elmt (Ref_Elmt);
+ end loop;
+ end if;
+
-- Otherwise check whether the lack of indicator Part_Of agrees with
-- the placement of the variable with respect to the state space.
-- Normalized_Position_Max Uint10
-- Part_Of_Constituents Elist10
+ -- Block_Node Node11
-- Component_Bit_Offset Uint11
-- Full_View Node11
-- Entry_Component Node11
-- Enumeration_Pos Uint11
-- Generic_Homonym Node11
+ -- Part_Of_References Elist11
-- Protected_Body_Subprogram Node11
- -- Block_Node Node11
-- Barrier_Function Node12
-- Enumeration_Rep Uint12
return Elist10 (Id);
end Part_Of_Constituents;
+ function Part_Of_References (Id : E) return L is
+ begin
+ pragma Assert (Ekind (Id) = E_Variable);
+ return Elist11 (Id);
+ end Part_Of_References;
+
function Partial_View_Has_Unknown_Discr (Id : E) return B is
begin
pragma Assert (Is_Type (Id));
Set_Elist10 (Id, V);
end Set_Part_Of_Constituents;
+ procedure Set_Part_Of_References (Id : E; V : L) is
+ begin
+ pragma Assert (Ekind (Id) = E_Variable);
+ Set_Elist11 (Id, V);
+ end Set_Part_Of_References;
+
procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True) is
begin
pragma Assert (Is_Type (Id));
when E_Generic_Package =>
Write_Str ("Generic_Homonym");
- when E_Function |
- E_Procedure |
- E_Entry |
- E_Entry_Family =>
+ when E_Variable =>
+ Write_Str ("Part_Of_References");
+
+ when E_Entry |
+ E_Entry_Family |
+ E_Function |
+ E_Procedure =>
Write_Str ("Protected_Body_Subprogram");
when others =>
-- constituents that are subject to indicator Part_Of (both aspect and
-- option variants).
+-- Part_Of_References (Elist11)
+-- Present in variable entities. Contains all references to the variable
+-- when it is subject to pragma Part_Of. If the variable is a constituent
+-- of a single protected/task type, the references are examined as they
+-- must appear only within the type defintion and the corresponding body.
+
-- Partial_View_Has_Unknown_Discr (Flag280)
-- Present in all types. Set to Indicate that the partial view of a type
-- has unknown discriminants. A default initialization of an object of
-- Hiding_Loop_Variable (Node8)
-- Current_Value (Node9)
-- Part_Of_Constituents (Elist10)
+ -- Part_Of_References (Elist11)
-- Esize (Uint12)
-- Extra_Accessibility (Node13)
-- Alignment (Uint14)
function Packed_Array_Impl_Type (Id : E) return E;
function Parent_Subtype (Id : E) return E;
function Part_Of_Constituents (Id : E) return L;
+ function Part_Of_References (Id : E) return L;
function Partial_View_Has_Unknown_Discr (Id : E) return B;
function Pending_Access_Types (Id : E) return L;
function Postconditions_Proc (Id : E) return E;
procedure Set_Packed_Array_Impl_Type (Id : E; V : E);
procedure Set_Parent_Subtype (Id : E; V : E);
procedure Set_Part_Of_Constituents (Id : E; V : L);
+ procedure Set_Part_Of_References (Id : E; V : L);
procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True);
procedure Set_Pending_Access_Types (Id : E; V : L);
procedure Set_Postconditions_Proc (Id : E; V : E);
pragma Inline (Parameter_Mode);
pragma Inline (Parent_Subtype);
pragma Inline (Part_Of_Constituents);
+ pragma Inline (Part_Of_References);
pragma Inline (Partial_View_Has_Unknown_Discr);
pragma Inline (Pending_Access_Types);
pragma Inline (Postconditions_Proc);
pragma Inline (Set_Packed_Array_Impl_Type);
pragma Inline (Set_Parent_Subtype);
pragma Inline (Set_Part_Of_Constituents);
+ pragma Inline (Set_Part_Of_References);
pragma Inline (Set_Partial_View_Has_Unknown_Discr);
pragma Inline (Set_Pending_Access_Types);
pragma Inline (Set_Postconditions_Proc);
if Ekind (Item_Id) = E_Abstract_State then
Append_New_Elmt (Item_Id, States_Seen);
+
+ -- The variable may eventually become a constituent of a
+ -- single protected/task type. Record the reference now
+ -- and verify its legality when analyzing the contract of
+ -- the variable (SPARK RM 9.3).
+
+ elsif Ekind (Item_Id) = E_Variable then
+ Record_Possible_Part_Of_Reference
+ (Var_Id => Item_Id,
+ Ref => Item);
end if;
if Ekind_In (Item_Id, E_Abstract_State,
if Ekind (Item_Id) = E_Abstract_State then
Append_New_Elmt (Item_Id, States_Seen);
+
+ -- The variable may eventually become a constituent of a single
+ -- protected/task type. Record the reference now and verify its
+ -- legality when analyzing the contract of the variable
+ -- (SPARK RM 9.3).
+
+ elsif Ekind (Item_Id) = E_Variable then
+ Record_Possible_Part_Of_Reference
+ (Var_Id => Item_Id,
+ Ref => Item);
end if;
if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
then
Match_Constituent (Constit_Id);
+ -- The variable may eventually become a constituent of a
+ -- single protected/task type. Record the reference now
+ -- and verify its legality when analyzing the contract of
+ -- the variable (SPARK RM 9.3).
+
+ if Ekind (Constit_Id) = E_Variable then
+ Record_Possible_Part_Of_Reference
+ (Var_Id => Constit_Id,
+ Ref => Constit);
+ end if;
+
-- Otherwise the constituent is illegal
else
then
Check_Elab_Call (N);
end if;
+
+ -- The variable may eventually become a constituent of a single
+ -- protected/task type. Record the reference now and verify its
+ -- legality when analyzing the contract of the variable
+ -- (SPARK RM 9.3).
+
+ if Ekind (E) = E_Variable then
+ Record_Possible_Part_Of_Reference (E, N);
+ end if;
end if;
-- A Ghost entity must appear in a specific context
end if;
end Cannot_Raise_Constraint_Error;
+ -----------------------------
+ -- Check_Part_Of_Reference --
+ -----------------------------
+
+ procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id) is
+ Conc_Typ : constant Entity_Id := Encapsulating_State (Var_Id);
+ Decl : Node_Id;
+ OK_Use : Boolean := False;
+ Par : Node_Id;
+ Prag_Nam : Name_Id;
+ Spec_Id : Entity_Id;
+
+ begin
+ -- Traverse the parent chain looking for a suitable context for the
+ -- reference to the concurrent constituent.
+
+ Par := Parent (Ref);
+ while Present (Par) loop
+ if Nkind (Par) = N_Pragma then
+ Prag_Nam := Pragma_Name (Par);
+
+ -- A concurrent constituent is allowed to appear in pragmas
+ -- Initial_Condition and Initializes as this is part of the
+ -- elaboration checks for the constituent (SPARK RM 9.3).
+
+ if Nam_In (Prag_Nam, Name_Initial_Condition, Name_Initializes) then
+ OK_Use := True;
+ exit;
+
+ -- When the reference appears within pragma Depends or Global,
+ -- check whether the pragma applies to a single task type. Note
+ -- that the pragma is not encapsulated by the type definition,
+ -- but this is still a valid context.
+
+ elsif Nam_In (Prag_Nam, Name_Depends, Name_Global) then
+ Decl := Find_Related_Declaration_Or_Body (Par);
+
+ if Nkind (Decl) = N_Object_Declaration
+ and then Defining_Entity (Decl) = Conc_Typ
+ then
+ OK_Use := True;
+ exit;
+ end if;
+ end if;
+
+ -- The reference appears somewhere in the definition of the single
+ -- protected/task type (SPARK RM 9.3).
+
+ elsif Nkind_In (Par, N_Single_Protected_Declaration,
+ N_Single_Task_Declaration)
+ and then Defining_Entity (Par) = Conc_Typ
+ then
+ OK_Use := True;
+ exit;
+
+ -- The reference appears within the expanded declaration or the body
+ -- of the single protected/task type (SPARK RM 9.3).
+
+ elsif Nkind_In (Par, N_Protected_Body,
+ N_Protected_Type_Declaration,
+ N_Task_Body,
+ N_Task_Type_Declaration)
+ then
+ Spec_Id := Unique_Defining_Entity (Par);
+
+ if Present (Anonymous_Object (Spec_Id))
+ and then Anonymous_Object (Spec_Id) = Conc_Typ
+ then
+ OK_Use := True;
+ exit;
+ end if;
+
+ -- The reference has been relocated within an internally generated
+ -- package or subprogram. Assume that the reference is legal as the
+ -- real check was already performed in the original context of the
+ -- reference.
+
+ elsif Nkind_In (Par, N_Package_Body,
+ N_Package_Declaration,
+ N_Subprogram_Body,
+ N_Subprogram_Declaration)
+ and then not Comes_From_Source (Par)
+ then
+ OK_Use := True;
+ exit;
+
+ -- The reference has been relocated to an inlined body for GNATprove.
+ -- Assume that the reference is legal as the real check was already
+ -- performed in the original context of the reference.
+
+ elsif GNATprove_Mode
+ and then Nkind (Par) = N_Subprogram_Body
+ and then Chars (Defining_Entity (Par)) = Name_uParent
+ then
+ OK_Use := True;
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ -- The reference is illegal as it appears outside the definition or
+ -- body of the single protected/task type.
+
+ if not OK_Use then
+ Error_Msg_NE
+ ("reference to variable & cannot appear in this context",
+ Ref, Var_Id);
+ Error_Msg_Name_1 := Chars (Var_Id);
+
+ if Ekind (Conc_Typ) = E_Protected_Type then
+ Error_Msg_NE
+ ("\% is constituent of single protected type &", Ref, Conc_Typ);
+ else
+ Error_Msg_NE
+ ("\% is constituent of single task type &", Ref, Conc_Typ);
+ end if;
+ end if;
+ end Check_Part_Of_Reference;
+
-----------------------------------------
-- Check_Dynamically_Tagged_Expression --
-----------------------------------------
Set_Sloc (Endl, Loc);
end Process_End_Label;
+ ---------------------------------------
+ -- Record_Possible_Part_Of_Reference --
+ ---------------------------------------
+
+ procedure Record_Possible_Part_Of_Reference
+ (Var_Id : Entity_Id;
+ Ref : Node_Id)
+ is
+ Encap : constant Entity_Id := Encapsulating_State (Var_Id);
+ Refs : Elist_Id;
+
+ begin
+ -- The variable is a constituent of a single protected/task type. Such
+ -- a variable acts as a component of the type and must appear within a
+ -- specific region (SPARK RM 9.3). Instead of recording the reference,
+ -- verify its legality now.
+
+ if Present (Encap) and then Is_Single_Concurrent_Object (Encap) then
+ Check_Part_Of_Reference (Var_Id, Ref);
+
+ -- The variable is subject to pragma Part_Of and may eventually become a
+ -- constituent of a single protected/task type. Record the reference to
+ -- verify its placement when the contract of the variable is analyzed.
+
+ elsif Present (Get_Pragma (Var_Id, Pragma_Part_Of)) then
+ Refs := Part_Of_References (Var_Id);
+
+ if No (Refs) then
+ Refs := New_Elmt_List;
+ Set_Part_Of_References (Var_Id, Refs);
+ end if;
+
+ Append_Elmt (Ref, Refs);
+ end if;
+ end Record_Possible_Part_Of_Reference;
+
----------------
-- Referenced --
----------------
-- not necessarily mean that CE could be raised, but a response of True
-- means that for sure CE cannot be raised.
+ procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id);
+ -- Verify the legality of reference Ref to variable Var_Id when the
+ -- variable is a constituent of a single protected/task type.
+
procedure Check_Dynamically_Tagged_Expression
(Expr : Node_Id;
Typ : Entity_Id;
-- parameter Ent gives the entity to which the End_Label refers,
-- and to which cross-references are to be generated.
+ procedure Record_Possible_Part_Of_Reference
+ (Var_Id : Entity_Id;
+ Ref : Node_Id);
+ -- Save reference Ref to variable Var_Id when the variable is subject to
+ -- pragma Part_Of. If the variable is known to be a constituent of a single
+ -- protected/task type, the legality of the reference is verified and the
+ -- save does not take place.
+
function Referenced (Id : Entity_Id; Expr : Node_Id) return Boolean;
-- Determine whether entity Id is referenced within expression Expr
projects / gcc.git / commitdiff