+2014-02-24 Yannick Moy <moy@adacore.com>
+
+ * freeze.adb (Freeze_Entity): Do not issue warning
+ for pre/post being ignored on imported subprogram in GNATprove
+ mode.
+
+2014-02-24 Robert Dewar <dewar@adacore.com>
+
+ * exp_ch5.adb, sem_ch5.adb, sem_type.adb, sem_res.adb, sem_attr.adb,
+ stand.ads, sem_eval.adb: Minor reformatting.
+
+2014-02-24 Yannick Moy <moy@adacore.com>
+
+ * sem_prag.adb: Minor rewording in error message.
+
+2014-02-24 Johannes Kanig <kanig@adacore.com>
+
+ * exp_util.adb (Expand_Subtype_From_Expr): Do not expand subtypes in
+ GNATprove_mode, gnat2why doesn't need nor use these types.
+
+2014-02-24 Gary Dismukes <dismukes@adacore.com>
+
+ * exp_ch4.adb (Expand_N_Op_Expon): On the AAMP
+ target, in the case of signed integer exponentiation that uses a
+ run-time routine, always select the Exp_* versions, since overflow
+ checking is automatically done by AAMP arithmetic instructions.
+
+2014-02-24 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_ch13.adb (Analyze_Aspect_Specifications):
+ When the related context is a package instace, insert pragma
+ Abstract_State after all internally-generated renamings related
+ to the instance "header".
+
+2014-02-24 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch3.adb (Analyze_Declarations): Analyze Contract of abstract
+ subprograms.
+ * sem_disp.adb (Check_Dispatching_Context): A non-dispatching
+ call to an abstract subprogram is legal if it appears in a
+ pre/postcondition of another abstract operation.
+
2014-02-24 Sergey Rybin <rybin@adacore.com frybin>
* gnat_ugn.texi: Misc updates.
then
Etyp := Standard_Long_Long_Integer;
- if Ovflo then
+ -- Overflow checking is the only choice on the AAMP target, where
+ -- arithmetic instructions check overflow automatically, so only
+ -- one version of the exponentiation unit is needed.
+
+ if Ovflo or else AAMP_On_Target then
Rent := RE_Exp_Long_Long_Integer;
else
Rent := RE_Exn_Long_Long_Integer;
elsif Is_Signed_Integer_Type (Rtyp) then
Etyp := Standard_Integer;
- if Ovflo then
+ -- Overflow checking is the only choice on the AAMP target, where
+ -- arithmetic instructions check overflow automatically, so only
+ -- one version of the exponentiation unit is needed.
+
+ if Ovflo or else AAMP_On_Target then
Rent := RE_Exp_Integer;
else
Rent := RE_Exn_Integer;
is
Loc : constant Source_Ptr := Sloc (N);
Stats : constant List_Id := Statements (N);
-
- Typ : constant Entity_Id := Base_Type (Etype (Container));
- First_Op : constant Entity_Id :=
+ Typ : constant Entity_Id := Base_Type (Etype (Container));
+ First_Op : constant Entity_Id :=
Get_Iterable_Type_Primitive (Typ, Name_First);
- Next_Op : constant Entity_Id :=
+ Next_Op : constant Entity_Id :=
Get_Iterable_Type_Primitive (Typ, Name_Next);
+
Has_Element_Op : constant Entity_Id :=
Get_Iterable_Type_Primitive (Typ, Name_Has_Element);
begin
-- Declaration for Cursor
Init :=
- Make_Object_Declaration (Loc,
- Defining_Identifier => Cursor,
- Object_Definition => New_Occurrence_Of (Etype (First_Op), Loc),
- Expression =>
- Make_Function_Call (Loc,
- Name => New_Occurrence_Of (First_Op, Loc),
- Parameter_Associations =>
- New_List (New_Occurrence_Of (Container, Loc))));
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Cursor,
+ Object_Definition => New_Occurrence_Of (Etype (First_Op), Loc),
+ Expression =>
+ Make_Function_Call (Loc,
+ Name => New_Occurrence_Of (First_Op, Loc),
+ Parameter_Associations => New_List (
+ New_Occurrence_Of (Container, Loc))));
-- Statement that advances cursor in loop
Advance :=
Make_Assignment_Statement (Loc,
- Name => New_Occurrence_Of (Cursor, Loc),
+ Name => New_Occurrence_Of (Cursor, Loc),
Expression =>
Make_Function_Call (Loc,
- Name => New_Occurrence_Of (Next_Op, Loc),
- Parameter_Associations =>
- New_List
- (New_Occurrence_Of (Container, Loc),
- New_Occurrence_Of (Cursor, Loc))));
+ Name => New_Occurrence_Of (Next_Op, Loc),
+ Parameter_Associations => New_List (
+ New_Occurrence_Of (Container, Loc),
+ New_Occurrence_Of (Cursor, Loc))));
-- Iterator is rewritten as a while_loop
Make_Iteration_Scheme (Loc,
Condition =>
Make_Function_Call (Loc,
- Name =>
- New_Occurrence_Of (Has_Element_Op, Loc),
- Parameter_Associations =>
- New_List
- (New_Occurrence_Of (Container, Loc),
- New_Occurrence_Of (Cursor, Loc)))),
- Statements => Stats,
- End_Label => Empty);
+ Name => New_Occurrence_Of (Has_Element_Op, Loc),
+ Parameter_Associations => New_List (
+ New_Occurrence_Of (Container, Loc),
+ New_Occurrence_Of (Cursor, Loc)))),
+ Statements => Stats,
+ End_Label => Empty);
end Build_Formal_Container_Iteration;
------------------------------
Container : constant Node_Id := Entity (Name (I_Spec));
Stats : constant List_Id := Statements (N);
- Advance : Node_Id;
- Init : Node_Id;
- New_Loop : Node_Id;
+ Advance : Node_Id;
+ Init : Node_Id;
+ New_Loop : Node_Id;
begin
-- The expansion resembles the one for Ada containers, but the
Cursor : constant Entity_Id :=
Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (Element), 'C'));
+ Chars => New_External_Name (Chars (Element), 'C'));
Elmt_Decl : Node_Id;
Elmt_Ref : Node_Id;
- Element_Op : constant Entity_Id :=
- Get_Iterable_Type_Primitive
- (Container_Typ, Name_Element);
+ Element_Op : constant Entity_Id :=
+ Get_Iterable_Type_Primitive (Container_Typ, Name_Element);
Advance : Node_Id;
Init : Node_Id;
-- Declaration for Element.
- Elmt_Decl := Make_Object_Declaration (Loc,
- Defining_Identifier => Element,
- Object_Definition => New_Occurrence_Of (Etype (Element_Op), Loc));
+ Elmt_Decl :=
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Element,
+ Object_Definition => New_Occurrence_Of (Etype (Element_Op), Loc));
-- The element is only modified in expanded code, so it appears as
-- unassigned to the warning machinery. We must suppress this spurious
Set_Warnings_Off (Element);
- Elmt_Ref := Make_Assignment_Statement (Loc,
- Name => New_Occurrence_Of (Element, Loc),
- Expression =>
- Make_Function_Call (Loc,
- Name => New_Occurrence_Of (Element_Op, Loc),
- Parameter_Associations =>
- New_List
- (New_Occurrence_Of (Container, Loc),
- New_Occurrence_Of (Cursor, Loc))));
+ Elmt_Ref :=
+ Make_Assignment_Statement (Loc,
+ Name => New_Occurrence_Of (Element, Loc),
+ Expression =>
+ Make_Function_Call (Loc,
+ Name => New_Occurrence_Of (Element_Op, Loc),
+ Parameter_Associations => New_List (
+ New_Occurrence_Of (Container, Loc),
+ New_Occurrence_Of (Cursor, Loc))));
Prepend (Elmt_Ref, Stats);
Append_To (Stats, Advance);
- -- The loop is rewritten as a block, to hold the declaration for the
- -- element.
+ -- The loop is rewritten as a block, to hold the element declaration
- New_Loop := Make_Block_Statement (Loc,
- Declarations => New_List (Elmt_Decl),
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (New_Loop)));
+ New_Loop :=
+ Make_Block_Statement (Loc,
+ Declarations => New_List (Elmt_Decl),
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (New_Loop)));
Rewrite (N, New_Loop);
Analyze (New_Loop);
else
Expand_Formal_Container_Loop (N);
end if;
+
return;
end if;
-- may be constants that depend on the bounds of a string literal, both
-- standard string types and more generally arrays of characters.
- -- In GNATprove mode, we also need the more precise subtype to be set
+ -- In GNATprove mode, these extra subtypes are not needed
- if not (Expander_Active or GNATprove_Mode)
- and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
- then
+ if GNATprove_Mode then
return;
end if;
- -- In GNATprove mode, Unc_Type might not be complete when analyzing
- -- a generic unit. As generic units are not analyzed directly in
- -- GNATprove, return here rather than failing later.
-
- if GNATprove_Mode and then No (Underlying_Type (Unc_Type)) then
+ if not Expander_Active
+ and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
+ then
return;
end if;
end if;
end;
- -- Pre/post conditions are implemented through a subprogram in
- -- the corresponding body, and therefore are not checked on an
- -- imported subprogram for which the body is not available.
+ -- Pre/post conditions are implemented through a subprogram
+ -- in the corresponding body, and therefore are not checked on
+ -- an imported subprogram for which the body is not available.
+ -- This warning is not issued in GNATprove mode, as these
+ -- contracts are handled in formal verification, so the
+ -- warning would be misleading in that case.
-- Could consider generating a wrapper to take care of this???
and then Is_Imported (E)
and then Present (Contract (E))
and then Present (Pre_Post_Conditions (Contract (E)))
+ and then not GNATprove_Mode
then
Error_Msg_NE
("pre/post conditions on imported subprogram are not "
elsif Comp_Type /= Base_Type (Etype (Comp)) then
Error_Msg_N
("components in choice list must have same type",
- Assoc);
+ Assoc);
end if;
end if;
end if;
when Aspect_Abstract_State => Abstract_State : declare
Context : Node_Id := N;
+ Decl : Node_Id;
Decls : List_Id;
begin
if Nkind_In (Context, N_Generic_Package_Declaration,
N_Package_Declaration)
then
- Decls := Visible_Declarations (Specification (Context));
-
Make_Aitem_Pragma
(Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Pragma_Name => Name_Abstract_State);
Decorate_Aspect_And_Pragma (Aspect, Aitem);
- if No (Decls) then
- Decls := New_List;
- Set_Visible_Declarations (Context, Decls);
- end if;
+ Decls := Visible_Declarations (Specification (Context));
- Prepend_To (Decls, Aitem);
+ -- In general pragma Abstract_State must be at the top
+ -- of the existing visible declarations to emulate its
+ -- source counterpart. The only exception to this is a
+ -- generic instance in which case the pragma must be
+ -- inserted after the association renamings.
+
+ if Present (Decls) then
+
+ -- The visible declarations of a generic instance have
+ -- the following structure:
+
+ -- <renamings of generic formals>
+ -- <renamings of internally-generated spec and body>
+ -- <first source declaration>
+
+ -- The pragma must be inserted before the first source
+ -- declaration.
+
+ if Is_Generic_Instance (Defining_Entity (Context)) then
+
+ -- Skip the instance "header"
+
+ Decl := First (Decls);
+ while Present (Decl)
+ and then not Comes_From_Source (Decl)
+ loop
+ Decl := Next (Decl);
+ end loop;
+
+ if Present (Decl) then
+ Insert_Before (Decl, Aitem);
+ else
+ Append_To (Decls, Aitem);
+ end if;
+
+ -- The related package is not a generic instance, the
+ -- corresponding pragma must be the first declaration.
+
+ else
+ Prepend_To (Decls, Aitem);
+ end if;
+
+ -- Otherwise the pragma forms a new declarative list
+
+ else
+ Set_Visible_Declarations
+ (Specification (Context), New_List (Aitem));
+ end if;
else
Error_Msg_NE
elsif Nkind (Decl) = N_Subprogram_Body then
Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
- elsif Nkind (Decl) = N_Subprogram_Declaration then
+ elsif Nkind_In (Decl,
+ N_Subprogram_Declaration,
+ N_Abstract_Subprogram_Declaration)
+ then
Analyze_Subprogram_Contract (Defining_Entity (Decl));
end if;
else
Set_Ekind (Def_Id, E_Loop_Parameter);
+ -- OF present
+
if Of_Present (N) then
if Has_Aspect (Typ, Aspect_Iterable) then
if No (Get_Iterable_Type_Primitive (Typ, Name_Element)) then
- Error_Msg_N ("Missing Element primitive for iteration", N);
+ Error_Msg_N ("missing Element primitive for iteration", N);
end if;
-- For a predefined container, The type of the loop variable is
else
declare
Element : constant Entity_Id :=
- Find_Value_Of_Aspect (Typ, Aspect_Iterator_Element);
+ Find_Value_Of_Aspect (Typ, Aspect_Iterator_Element);
+
begin
if No (Element) then
Error_Msg_NE ("cannot iterate over&", N, Typ);
return;
+
else
Set_Etype (Def_Id, Entity (Element));
-- matches element type of container.
if Present (Subt)
- and then Bas /= Base_Type (Etype (Def_Id))
+ and then Bas /= Base_Type (Etype (Def_Id))
then
Error_Msg_N
("subtype indication does not match element type",
- Subt);
+ Subt);
end if;
-- If the container has a variable indexing aspect, the
end;
end if;
+ -- OF not present
+
else
-- For an iteration of the form IN, the name must denote an
-- iterator, typically the result of a call to Iterate. Give a
if Has_Aspect (Typ, Aspect_Iterable) then
Set_Etype (Def_Id,
Get_Cursor_Type
- (Parent (Find_Value_Of_Aspect (Typ, Aspect_Iterable)), Typ));
+ (Parent (Find_Value_Of_Aspect (Typ, Aspect_Iterable)),
+ Typ));
Ent := Etype (Def_Id);
else
-- A loop parameter cannot be volatile. This check is peformed only when
-- SPARK_Mode is on as it is not a standard Ada legality check.
+
-- Not clear whether this applies to element iterators, where the
-- cursor is not an explicit entity ???
-- the current declarative part. The expression will be properly
-- rewritten/reanalyzed when the postcondition procedure is built.
+ -- Similarly, if this is a pre/postcondition for an abstract
+ -- subprogram, it may call another abstract function which is
+ -- a primitive of an abstract type. The call is non-dispatching
+ -- but will be legal in overridings of the operation.
+
elsif In_Spec_Expression
and then Is_Subprogram (Current_Scope)
and then
- Nkind (Parent (Current_Scope)) = N_Procedure_Specification
- and then Null_Present (Parent (Current_Scope))
+ ((Nkind (Parent (Current_Scope)) = N_Procedure_Specification
+ and then Null_Present (Parent (Current_Scope)))
+ or else Is_Abstract_Subprogram (Current_Scope))
then
null;
-- If either subtype is nonstatic then they're not compatible
elsif not Is_Static_Subtype (T1)
- or else not Is_Static_Subtype (T2)
+ or else
+ not Is_Static_Subtype (T2)
then
return False;
-- (and Esizes can be set when Frontend_Layout_On_Target is True).
elsif not Formal_Derived_Matching
- and then Known_Static_Esize (T1) and then Known_Static_Esize (T2)
+ and then Known_Static_Esize (T1)
+ and then Known_Static_Esize (T2)
and then Esize (T1) /= Esize (T2)
then
return False;
procedure Grouping_Error (Prag : Node_Id) is
begin
Error_Msg_Sloc := Sloc (Prag);
- Error_Pragma ("pragma% must appear immediately after pragma#");
+ Error_Pragma
+ ("pragma% should appear immediately after pragma#");
end Grouping_Error;
-- Start of processing for Check_Loop_Pragma_Grouping
-- A useful optimization: check whether the dereference denotes an
-- element of a container, and if so rewrite it as a call to the
-- corresponding Element function.
+
-- Disabled for now, on advice of ARG. A more restricted form of the
-- predicate might be acceptable ???
elsif BT2 = Any_Type then
return True;
- -- A Raise_Expressions is legal in any expression context.
+ -- A Raise_Expressions is legal in any expression context
elsif BT2 = Raise_Type then
return True;
-- The type Raise_Type denotes the type of a Raise_Expression. It is
-- compatible with all other types, and must eventually resolve to a
-- concrete type that is imposed by the context.
+ --
+ -- Historical note: we used to use Any_Type for this purpose, but the
+ -- confusion of meanings (Any_Type normally indicates an error) caused
+ -- difficulties. In particular some needed expansions were skipped since
+ -- the nodes in question looked like they had an error.
Universal_Integer : Entity_Id;
-- Entity for universal integer type. The bounds of this type correspond
projects / thirdparty / gcc.git / commitdiff
