+2014-02-06 Robert Dewar <dewar@adacore.com>
+
+ * sprint.adb: Minor reformatting.
+
+2014-02-06 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_ch4.adb (Process_Transient_Object): Add local variable
+ Temp_Ins. When the transient object is initialized by an
+ aggregate, the hook must capture the object after the last
+ component assignment takes place.
+ * exp_ch7.adb (Detect_Subprogram_Call): Expose the subprogram to
+ routine Is_Subprogram_Call.
+ (Is_Subprogram_Call): Inspect an
+ aggregate that has been heavily expanded for subprogram calls.
+ (Process_Transient_Objects): Add local variables Expr, Ptr_Id
+ and Temp_Ins. Remove the nested declare block and adjust the
+ indentation. When the transient object is initialized by an
+ aggregate, the hook must capture the object after the last
+ component assignment takes place.
+
+2014-02-06 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_prag.adb (Analyze_Global_Item): Detect illegal uses of
+ external states with enabled properties that do not match the
+ global mode.
+ (Property_Error): New routine.
+ * sem_res.adb (Property_Error): New routine.
+ (Resolve_Actuals): Detect illegal uses of external variables with
+ enabled properties in procedure calls that do not match the mode of
+ the corresponding formal parameter.
+
+2014-02-06 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_util.adb (Has_Enabled_Property): Rename
+ formal parameter Prop_Nam to Property. Update the comment on usage
+ and all occurrences in the body. Add local variable Prop_Nam. When
+ inspecting a property with an expression, the property name
+ appears as the first choice of the component association.
+
2014-02-04 Robert Dewar <dewar@adacore.com>
* exp_ch5.adb, einfo.ads, freeze.adb, sem_ch8.adb: Minor reformatting.
Fin_Stmts : List_Id;
Ptr_Id : Entity_Id;
Temp_Id : Entity_Id;
+ Temp_Ins : Node_Id;
-- Start of processing for Process_Transient_Object
-- <or>
-- Temp := Obj_Id'Unrestricted_Access;
- Insert_After_And_Analyze (Decl,
+ -- When the transient object is initialized by an aggregate, the hook
+ -- must capture the object after the last component assignment takes
+ -- place. Only then is the object fully initialized.
+
+ if Ekind (Obj_Id) = E_Variable
+ and then Present (Last_Aggregate_Assignment (Obj_Id))
+ then
+ Temp_Ins := Last_Aggregate_Assignment (Obj_Id);
+
+ -- Otherwise the hook seizes the related object immediately
+
+ else
+ Temp_Ins := Decl;
+ end if;
+
+ Insert_After_And_Analyze (Temp_Ins,
Make_Assignment_Statement (Loc,
Name => New_Reference_To (Temp_Id, Loc),
Expression => Expr));
Expression => Make_Integer_Literal (Loc, Counter_Val));
-- Insert the counter after all initialization has been done. The
- -- place of insertion depends on the context. When dealing with a
- -- controlled function, the counter is inserted directly after the
- -- declaration because such objects lack init calls.
+ -- place of insertion depends on the context. If an object is being
+ -- initialized via an aggregate, then the counter must be inserted
+ -- after the last aggregate assignment.
- Find_Last_Init (Decl, Obj_Typ, Count_Ins, Body_Ins);
+ if Ekind (Obj_Id) = E_Variable
+ and then Present (Last_Aggregate_Assignment (Obj_Id))
+ then
+ Count_Ins := Last_Aggregate_Assignment (Obj_Id);
+ Body_Ins := Empty;
+
+ -- In all other cases the counter is inserted after the last call to
+ -- either [Deep_]Initialize or the type specific init proc.
+
+ else
+ Find_Last_Init (Decl, Obj_Typ, Count_Ins, Body_Ins);
+ end if;
Insert_After (Count_Ins, Inc_Decl);
Analyze (Inc_Decl);
function Is_Subprogram_Call (N : Node_Id) return Traverse_Result;
-- Determine whether an arbitrary node denotes a subprogram call
+ procedure Detect_Subprogram_Call is
+ new Traverse_Proc (Is_Subprogram_Call);
+
------------------------
-- Is_Subprogram_Call --
------------------------
function Is_Subprogram_Call (N : Node_Id) return Traverse_Result is
begin
- -- A regular procedure or function call
+ -- Aggregates are usually rewritten into component by component
+ -- assignments and replaced by a reference to a temporary in the
+ -- original tree. Peek in the aggregate to detect function calls.
- if Nkind (N) in N_Subprogram_Call then
- Must_Hook := True;
- return Abandon;
+ if Nkind (N) = N_Identifier
+ and then Nkind_In (Original_Node (N), N_Aggregate,
+ N_Extension_Aggregate)
+ then
+ Detect_Subprogram_Call (Original_Node (N));
+ return OK;
-- Detect a call to a function that returns on the secondary stack
Must_Hook := True;
return Abandon;
+ -- A regular procedure or function call
+
+ elsif Nkind (N) in N_Subprogram_Call then
+ Must_Hook := True;
+ return Abandon;
+
-- Keep searching
else
end if;
end Is_Subprogram_Call;
- procedure Detect_Subprogram_Call is
- new Traverse_Proc (Is_Subprogram_Call);
-
-- Local variables
Built : Boolean := False;
Desig_Typ : Entity_Id;
+ Expr : Node_Id;
Fin_Block : Node_Id;
Fin_Data : Finalization_Exception_Data;
Fin_Decls : List_Id;
Obj_Ref : Node_Id;
Obj_Typ : Entity_Id;
Prev_Fin : Node_Id := Empty;
+ Ptr_Id : Entity_Id;
Stmt : Node_Id;
Stmts : List_Id;
Temp_Id : Entity_Id;
+ Temp_Ins : Node_Id;
-- Start of processing for Process_Transient_Objects
-- time around.
if not Built then
+ Built := True;
Fin_Decls := New_List;
Build_Object_Declarations (Fin_Data, Fin_Decls, Loc);
-
- Built := True;
end if;
-- Transient variables associated with subprogram calls need
-- "hooks" are picked up by the finalization machinery.
if Must_Hook then
- declare
- Expr : Node_Id;
- Ptr_Id : Entity_Id;
- begin
- -- Step 1: Create an access type which provides a
- -- reference to the transient object. Generate:
+ -- Step 1: Create an access type which provides a reference
+ -- to the transient object. Generate:
- -- Ann : access [all] <Desig_Typ>;
+ -- Ann : access [all] <Desig_Typ>;
- Ptr_Id := Make_Temporary (Loc, 'A');
+ Ptr_Id := Make_Temporary (Loc, 'A');
- Insert_Action (Stmt,
- Make_Full_Type_Declaration (Loc,
- Defining_Identifier => Ptr_Id,
- Type_Definition =>
- Make_Access_To_Object_Definition (Loc,
- All_Present =>
- Ekind (Obj_Typ) = E_General_Access_Type,
- Subtype_Indication =>
- New_Reference_To (Desig_Typ, Loc))));
+ Insert_Action (Stmt,
+ Make_Full_Type_Declaration (Loc,
+ Defining_Identifier => Ptr_Id,
+ Type_Definition =>
+ Make_Access_To_Object_Definition (Loc,
+ All_Present =>
+ Ekind (Obj_Typ) = E_General_Access_Type,
+ Subtype_Indication =>
+ New_Reference_To (Desig_Typ, Loc))));
- -- Step 2: Create a temporary which acts as a hook to
- -- the transient object. Generate:
+ -- Step 2: Create a temporary which acts as a hook to the
+ -- transient object. Generate:
- -- Temp : Ptr_Id := null;
+ -- Temp : Ptr_Id := null;
- Temp_Id := Make_Temporary (Loc, 'T');
+ Temp_Id := Make_Temporary (Loc, 'T');
- Insert_Action (Stmt,
- Make_Object_Declaration (Loc,
- Defining_Identifier => Temp_Id,
- Object_Definition =>
- New_Reference_To (Ptr_Id, Loc)));
+ Insert_Action (Stmt,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Temp_Id,
+ Object_Definition =>
+ New_Reference_To (Ptr_Id, Loc)));
- -- Mark the temporary as a transient hook. This signals
- -- the machinery in Build_Finalizer to recognize this
- -- special case.
+ -- Mark the temporary as a transient hook. This signals the
+ -- machinery in Build_Finalizer to recognize this special
+ -- case.
- Set_Status_Flag_Or_Transient_Decl (Temp_Id, Stmt);
+ Set_Status_Flag_Or_Transient_Decl (Temp_Id, Stmt);
- -- Step 3: Hook the transient object to the temporary
+ -- Step 3: Hook the transient object to the temporary
- if Is_Access_Type (Obj_Typ) then
- Expr :=
- Convert_To (Ptr_Id, New_Reference_To (Obj_Id, Loc));
- else
- Expr :=
- Make_Attribute_Reference (Loc,
- Prefix => New_Reference_To (Obj_Id, Loc),
- Attribute_Name => Name_Unrestricted_Access);
- end if;
+ if Is_Access_Type (Obj_Typ) then
+ Expr :=
+ Convert_To (Ptr_Id, New_Reference_To (Obj_Id, Loc));
+ else
+ Expr :=
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Reference_To (Obj_Id, Loc),
+ Attribute_Name => Name_Unrestricted_Access);
+ end if;
- -- Generate:
- -- Temp := Ptr_Id (Obj_Id);
- -- <or>
- -- Temp := Obj_Id'Unrestricted_Access;
-
- Insert_After_And_Analyze (Stmt,
- Make_Assignment_Statement (Loc,
- Name => New_Reference_To (Temp_Id, Loc),
- Expression => Expr));
- end;
+ -- Generate:
+ -- Temp := Ptr_Id (Obj_Id);
+ -- <or>
+ -- Temp := Obj_Id'Unrestricted_Access;
+
+ -- When the transient object is initialized by an aggregate,
+ -- the hook must capture the object after the last component
+ -- assignment takes place. Only then is the object fully
+ -- initialized.
+
+ if Ekind (Obj_Id) = E_Variable
+ and then Present (Last_Aggregate_Assignment (Obj_Id))
+ then
+ Temp_Ins := Last_Aggregate_Assignment (Obj_Id);
+
+ -- Otherwise the hook seizes the related object immediately
+
+ else
+ Temp_Ins := Stmt;
+ end if;
+
+ Insert_After_And_Analyze (Temp_Ins,
+ Make_Assignment_Statement (Loc,
+ Name => New_Reference_To (Temp_Id, Loc),
+ Expression => Expr));
end if;
Stmts := New_List;
(Item : Node_Id;
Global_Mode : Name_Id)
is
+ procedure Property_Error
+ (State_Id : Entity_Id;
+ Prop_Nam : Name_Id);
+ -- Emit an error concerning state State_Id with enabled property
+ -- Async_Readers, Effective_Reads or Effective_Writes that is not
+ -- marked as In_Out or Output item.
+
+ --------------------
+ -- Property_Error --
+ --------------------
+
+ procedure Property_Error
+ (State_Id : Entity_Id;
+ Prop_Nam : Name_Id)
+ is
+ begin
+ Error_Msg_Name_1 := Prop_Nam;
+ Error_Msg_NE
+ ("external state & with enabled property % must have mode "
+ & "In_Out or Output (SPARK RM 7.1.2(7))", Item, State_Id);
+ end Property_Error;
+
+ -- Local variables
+
Item_Id : Entity_Id;
+ -- Start of processing for Analyze_Global_Item
+
begin
-- Detect one of the following cases
Ref => Item);
end if;
+ -- Detect an external state with an enabled property that
+ -- does not match the mode of the state.
+
+ if Global_Mode = Name_Input then
+ if Async_Readers_Enabled (Item_Id) then
+ Property_Error (Item_Id, Name_Async_Readers);
+
+ elsif Effective_Reads_Enabled (Item_Id) then
+ Property_Error (Item_Id, Name_Effective_Reads);
+
+ elsif Effective_Writes_Enabled (Item_Id) then
+ Property_Error (Item_Id, Name_Effective_Writes);
+ end if;
+
+ elsif Global_Mode = Name_Output
+ and then Async_Writers_Enabled (Item_Id)
+ then
+ Error_Msg_Name_1 := Name_Async_Writers;
+ Error_Msg_NE
+ ("external state & with enabled property % must have "
+ & "mode Input or In_Out (SPARK RM 7.1.2(7))",
+ Item, Item_Id);
+ end if;
+
-- Variable related checks
else
procedure Resolve_Actuals (N : Node_Id; Nam : Entity_Id) is
Loc : constant Source_Ptr := Sloc (N);
A : Node_Id;
- F : Entity_Id;
+ A_Id : Entity_Id;
A_Typ : Entity_Id;
+ F : Entity_Id;
F_Typ : Entity_Id;
Prev : Node_Id := Empty;
Orig_A : Node_Id;
-- an instance of the default expression. The insertion is always
-- a named association.
+ procedure Property_Error
+ (Var : Node_Id;
+ Var_Id : Entity_Id;
+ Prop_Nam : Name_Id);
+ -- Emit an error concerning variable Var with entity Var_Id that has
+ -- enabled property Prop_Nam when it acts as an actual parameter in a
+ -- call and the corresponding formal parameter is of mode IN.
+
function Same_Ancestor (T1, T2 : Entity_Id) return Boolean;
-- Check whether T1 and T2, or their full views, are derived from a
-- common type. Used to enforce the restrictions on array conversions
Prev := Actval;
end Insert_Default;
+ --------------------
+ -- Property_Error --
+ --------------------
+
+ procedure Property_Error
+ (Var : Node_Id;
+ Var_Id : Entity_Id;
+ Prop_Nam : Name_Id)
+ is
+ begin
+ Error_Msg_Name_1 := Prop_Nam;
+ Error_Msg_NE
+ ("external variable & with enabled property % cannot appear as "
+ & "actual in procedure call (SPARK RM 7.1.3(11))", Var, Var_Id);
+ Error_Msg_N ("\\corresponding formal parameter has mode In", Var);
+ end Property_Error;
+
-------------------
-- Same_Ancestor --
-------------------
("volatile object cannot act as actual in a call (SPARK "
& "RM 7.1.3(12))", A);
end if;
+
+ -- Detect an external variable with an enabled property that
+ -- does not match the mode of the corresponding formal in a
+ -- procedure call.
+
+ -- why only procedure calls ???
+
+ if Ekind (Nam) = E_Procedure
+ and then Is_Entity_Name (A)
+ and then Present (Entity (A))
+ and then Ekind (Entity (A)) = E_Variable
+ then
+ A_Id := Entity (A);
+
+ if Ekind (F) = E_In_Parameter then
+ if Async_Readers_Enabled (A_Id) then
+ Property_Error (A, A_Id, Name_Async_Readers);
+ elsif Effective_Reads_Enabled (A_Id) then
+ Property_Error (A, A_Id, Name_Effective_Reads);
+ elsif Effective_Writes_Enabled (A_Id) then
+ Property_Error (A, A_Id, Name_Effective_Writes);
+ end if;
+
+ elsif Ekind (F) = E_Out_Parameter
+ and then Async_Writers_Enabled (A_Id)
+ then
+ Error_Msg_Name_1 := Name_Async_Writers;
+ Error_Msg_NE
+ ("external variable & with enabled property % cannot "
+ & "appear as actual in procedure call (SPARK RM "
+ & "7.1.3(11))", A, A_Id);
+ Error_Msg_N
+ ("\\corresponding formal parameter has mode Out", A);
+ end if;
+ end if;
end if;
Next_Actual (A);
function Has_Enabled_Property
(State_Id : Node_Id;
- Prop_Nam : Name_Id) return Boolean;
+ Property : Name_Id) return Boolean;
-- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
-- Determine whether an abstract state denoted by its entity State_Id has
- -- enabled property Prop_Name.
+ -- enabled property Property.
function Has_Null_Extension (T : Entity_Id) return Boolean;
-- T is a derived tagged type. Check whether the type extension is null.
function Has_Enabled_Property
(State_Id : Node_Id;
- Prop_Nam : Name_Id) return Boolean
+ Property : Name_Id) return Boolean
is
- Decl : constant Node_Id := Parent (State_Id);
- Opt : Node_Id;
- Opt_Nam : Node_Id;
- Prop : Node_Id;
- Props : Node_Id;
+ Decl : constant Node_Id := Parent (State_Id);
+ Opt : Node_Id;
+ Opt_Nam : Node_Id;
+ Prop : Node_Id;
+ Prop_Nam : Node_Id;
+ Props : Node_Id;
begin
-- The declaration of an external abstract state appears as an extension
Prop := First (Expressions (Props));
while Present (Prop) loop
- if Chars (Prop) = Prop_Nam then
+ if Chars (Prop) = Property then
return True;
end if;
Prop := First (Component_Associations (Props));
while Present (Prop) loop
- if Chars (Prop) = Prop_Nam then
+ Prop_Nam := First (Choices (Prop));
+
+ if Chars (Prop_Nam) = Property then
return Is_True (Expr_Value (Expression (Prop)));
end if;
-- Single property
else
- return Chars (Props) = Prop_Nam;
+ return Chars (Props) = Property;
end if;
end if;
(Node : Node_Id;
Default : Node_Id);
-- Print the end label for a Handled_Sequence_Of_Statements in a body.
- -- If there is not end label, use the defining identifier of the enclosing
+ -- If there is no end label, use the defining identifier of the enclosing
-- construct. If the end label is present, treat it as a reference to the
-- defining entity of the construct: this guarantees that it carries the
-- proper sloc information for debugging purposes.