+2016-04-27 Bob Duff <duff@adacore.com>
+
+ * a-coinve.adb, a-comutr.adb, a-conhel.adb, a-convec.adb,
+ exp_util.adb: Remove assertions that can fail in obscure cases when
+ assertions are turned on but tampering checks are turned off.
+
+2016-04-27 Javier Miranda <miranda@adacore.com>
+
+ * exp_ch6.adb (Add_Call_By_Copy_Code,
+ Add_Simple_Call_By_Copy_Code, Expand_Actuals): Handle formals
+ whose type comes from the limited view.
+
+2016-04-27 Yannick Moy <moy@adacore.com>
+
+ * a-textio.adb: Complete previous patch.
+
+2016-04-27 Yannick Moy <moy@adacore.com>
+
+ * inline.adb (Expand_Inlined_Call): Use Cannot_Inline instead of
+ Error_Msg_N to issue message about impossibility to inline call,
+ with slight change of message.
+
+2016-04-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_spark.adb (Expand_Potential_Renaming): Removed.
+ (Expand_SPARK): Update the call to expand a potential renaming.
+ (Expand_SPARK_Potential_Renaming): New routine.
+ * exp_spark.ads (Expand_SPARK_Potential_Renaming): New routine.
+ * sem.adb Add with and use clauses for Exp_SPARK.
+ (Analyze): Expand a non-overloaded potential renaming for SPARK.
+
+2016-04-27 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch3.adb (Constrain_Discriminated_Type): In an instance,
+ check full view for the presence of defaulted discriminants,
+ even when the partial view of a private type has no visible and
+ no unknown discriminants.
+
2016-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* lib-xref.adb, exp_ch3.adb: Minor reformatting.
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
end Finalize;
procedure Finalize (Object : in out Iterator) is
- pragma Warnings (Off);
- pragma Assert (T_Check); -- not called if check suppressed
- pragma Warnings (On);
begin
Unbusy (Object.Container.TC);
end Finalize;
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
record
Container : Tree_Access;
Subtree : Tree_Node_Access;
- end record;
+ end record
+ with Disable_Controlled => not T_Check;
overriding procedure Finalize (Object : in out Root_Iterator);
---------------------
type Child_Iterator is new Root_Iterator and
- Tree_Iterator_Interfaces.Reversible_Iterator with null record;
+ Tree_Iterator_Interfaces.Reversible_Iterator with null record
+ with Disable_Controlled => not T_Check;
overriding function First (Object : Child_Iterator) return Cursor;
-- --
-- B o d y --
-- --
--- Copyright (C) 2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2015-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
------------
procedure Adjust (Control : in out Reference_Control_Type) is
- pragma Warnings (Off);
- -- GNAT warns here if checks are turned off, but assertions on
- pragma Assert (T_Check); -- not called if check suppressed
- pragma Warnings (On);
begin
if Control.T_Counts /= null then
Lock (Control.T_Counts.all);
--------------
procedure Finalize (Control : in out Reference_Control_Type) is
- pragma Warnings (Off);
- pragma Assert (T_Check); -- not called if check suppressed
- pragma Warnings (On);
begin
if Control.T_Counts /= null then
Unlock (Control.T_Counts.all);
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
end Finalize;
procedure Finalize (Object : in out Iterator) is
- pragma Warnings (Off);
- pragma Assert (T_Check); -- not called if check suppressed
- pragma Warnings (On);
begin
Unbusy (Object.Container.TC);
end Finalize;
function Get_Rest (S : String) return String is
- -- Each time we allocate a buffer the same size as what we have
- -- read so far. This limits us to a logarithmic number of calls
- -- to Get_Rest and also ensures only a linear use of stack space.
+ -- The first time we allocate a buffer of size 500. Each following
+ -- time we allocate a buffer the same size as what we have read so
+ -- far. This limits us to a logarithmic number of calls to Get_Rest
+ -- and also ensures only a linear use of stack space.
- Buffer : String (1 .. S'Length);
+ Buffer : String (1 .. Integer'Max (500, S'Length));
Last : Natural;
begin
return R;
else
- return Get_Rest (R);
+ pragma Assert (Last = Buffer'Last);
+
+ -- If the String has the same length as the buffer, and there
+ -- is no end of line, check whether we are at the end of file,
+ -- in which case we have the full String in the buffer.
+
+ if End_Of_File (File) then
+ return R;
+
+ else
+ return Get_Rest (R);
+ end if;
end if;
end;
end Get_Rest;
- -- Local variables
-
- Buffer : String (1 .. 500);
- ch : int;
- Last : Natural;
-
-- Start of processing for Get_Line
begin
- Get_Line (File, Buffer, Last);
-
- if Last < Buffer'Last then
- return Buffer (1 .. Last);
-
- -- If the String has the same length as the buffer, and there is no end
- -- of line, check whether we are at the end of file, in which case we
- -- have the full String in the buffer.
-
- elsif Last = Buffer'Last then
- ch := Getc (File);
-
- if ch = EOF then
- return Buffer;
-
- else
- Ungetc (ch, File);
- return Get_Rest (Buffer (1 .. Last));
- end if;
-
- else
- return Get_Rest (Buffer (1 .. Last));
- end if;
+ return Get_Rest ("");
end Get_Line;
function Get_Line return String is
---------------------------
procedure Add_Call_By_Copy_Code is
+ Crep : Boolean;
Expr : Node_Id;
+ F_Typ : Entity_Id := Etype (Formal);
+ Indic : Node_Id;
Init : Node_Id;
Temp : Entity_Id;
- Indic : Node_Id;
- Var : Entity_Id;
- F_Typ : constant Entity_Id := Etype (Formal);
V_Typ : Entity_Id;
- Crep : Boolean;
+ Var : Entity_Id;
begin
if not Is_Legal_Copy then
Temp := Make_Temporary (Loc, 'T', Actual);
+ -- Handle formals whose type comes from the limited view
+
+ if From_Limited_With (F_Typ)
+ and then Has_Non_Limited_View (F_Typ)
+ then
+ F_Typ := Non_Limited_View (F_Typ);
+ end if;
+
-- Use formal type for temp, unless formal type is an unconstrained
-- array, in which case we don't have to worry about bounds checks,
-- and we use the actual type, since that has appropriate bounds.
if Is_Array_Type (F_Typ) and then not Is_Constrained (F_Typ) then
Indic := New_Occurrence_Of (Etype (Actual), Loc);
else
- Indic := New_Occurrence_Of (Etype (Formal), Loc);
+ Indic := New_Occurrence_Of (F_Typ, Loc);
end if;
if Nkind (Actual) = N_Type_Conversion then
----------------------------------
procedure Add_Simple_Call_By_Copy_Code is
- Temp : Entity_Id;
Decl : Node_Id;
+ F_Typ : Entity_Id := Etype (Formal);
Incod : Node_Id;
- Outcod : Node_Id;
+ Indic : Node_Id;
Lhs : Node_Id;
+ Outcod : Node_Id;
Rhs : Node_Id;
- Indic : Node_Id;
- F_Typ : constant Entity_Id := Etype (Formal);
+ Temp : Entity_Id;
begin
if not Is_Legal_Copy then
return;
end if;
+ -- Handle formals whose type comes from the limited view
+
+ if From_Limited_With (F_Typ)
+ and then Has_Non_Limited_View (F_Typ)
+ then
+ F_Typ := Non_Limited_View (F_Typ);
+ end if;
+
-- Use formal type for temp, unless formal type is an unconstrained
-- array, in which case we don't have to worry about bounds checks,
-- and we use the actual type, since that has appropriate bounds.
if Is_Array_Type (F_Typ) and then not Is_Constrained (F_Typ) then
Indic := New_Occurrence_Of (Etype (Actual), Loc);
else
- Indic := New_Occurrence_Of (Etype (Formal), Loc);
+ Indic := New_Occurrence_Of (F_Typ, Loc);
end if;
-- Prepare to generate code
if Ekind (Formal) = E_Out_Parameter then
Incod := Empty;
- if Has_Discriminants (Etype (Formal)) then
+ if Has_Discriminants (F_Typ) then
Indic := New_Occurrence_Of (Etype (Actual), Loc);
end if;
E_Formal := Etype (Formal);
E_Actual := Etype (Actual);
+ -- Handle formals whose type comes from the limited view
+
+ if From_Limited_With (E_Formal)
+ and then Has_Non_Limited_View (E_Formal)
+ then
+ E_Formal := Non_Limited_View (E_Formal);
+ end if;
+
if Is_Scalar_Type (E_Formal)
or else Nkind (Actual) = N_Slice
then
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
-- Perform name evaluation for a renamed object
- procedure Expand_Potential_Renaming (N : Node_Id);
- -- N denotes a N_Identifier or N_Expanded_Name. If N references a renaming,
- -- replace N with the renamed object.
-
------------------
-- Expand_SPARK --
------------------
when N_Expanded_Name |
N_Identifier =>
- Expand_Potential_Renaming (N);
+ Expand_SPARK_Potential_Renaming (N);
when N_Object_Renaming_Declaration =>
Expand_SPARK_N_Object_Renaming_Declaration (N);
Evaluate_Name (Name (N));
end Expand_SPARK_N_Object_Renaming_Declaration;
- -------------------------------
- -- Expand_Potential_Renaming --
- -------------------------------
+ -------------------------------------
+ -- Expand_SPARK_Potential_Renaming --
+ -------------------------------------
- procedure Expand_Potential_Renaming (N : Node_Id) is
- Id : constant Entity_Id := Entity (N);
+ procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N);
+ Ren_Id : constant Entity_Id := Entity (N);
Typ : constant Entity_Id := Etype (N);
- Ren_Id : Node_Id;
+ Obj_Id : Node_Id;
begin
-- Replace a reference to a renaming with the actual renamed object
- if Ekind (Id) in Object_Kind then
- Ren_Id := Renamed_Object (Id);
+ if Ekind (Ren_Id) in Object_Kind then
+ Obj_Id := Renamed_Object (Ren_Id);
- if Present (Ren_Id) then
+ if Present (Obj_Id) then
-- The renamed object is an entity when instantiating generics
-- or inlining bodies. In this case the renaming is part of the
-- mapping "prologue" which links actuals to formals.
- if Nkind (Ren_Id) in N_Entity then
- Rewrite (N, New_Occurrence_Of (Ren_Id, Loc));
+ if Nkind (Obj_Id) in N_Entity then
+ Rewrite (N, New_Occurrence_Of (Obj_Id, Loc));
-- Otherwise the renamed object denotes a name
else
- Rewrite (N, New_Copy_Tree (Ren_Id));
+ Rewrite (N, New_Copy_Tree (Obj_Id));
Reset_Analyzed_Flags (N);
end if;
Analyze_And_Resolve (N, Typ);
end if;
end if;
- end Expand_Potential_Renaming;
+ end Expand_SPARK_Potential_Renaming;
end Exp_SPARK;
-- --
-- S p e c --
-- --
--- Copyright (C) 2011-2013, Free Software Foundation, Inc. --
+-- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
procedure Expand_SPARK (N : Node_Id);
+ procedure Expand_SPARK_Potential_Renaming (N : Node_Id);
+ -- N must denote an N_Expanded_Name or N_Identifier. If N is a reference to
+ -- a renaming, replace N with the renamed object.
+
end Exp_SPARK;
elsif Disable_Controlled (T) then
return False;
+ elsif Is_Class_Wide_Type (T) and then Disable_Controlled (Etype (T)) then
+ return False;
+
else
-- Class-wide types are treated as controlled because derivations
-- from the root type can introduce controlled components.
-- subprograms this must be done explicitly.
if In_Open_Scopes (Subp) then
- Error_Msg_N ("call to recursive subprogram cannot be inlined??", N);
+ Cannot_Inline
+ ("cannot inline call to recursive subprogram?", N, Subp);
Set_Is_Inlined (Subp, False);
-
- -- In GNATprove mode, issue a warning, and indicate that the
- -- subprogram is not always inlined by setting flag Is_Inlined_Always
- -- to False.
-
- if GNATprove_Mode then
- Set_Is_Inlined_Always (Subp, False);
- end if;
-
return;
-- Skip inlining if this is not a true inlining since the attribute
elsif Is_Unc
and then
- Nkind (First (Statements (Handled_Statement_Sequence (Orig_Bod))))
- = N_Extended_Return_Statement
+ Nkind (First (Statements (Handled_Statement_Sequence (Orig_Bod)))) =
+ N_Extended_Return_Statement
and then not Back_End_Inlining
then
return;
-- --
------------------------------------------------------------------------------
-with Atree; use Atree;
-with Debug; use Debug;
-with Debug_A; use Debug_A;
-with Elists; use Elists;
-with Expander; use Expander;
-with Fname; use Fname;
-with Ghost; use Ghost;
-with Lib; use Lib;
-with Lib.Load; use Lib.Load;
-with Nlists; use Nlists;
-with Output; use Output;
-with Restrict; use Restrict;
-with Sem_Attr; use Sem_Attr;
-with Sem_Aux; use Sem_Aux;
-with Sem_Ch2; use Sem_Ch2;
-with Sem_Ch3; use Sem_Ch3;
-with Sem_Ch4; use Sem_Ch4;
-with Sem_Ch5; use Sem_Ch5;
-with Sem_Ch6; use Sem_Ch6;
-with Sem_Ch7; use Sem_Ch7;
-with Sem_Ch8; use Sem_Ch8;
-with Sem_Ch9; use Sem_Ch9;
-with Sem_Ch10; use Sem_Ch10;
-with Sem_Ch11; use Sem_Ch11;
-with Sem_Ch12; use Sem_Ch12;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Prag; use Sem_Prag;
-with Sem_Util; use Sem_Util;
-with Sinfo; use Sinfo;
-with Stand; use Stand;
-with Stylesw; use Stylesw;
-with Uintp; use Uintp;
-with Uname; use Uname;
+with Atree; use Atree;
+with Debug; use Debug;
+with Debug_A; use Debug_A;
+with Elists; use Elists;
+with Exp_SPARK; use Exp_SPARK;
+with Expander; use Expander;
+with Fname; use Fname;
+with Ghost; use Ghost;
+with Lib; use Lib;
+with Lib.Load; use Lib.Load;
+with Nlists; use Nlists;
+with Output; use Output;
+with Restrict; use Restrict;
+with Sem_Attr; use Sem_Attr;
+with Sem_Aux; use Sem_Aux;
+with Sem_Ch2; use Sem_Ch2;
+with Sem_Ch3; use Sem_Ch3;
+with Sem_Ch4; use Sem_Ch4;
+with Sem_Ch5; use Sem_Ch5;
+with Sem_Ch6; use Sem_Ch6;
+with Sem_Ch7; use Sem_Ch7;
+with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch9; use Sem_Ch9;
+with Sem_Ch10; use Sem_Ch10;
+with Sem_Ch11; use Sem_Ch11;
+with Sem_Ch12; use Sem_Ch12;
+with Sem_Ch13; use Sem_Ch13;
+with Sem_Prag; use Sem_Prag;
+with Sem_Util; use Sem_Util;
+with Sinfo; use Sinfo;
+with Stand; use Stand;
+with Stylesw; use Stylesw;
+with Uintp; use Uintp;
+with Uname; use Uname;
with Unchecked_Deallocation;
and then Etype (N) = Standard_Void_Type)
then
Expand (N);
+
+ -- Replace a reference to a renaming with the renamed object for SPARK.
+ -- In general this modification is performed by Expand_SPARK, however
+ -- certain constructs may not reach the resolution or expansion phase
+ -- and thus remain unchanged. The replacement is not performed when the
+ -- construct is overloaded as resolution must first take place. This is
+ -- also not done when analyzing a generic to preserve the original tree
+ -- and because the reference may become overloaded in the instance.
+
+ elsif GNATprove_Mode
+ and then Nkind_In (N, N_Expanded_Name, N_Identifier)
+ and then not Is_Overloaded (N)
+ and then not Inside_A_Generic
+ then
+ Expand_SPARK_Potential_Renaming (N);
end if;
Ghost_Mode := Save_Ghost_Mode;
Related_Nod : Node_Id;
For_Access : Boolean := False)
is
- E : constant Entity_Id := Entity (Subtype_Mark (S));
+ E : Entity_Id := Entity (Subtype_Mark (S));
T : Entity_Id;
C : Node_Id;
Elist : Elist_Id := New_Elmt_List;
end if;
-- In an instance it may be necessary to retrieve the full view of a
- -- type with unknown discriminants. In other contexts the constraint
- -- is illegal.
+ -- type with unknown discriminants, or a full view with defaulted
+ -- discriminants. In other contexts the constraint is illegal.
if In_Instance
and then Is_Private_Type (T)
- and then Has_Unknown_Discriminants (T)
and then Present (Full_View (T))
+ and then
+ (Has_Unknown_Discriminants (T)
+ or else (not Has_Discriminants (T)
+ and then Has_Discriminants (Full_View (T))
+ and then Present
+ (Discriminant_Default_Value
+ (First_Discriminant (Full_View (T))))))
then
T := Full_View (T);
+ E := Full_View (E);
end if;
-- Ada 2005 (AI-412): Constrained incomplete subtypes are illegal.
May_Have_Null_Exclusion : Boolean;
- procedure Check_Incomplete (T : Entity_Id);
+ procedure Check_Incomplete (T : Node_Id);
-- Called to verify that an incomplete type is not used prematurely
----------------------
-- Check_Incomplete --
----------------------
- procedure Check_Incomplete (T : Entity_Id) is
+ procedure Check_Incomplete (T : Node_Id) is
begin
-- Ada 2005 (AI-412): Incomplete subtypes are legal