+2009-04-10 Robert Dewar <dewar@adacore.com>
+
+ * gnat_rm.texi: Document that postconditions are tested on implicit
+ returns.
+
+ * sem_aux.adb: Minor reformatting
+
+2009-04-10 Gary Dismukes <dismukes@adacore.com>
+
+ * itypes.adb (Create_Null_Excluding_Itype): Apply Base_Type when
+ setting Etype.
+
+ * par-ch3.adb (P_Access_Type_Definition): Set new attribute
+ Null_Exclusion_In_Return_Present when an access-to-function type has a
+ result type with an explicit not null.
+
+ * sem_ch3.adb (Access_Subprogram_Definition): If a null exclusion is
+ given on the result type, then create a null-excluding itype for the
+ function.
+
+ * sem_ch6.adb (Analyze_Return_Type): Create a null-excluding itype in
+ the case where a null exclusion is imposed on a named access type.
+ (Analyze_Subprogram_Specification): Push and pop the scope of the
+ function around the call to Analyze_Return_Type in the case of no
+ formals, for consistency with handling when formals are present
+ (Process_Formals does this). Ensures that any itype created for the
+ return type will be associated with the proper scope.
+
+ * sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): If a null
+ exclusion is given on a generic function's result type, then create a
+ null-excluding itype for the generic function.
+ (Instantiate_Object): Set Null_Exclusion_Present of a constant created
+ for an actual for a formal in object according to the setting on the
+ formal. Ensures null exclusion checks are done when the association is
+ elaborated.
+
+ * sinfo.ads: Add new flag Null_Exclusion_In_Return_Present on
+ N_Access_Function_Definition.
+
+ * sinfo.adb: Add Get_ and Set_ operations for
+ Null_Exclusion_In_Return_Present.
+
2009-04-10 Bob Duff <duff@adacore.com>
* exp_ch5.adb, exp_ch6.adb, sem_ch6.adb: Move the code that creates a
The @code{Postcondition} pragma allows specification of automatic
postcondition checks for subprograms. These checks are similar to
assertions, but are automatically inserted just prior to the return
-statements of the subprogram with which they are associated.
-Furthermore, the boolean expression which is the condition which
+statements of the subprogram with which they are associated (including
+implicit returns at the end of procedure bodies and associated
+exception handlers).
+
+In addition, the boolean expression which is the condition which
must be true may contain references to function'Result in the case
of a function to refer to the returned value.
Scope_Id => Scope_Id);
Set_Directly_Designated_Type (I_Typ, Directly_Designated_Type (T));
- Set_Etype (I_Typ, T);
+ Set_Etype (I_Typ, Base_Type (T));
Set_Depends_On_Private (I_Typ, Depends_On_Private (T));
Set_Is_Public (I_Typ, Is_Public (T));
Set_From_With_Type (I_Typ, From_With_Type (T));
else
Result_Node := P_Subtype_Mark;
No_Constraint;
- end if;
- -- Note: A null exclusion given on the result type needs to
- -- be coded by a distinct flag, since Null_Exclusion_Present
- -- on an access-to-function type pertains to a null exclusion
- -- on the access type itself (as set above). ???
- -- Set_Null_Exclusion_Present??? (Type_Def_Node, Result_Not_Null);
+ -- A null exclusion on the result type must be recorded in a flag
+ -- distinct from the one used for the access-to-subprogram type's
+ -- null exclusion.
+
+ Set_Null_Exclusion_In_Return_Present
+ (Type_Def_Node, Result_Not_Null);
+ end if;
Set_Result_Definition (Type_Def_Node, Result_Node);
return Renamed_Object (Ent);
-- If this is a component declaration whose entity is constant, it is
- -- a prival within a protected function. It does not have a constant
- -- value.
+ -- a prival within a protected function (and so has no constant value).
elsif Nkind (D) = N_Component_Declaration then
return Empty;
with Fname.UF; use Fname.UF;
with Freeze; use Freeze;
with Hostparm;
+with Itypes; use Itypes;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
with Lib.Xref; use Lib.Xref;
New_N : Node_Id;
Result_Type : Entity_Id;
Save_Parent : Node_Id;
+ Typ : Entity_Id;
begin
-- Create copy of generic unit, and save for instantiation. If the unit
Set_Etype (Id, Result_Type);
else
Find_Type (Result_Definition (Spec));
- Set_Etype (Id, Entity (Result_Definition (Spec)));
+ Typ := Entity (Result_Definition (Spec));
+
+ -- If a null exclusion is imposed on the result type, then create
+ -- a null-excluding itype (an access subtype) and use it as the
+ -- function's Etype.
+
+ if Is_Access_Type (Typ)
+ and then Null_Exclusion_Present (Spec)
+ then
+ Set_Etype (Id,
+ Create_Null_Excluding_Itype
+ (T => Typ,
+ Related_Nod => Spec,
+ Scope_Id => Defining_Unit_Name (Spec)));
+ else
+ Set_Etype (Id, Typ);
+ end if;
end if;
else
Decl_Node :=
Make_Object_Declaration (Loc,
- Defining_Identifier => New_Copy (Formal_Id),
- Constant_Present => True,
- Object_Definition => New_Copy_Tree (Def),
- Expression => Actual);
+ Defining_Identifier => New_Copy (Formal_Id),
+ Constant_Present => True,
+ Null_Exclusion_Present => Null_Exclusion_Present (Formal),
+ Object_Definition => New_Copy_Tree (Def),
+ Expression => Actual);
Set_Corresponding_Generic_Association (Decl_Node, Act_Assoc);
Decl_Node :=
Make_Object_Declaration (Sloc (Formal),
- Defining_Identifier => New_Copy (Formal_Id),
- Constant_Present => True,
- Object_Definition => New_Copy (Def),
- Expression => New_Copy_Tree
- (Default_Expression (Formal)));
+ Defining_Identifier => New_Copy (Formal_Id),
+ Constant_Present => True,
+ Null_Exclusion_Present => Null_Exclusion_Present (Formal),
+ Object_Definition => New_Copy (Def),
+ Expression => New_Copy_Tree
+ (Default_Expression (Formal)));
Append (Decl_Node, List);
Set_Analyzed (Expression (Decl_Node), False);
Decl_Node :=
Make_Object_Declaration (Loc,
- Defining_Identifier => New_Copy (Formal_Id),
- Constant_Present => True,
- Object_Definition => New_Copy (Def),
- Expression =>
+ Defining_Identifier => New_Copy (Formal_Id),
+ Constant_Present => True,
+ Null_Exclusion_Present => Null_Exclusion_Present (Formal),
+ Object_Definition => New_Copy (Def),
+ Expression =>
Make_Attribute_Reference (Sloc (Formal_Id),
Attribute_Name => Name_First,
Prefix => New_Copy (Def)));
else
Analyze (Result_Definition (T_Def));
- Set_Etype (Desig_Type, Entity (Result_Definition (T_Def)));
+
+ declare
+ Typ : constant Entity_Id := Entity (Result_Definition (T_Def));
+
+ begin
+ -- If a null exclusion is imposed on the result type, then
+ -- create a null-excluding itype (an access subtype) and use
+ -- it as the function's Etype.
+
+ if Is_Access_Type (Typ)
+ and then Null_Exclusion_In_Return_Present (T_Def)
+ then
+ Set_Etype (Desig_Type,
+ Create_Null_Excluding_Itype
+ (T => Typ,
+ Related_Nod => T_Def,
+ Scope_Id => Current_Scope));
+ else
+ Set_Etype (Desig_Type, Typ);
+ end if;
+ end;
end if;
if not (Is_Type (Etype (Desig_Type))) then
Set_Is_Local_Anonymous_Access (Typ);
Set_Etype (Designator, Typ);
+ -- Ada 2005 (AI-231): Ensure proper usage of null exclusion
+
+ Null_Exclusion_Static_Checks (N);
+
-- Subtype_Mark case
else
Typ := Entity (Result_Definition (N));
Set_Etype (Designator, Typ);
+ -- Ada 2005 (AI-231): Ensure proper usage of null exclusion
+
+ Null_Exclusion_Static_Checks (N);
+
+ -- If a null exclusion is imposed on the result type, then create
+ -- a null-excluding itype (an access subtype) and use it as the
+ -- function's Etype. Note that the null exclusion checks are done
+ -- right before this, because they don't get applied to types that
+ -- do not come from source.
+
+ if Is_Access_Type (Typ)
+ and then Null_Exclusion_Present (N)
+ then
+ Set_Etype (Designator,
+ Create_Null_Excluding_Itype
+ (T => Typ,
+ Related_Nod => N,
+ Scope_Id => Scope (Current_Scope)));
+ else
+ Set_Etype (Designator, Typ);
+ end if;
+
if Ekind (Typ) = E_Incomplete_Type
and then Is_Value_Type (Typ)
then
end if;
end if;
- -- Ada 2005 (AI-231): Ensure proper usage of null exclusion
-
- Null_Exclusion_Static_Checks (N);
-
-- Case where result definition does indicate an error
else
End_Scope;
+ -- The subprogram scope is pushed and popped around the processing of
+ -- the return type for consistency with call above to Process_Formals
+ -- (which itself can call Analyze_Return_Type), and to ensure that any
+ -- itype created for the return type will be associated with the proper
+ -- scope.
+
elsif Nkind (N) = N_Function_Specification then
+ Push_Scope (Designator);
+
Analyze_Return_Type (N);
+
+ End_Scope;
end if;
if Nkind (N) = N_Function_Specification then
return Flag11 (N);
end Null_Exclusion_Present;
+ function Null_Exclusion_In_Return_Present
+ (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Access_Function_Definition);
+ return Flag14 (N);
+ end Null_Exclusion_In_Return_Present;
+
function Null_Record_Present
(N : Node_Id) return Boolean is
begin
Set_Flag11 (N, Val);
end Set_Null_Exclusion_Present;
+ procedure Set_Null_Exclusion_In_Return_Present
+ (N : Node_Id; Val : Boolean := True) is
+ begin
+ pragma Assert (False
+ or else NT (N).Nkind = N_Access_Function_Definition);
+ Set_Flag14 (N, Val);
+ end Set_Null_Exclusion_In_Return_Present;
+
procedure Set_Null_Record_Present
(N : Node_Id; Val : Boolean := True) is
begin
-- N_Access_Function_Definition
-- Sloc points to ACCESS
-- Null_Exclusion_Present (Flag11)
+ -- Null_Exclusion_In_Return_Present (Flag14)
-- Protected_Present (Flag6)
-- Parameter_Specifications (List3) (set to No_List if no formal part)
-- Result_Definition (Node4) result subtype (subtype mark or access def)
function Null_Exclusion_Present
(N : Node_Id) return Boolean; -- Flag11
+ function Null_Exclusion_In_Return_Present
+ (N : Node_Id) return Boolean; -- Flag14
+
function Null_Record_Present
(N : Node_Id) return Boolean; -- Flag17
procedure Set_Null_Exclusion_Present
(N : Node_Id; Val : Boolean := True); -- Flag11
+ procedure Set_Null_Exclusion_In_Return_Present
+ (N : Node_Id; Val : Boolean := True); -- Flag14
+
procedure Set_Null_Record_Present
(N : Node_Id; Val : Boolean := True); -- Flag17
pragma Inline (No_Truncation);
pragma Inline (Null_Present);
pragma Inline (Null_Exclusion_Present);
+ pragma Inline (Null_Exclusion_In_Return_Present);
pragma Inline (Null_Record_Present);
pragma Inline (Object_Definition);
pragma Inline (Original_Discriminant);
pragma Inline (Set_No_Truncation);
pragma Inline (Set_Null_Present);
pragma Inline (Set_Null_Exclusion_Present);
+ pragma Inline (Set_Null_Exclusion_In_Return_Present);
pragma Inline (Set_Null_Record_Present);
pragma Inline (Set_Object_Definition);
pragma Inline (Set_Original_Discriminant);