+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
-- 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
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})
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})
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})
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})
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})
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})
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).
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
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)
-- 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
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 --
-------------------------------------
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
-- 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;
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.
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 --
-------------------------------
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
git://gcc.gnu.org / gcc.git / commitdiff