[multiple changes]
2014-02-19 Ed Schonberg <schonberg@adacore.com> * sem_util.ads, sem_util.adb (Get_Cursor_Type): Moved to sem_util from sem_ch13, for use elsewhere. * sem_ch13.adb (Get_Cursor_Type): Moved to sem_util. * sem_ch5.adb (Analyze_Iterator_Specification): Set properly the cursor type on the loop variable when the iteration is over o formal container. 2014-02-19 Vincent Celier <celier@adacore.com> * prj-conf.adb (Add_Default_GNAT_Naming_Scheme): Add declaration for an empty Target (Check_Target): Never fail when an empty target is declared in the configuration project. 2014-02-19 Ed Schonberg <schonberg@adacore.com> * sem_prag.adb (Check_Arg_Is_Local_Name): Argument is local if the pragma comes fron a predicate aspect and the context is a record declaration within the scope that declares the type. 2014-02-19 Robert Dewar <dewar@adacore.com> * gnat_rm.texi: Minor clarifications. * expander.adb, sem_aggr.adb: Add comments. From-SVN: r207903
This commit is contained in:
Arnaud Charlet
parent
322913f876
commit
110e2969e0
|
|
@ -1,3 +1,29 @@
|
|||
2014-02-19 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_util.ads, sem_util.adb (Get_Cursor_Type): Moved to sem_util
|
||||
from sem_ch13, for use elsewhere.
|
||||
* sem_ch13.adb (Get_Cursor_Type): Moved to sem_util.
|
||||
* sem_ch5.adb (Analyze_Iterator_Specification): Set properly the
|
||||
cursor type on the loop variable when the iteration is over o
|
||||
formal container.
|
||||
|
||||
2014-02-19 Vincent Celier <celier@adacore.com>
|
||||
|
||||
* prj-conf.adb (Add_Default_GNAT_Naming_Scheme): Add declaration
|
||||
for an empty Target (Check_Target): Never fail when an empty
|
||||
target is declared in the configuration project.
|
||||
|
||||
2014-02-19 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_prag.adb (Check_Arg_Is_Local_Name): Argument is local if
|
||||
the pragma comes fron a predicate aspect and the context is a
|
||||
record declaration within the scope that declares the type.
|
||||
|
||||
2014-02-19 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* gnat_rm.texi: Minor clarifications.
|
||||
* expander.adb, sem_aggr.adb: Add comments.
|
||||
|
||||
2014-02-19 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_prag.adb (Check_Arg_Is_Local_Name): For an aspect that
|
||||
|
|
|
|||
|
|
@ -89,9 +89,12 @@ package body Expander is
|
|||
-- Full_Analysis flag indicates whether we are performing a complete
|
||||
-- analysis, in which case Full_Analysis = True or a pre-analysis in
|
||||
-- which case Full_Analysis = False. See the spec of Sem for more info
|
||||
-- on this. Additionally, the GNATprove_Mode flag indicates that a light
|
||||
-- on this.
|
||||
|
||||
-- Additionally, the GNATprove_Mode flag indicates that a light
|
||||
-- expansion for formal verification should be used. This expansion is
|
||||
-- never done inside generics.
|
||||
-- never done inside generics, because otherwise, this breaks the name
|
||||
-- resolution mechanism for generic instances
|
||||
|
||||
-- The second reason for the Expander_Active flag to be False is that
|
||||
-- we are performing a pre-analysis. During pre-analysis all expansion
|
||||
|
|
|
|||
|
|
@ -17523,8 +17523,12 @@ is specifically authorized by the Ada Reference Manual
|
|||
This child of @code{Ada.Containers} defines a modified version of the
|
||||
Ada 2005 container for doubly linked lists, meant to facilitate formal
|
||||
verification of code using such containers. The specification of this
|
||||
unit is compatible with SPARK 2014. Note that the API of this unit may
|
||||
be subject to incompatible changes as SPARK 2014 evolves.
|
||||
unit is compatible with SPARK 2014.
|
||||
|
||||
Note that although this container was designed with formal verification
|
||||
in mind, it may well be generally useful in that it is a simplified more
|
||||
efficient version than the one defined in the standard. In particular it
|
||||
does not have the complex overhead required to detect cursor tampering.
|
||||
|
||||
@node Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads)
|
||||
@section @code{Ada.Containers.Formal_Hashed_Maps} (@file{a-cfhama.ads})
|
||||
|
|
@ -17535,8 +17539,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
|
|||
This child of @code{Ada.Containers} defines a modified version of the
|
||||
Ada 2005 container for hashed maps, meant to facilitate formal
|
||||
verification of code using such containers. The specification of this
|
||||
unit is compatible with SPARK 2014. Note that the API of this unit may
|
||||
be subject to incompatible changes as SPARK 2014 evolves.
|
||||
unit is compatible with SPARK 2014.
|
||||
|
||||
Note that although this container was designed with formal verification
|
||||
in mind, it may well be generally useful in that it is a simplified more
|
||||
efficient version than the one defined in the standard. In particular it
|
||||
does not have the complex overhead required to detect cursor tampering.
|
||||
|
||||
@node Ada.Containers.Formal_Hashed_Sets (a-cfhase.ads)
|
||||
@section @code{Ada.Containers.Formal_Hashed_Sets} (@file{a-cfhase.ads})
|
||||
|
|
@ -17547,8 +17555,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
|
|||
This child of @code{Ada.Containers} defines a modified version of the
|
||||
Ada 2005 container for hashed sets, meant to facilitate formal
|
||||
verification of code using such containers. The specification of this
|
||||
unit is compatible with SPARK 2014. Note that the API of this unit may
|
||||
be subject to incompatible changes as SPARK 2014 evolves.
|
||||
unit is compatible with SPARK 2014.
|
||||
|
||||
Note that although this container was designed with formal verification
|
||||
in mind, it may well be generally useful in that it is a simplified more
|
||||
efficient version than the one defined in the standard. In particular it
|
||||
does not have the complex overhead required to detect cursor tampering.
|
||||
|
||||
@node Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)
|
||||
@section @code{Ada.Containers.Formal_Ordered_Maps} (@file{a-cforma.ads})
|
||||
|
|
@ -17559,8 +17571,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
|
|||
This child of @code{Ada.Containers} defines a modified version of the
|
||||
Ada 2005 container for ordered maps, meant to facilitate formal
|
||||
verification of code using such containers. The specification of this
|
||||
unit is compatible with SPARK 2014. Note that the API of this unit may
|
||||
be subject to incompatible changes as SPARK 2014 evolves.
|
||||
unit is compatible with SPARK 2014.
|
||||
|
||||
Note that although this container was designed with formal verification
|
||||
in mind, it may well be generally useful in that it is a simplified more
|
||||
efficient version than the one defined in the standard. In particular it
|
||||
does not have the complex overhead required to detect cursor tampering.
|
||||
|
||||
@node Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)
|
||||
@section @code{Ada.Containers.Formal_Ordered_Sets} (@file{a-cforse.ads})
|
||||
|
|
@ -17571,8 +17587,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
|
|||
This child of @code{Ada.Containers} defines a modified version of the
|
||||
Ada 2005 container for ordered sets, meant to facilitate formal
|
||||
verification of code using such containers. The specification of this
|
||||
unit is compatible with SPARK 2014. Note that the API of this unit may
|
||||
be subject to incompatible changes as SPARK 2014 evolves.
|
||||
unit is compatible with SPARK 2014.
|
||||
|
||||
Note that although this container was designed with formal verification
|
||||
in mind, it may well be generally useful in that it is a simplified more
|
||||
efficient version than the one defined in the standard. In particular it
|
||||
does not have the complex overhead required to detect cursor tampering.
|
||||
|
||||
@node Ada.Containers.Formal_Vectors (a-cofove.ads)
|
||||
@section @code{Ada.Containers.Formal_Vectors} (@file{a-cofove.ads})
|
||||
|
|
@ -17583,8 +17603,12 @@ be subject to incompatible changes as SPARK 2014 evolves.
|
|||
This child of @code{Ada.Containers} defines a modified version of the
|
||||
Ada 2005 container for vectors, meant to facilitate formal
|
||||
verification of code using such containers. The specification of this
|
||||
unit is compatible with SPARK 2014. Note that the API of this unit may
|
||||
be subject to incompatible changes as SPARK 2014 evolves.
|
||||
unit is compatible with SPARK 2014.
|
||||
|
||||
Note that although this container was designed with formal verification
|
||||
in mind, it may well be generally useful in that it is a simplified more
|
||||
efficient version than the one defined in the standard. In particular it
|
||||
does not have the complex overhead required to detect cursor tampering.
|
||||
|
||||
@node Ada.Command_Line.Environment (a-colien.ads)
|
||||
@section @code{Ada.Command_Line.Environment} (@file{a-colien.ads})
|
||||
|
|
|
|||
|
|
@ -202,6 +202,10 @@ package body Prj.Conf is
|
|||
Create_Attribute (Name_Library_Auto_Init_Supported, "false");
|
||||
end if;
|
||||
|
||||
-- Declare an empty target
|
||||
|
||||
Create_Attribute (Name_Target, "");
|
||||
|
||||
-- Setup Ada support (Ada is the default language here, since this
|
||||
-- is only called when no config file existed initially, ie for
|
||||
-- gnatmake).
|
||||
|
|
@ -574,7 +578,8 @@ package body Prj.Conf is
|
|||
OK :=
|
||||
Target = ""
|
||||
or else (Tgt_Name /= No_Name
|
||||
and then Target = Get_Name_String (Tgt_Name));
|
||||
and then (Length_Of_Name (Tgt_Name) = 0
|
||||
or else Target = Get_Name_String (Tgt_Name)));
|
||||
|
||||
if not OK then
|
||||
if Autoconf_Specified then
|
||||
|
|
|
|||
|
|
@ -455,9 +455,12 @@ package body Sem_Aggr is
|
|||
end if;
|
||||
|
||||
-- This is really expansion activity, so make sure that expansion is
|
||||
-- on and is allowed. In GNATprove mode, we also want check flags to be
|
||||
-- added in the tree, so that the formal verification can rely on those
|
||||
-- to be present.
|
||||
-- on and is allowed. In GNATprove mode, we also want check flags to
|
||||
-- be added in the tree, so that the formal verification can rely on
|
||||
-- those to be present. In GNATprove mode for formal verification, some
|
||||
-- treatment typically only done during expansion needs to be performed
|
||||
-- on the tree, but it should not be applied inside generics. Otherwise,
|
||||
-- this breaks the name resolution mechanism for generic instances.
|
||||
|
||||
if not Expander_Active
|
||||
and (Inside_A_Generic or not Full_Analysis or not GNATprove_Mode)
|
||||
|
|
|
|||
|
|
@ -128,12 +128,6 @@ package body Sem_Ch13 is
|
|||
-- Uint value. If the value is inappropriate, then error messages are
|
||||
-- posted as required, and a value of No_Uint is returned.
|
||||
|
||||
function Get_Cursor_Type
|
||||
(Aspect : Node_Id;
|
||||
Typ : Entity_Id) return Entity_Id;
|
||||
-- Find Cursor type in scope of Typ, by locating primitive operation First.
|
||||
-- For use in resolving the other primitive operations of an Iterable type.
|
||||
|
||||
function Is_Operational_Item (N : Node_Id) return Boolean;
|
||||
-- A specification for a stream attribute is allowed before the full type
|
||||
-- is declared, as explained in AI-00137 and the corrigendum. Attributes
|
||||
|
|
@ -9756,81 +9750,6 @@ package body Sem_Ch13 is
|
|||
end if;
|
||||
end Get_Alignment_Value;
|
||||
|
||||
---------------------
|
||||
-- Get_Cursor_Type --
|
||||
---------------------
|
||||
|
||||
function Get_Cursor_Type
|
||||
(Aspect : Node_Id;
|
||||
Typ : Entity_Id) return Entity_Id
|
||||
is
|
||||
Assoc : Node_Id;
|
||||
Func : Entity_Id;
|
||||
First_Op : Entity_Id;
|
||||
Cursor : Entity_Id;
|
||||
|
||||
begin
|
||||
-- If error already detected, return
|
||||
|
||||
if Error_Posted (Aspect) then
|
||||
return Any_Type;
|
||||
end if;
|
||||
|
||||
-- The cursor type for an Iterable aspect is the return type of a
|
||||
-- non-overloaded First primitive operation. Locate association for
|
||||
-- First.
|
||||
|
||||
Assoc := First (Component_Associations (Expression (Aspect)));
|
||||
First_Op := Any_Id;
|
||||
while Present (Assoc) loop
|
||||
if Chars (First (Choices (Assoc))) = Name_First then
|
||||
First_Op := Expression (Assoc);
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Next (Assoc);
|
||||
end loop;
|
||||
|
||||
if First_Op = Any_Id then
|
||||
Error_Msg_N ("aspect Iterable must specify First operation", Aspect);
|
||||
return Any_Type;
|
||||
end if;
|
||||
|
||||
Cursor := Any_Type;
|
||||
|
||||
-- Locate function with desired name and profile in scope of type
|
||||
|
||||
Func := First_Entity (Scope (Typ));
|
||||
while Present (Func) loop
|
||||
if Chars (Func) = Chars (First_Op)
|
||||
and then Ekind (Func) = E_Function
|
||||
and then Present (First_Formal (Func))
|
||||
and then Etype (First_Formal (Func)) = Typ
|
||||
and then No (Next_Formal (First_Formal (Func)))
|
||||
then
|
||||
if Cursor /= Any_Type then
|
||||
Error_Msg_N
|
||||
("Operation First for iterable type must be unique", Aspect);
|
||||
return Any_Type;
|
||||
|
||||
else
|
||||
Cursor := Etype (Func);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next_Entity (Func);
|
||||
end loop;
|
||||
|
||||
-- If not found, no way to resolve remaining primitives.
|
||||
|
||||
if Cursor = Any_Type then
|
||||
Error_Msg_N
|
||||
("No legal primitive operation First for Iterable type", Aspect);
|
||||
end if;
|
||||
|
||||
return Cursor;
|
||||
end Get_Cursor_Type;
|
||||
|
||||
-------------------------------------
|
||||
-- Inherit_Aspects_At_Freeze_Point --
|
||||
-------------------------------------
|
||||
|
|
|
|||
|
|
@ -1807,7 +1807,10 @@ package body Sem_Ch5 is
|
|||
end if;
|
||||
end if;
|
||||
|
||||
Typ := Etype (Iter_Name);
|
||||
-- Get base type of container, for proper retrieval of Cursor type
|
||||
-- and primitive operations.
|
||||
|
||||
Typ := Base_Type (Etype (Iter_Name));
|
||||
|
||||
if Is_Array_Type (Typ) then
|
||||
if Of_Present (N) then
|
||||
|
|
@ -1918,17 +1921,25 @@ package body Sem_Ch5 is
|
|||
|
||||
-- The result type of Iterate function is the classwide type of
|
||||
-- the interface parent. We need the specific Cursor type defined
|
||||
-- in the container package.
|
||||
-- in the container package. We obtain it by name for a predefined
|
||||
-- container, or through the Iterable aspect for a formal one.
|
||||
|
||||
Ent := First_Entity (Scope (Typ));
|
||||
while Present (Ent) loop
|
||||
if Chars (Ent) = Name_Cursor then
|
||||
Set_Etype (Def_Id, Etype (Ent));
|
||||
exit;
|
||||
end if;
|
||||
if Has_Aspect (Typ, Aspect_Iterable) then
|
||||
Set_Etype (Def_Id,
|
||||
Get_Cursor_Type
|
||||
(Parent (Find_Value_Of_Aspect (Typ, Aspect_Iterable)), Typ));
|
||||
|
||||
Next_Entity (Ent);
|
||||
end loop;
|
||||
else
|
||||
Ent := First_Entity (Scope (Typ));
|
||||
while Present (Ent) loop
|
||||
if Chars (Ent) = Name_Cursor then
|
||||
Set_Etype (Def_Id, Etype (Ent));
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Next_Entity (Ent);
|
||||
end loop;
|
||||
end if;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
|
|
|||
|
|
@ -3898,6 +3898,18 @@ package body Sem_Prag is
|
|||
then
|
||||
OK := True;
|
||||
|
||||
-- If the aspect is a predicate (possibly others ???) and the
|
||||
-- context is a record type, this is a discriminant expression
|
||||
-- within a type declaration, that freezes the predicated
|
||||
-- subtype.
|
||||
|
||||
elsif From_Aspect_Specification (N)
|
||||
and then Prag_Id = Pragma_Predicate
|
||||
and then Ekind (Current_Scope) = E_Record_Type
|
||||
and then Scop = Scope (Current_Scope)
|
||||
then
|
||||
OK := True;
|
||||
|
||||
-- Default case, just check that the pragma occurs in the scope
|
||||
-- of the entity denoted by the name.
|
||||
|
||||
|
|
|
|||
|
|
@ -6387,6 +6387,80 @@ package body Sem_Util is
|
|||
return Proper_Body (Unit (Library_Unit (N)));
|
||||
end Get_Body_From_Stub;
|
||||
|
||||
---------------------
|
||||
-- Get_Cursor_Type --
|
||||
---------------------
|
||||
|
||||
function Get_Cursor_Type
|
||||
(Aspect : Node_Id;
|
||||
Typ : Entity_Id) return Entity_Id
|
||||
is
|
||||
Assoc : Node_Id;
|
||||
Func : Entity_Id;
|
||||
First_Op : Entity_Id;
|
||||
Cursor : Entity_Id;
|
||||
|
||||
begin
|
||||
-- If error already detected, return
|
||||
|
||||
if Error_Posted (Aspect) then
|
||||
return Any_Type;
|
||||
end if;
|
||||
|
||||
-- The cursor type for an Iterable aspect is the return type of a
|
||||
-- non-overloaded First primitive operation. Locate association for
|
||||
-- First.
|
||||
|
||||
Assoc := First (Component_Associations (Expression (Aspect)));
|
||||
First_Op := Any_Id;
|
||||
while Present (Assoc) loop
|
||||
if Chars (First (Choices (Assoc))) = Name_First then
|
||||
First_Op := Expression (Assoc);
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Next (Assoc);
|
||||
end loop;
|
||||
|
||||
if First_Op = Any_Id then
|
||||
Error_Msg_N ("aspect Iterable must specify First operation", Aspect);
|
||||
return Any_Type;
|
||||
end if;
|
||||
|
||||
Cursor := Any_Type;
|
||||
|
||||
-- Locate function with desired name and profile in scope of type
|
||||
|
||||
Func := First_Entity (Scope (Typ));
|
||||
while Present (Func) loop
|
||||
if Chars (Func) = Chars (First_Op)
|
||||
and then Ekind (Func) = E_Function
|
||||
and then Present (First_Formal (Func))
|
||||
and then Etype (First_Formal (Func)) = Typ
|
||||
and then No (Next_Formal (First_Formal (Func)))
|
||||
then
|
||||
if Cursor /= Any_Type then
|
||||
Error_Msg_N
|
||||
("Operation First for iterable type must be unique", Aspect);
|
||||
return Any_Type;
|
||||
|
||||
else
|
||||
Cursor := Etype (Func);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next_Entity (Func);
|
||||
end loop;
|
||||
|
||||
-- If not found, no way to resolve remaining primitives.
|
||||
|
||||
if Cursor = Any_Type then
|
||||
Error_Msg_N
|
||||
("No legal primitive operation First for Iterable type", Aspect);
|
||||
end if;
|
||||
|
||||
return Cursor;
|
||||
end Get_Cursor_Type;
|
||||
-------------------------------
|
||||
-- Get_Default_External_Name --
|
||||
-------------------------------
|
||||
|
|
|
|||
|
|
@ -777,6 +777,14 @@ package Sem_Util is
|
|||
function Get_Body_From_Stub (N : Node_Id) return Node_Id;
|
||||
-- Return the body node for a stub (subprogram or package)
|
||||
|
||||
function Get_Cursor_Type
|
||||
(Aspect : Node_Id;
|
||||
Typ : Entity_Id) return Entity_Id;
|
||||
-- Find Cursor type in scope of formal container Typ, by locating primitive
|
||||
-- operation First.
|
||||
-- For use in resolving the other primitive operations of an Iterable type
|
||||
-- and expanding loops and quantified expressions over formal containers.
|
||||
|
||||
function Get_Default_External_Name (E : Node_Or_Entity_Id) return Node_Id;
|
||||
-- This is used to construct the string literal node representing a
|
||||
-- default external name, i.e. one that is constructed from the name of an
|
||||
|
|
|
|||
Loading…
Reference in New Issue