+2016-04-18 Yannick Moy <moy@adacore.com>
+
+ * sem_util.adb (Apply_Compile_Time_Constraint_Error): Do not generate
+ raise node in GNATprove mode.
+
+2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * s-fileio.adb: Minor reformatting.
+ * sem_prag.adb (Analyze_Input_Item): Add local
+ variable Input_OK. Do not consider mappings of generic formal
+ parameters to actuals.
+
+2016-04-18 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch5.adb (Get_Cursor_Type): If iterator type is a derived
+ type, the cursor is declared in the scope of the parent type.
+ (Analyze_Parameter_Specification): A qualified expression with an
+ iterator type indicates an iteration over a container (explicit
+ or implicit).
+
2016-04-18 Arnaud Charlet <charlet@adacore.com>
* osint-c.ads, osint-c.adb (Delete_C_File, Delete_H_File): New.
else
Fopen_Mode
- (Namestr, Mode, Text_Encoding in Text_Content_Encoding,
- Creat, Amethod, Fopstr);
+ (Namestr => Namestr,
+ Mode => Mode,
+ Text => Text_Encoding in Text_Content_Encoding,
+ Creat => Creat,
+ Amethod => Amethod,
+ Fopstr => Fopstr);
-- A special case, if we are opening (OPEN case) a file and the
-- mode returned by Fopen_Mode is not "r" or "r+", then we first
else
Fopen_Mode
- (File.Name.all, Mode, File.Text_Encoding in Text_Content_Encoding,
- False, File.Access_Method, Fopstr);
+ (Namestr => File.Name.all,
+ Mode => Mode,
+ Text => File.Text_Encoding in Text_Content_Encoding,
+ Creat => False,
+ Amethod => File.Access_Method,
+ Fopstr => Fopstr);
File.Stream := freopen
(File.Name.all'Address, Fopstr'Address, File.Stream,
Ent : Entity_Id;
begin
- Ent := First_Entity (Scope (Typ));
+ -- If iterator type is derived, the cursor is declared in the scope
+ -- of the parent type.
+
+ if Is_Derived_Type (Typ) then
+ Ent := First_Entity (Scope (Etype (Typ)));
+ else
+ Ent := First_Entity (Scope (Typ));
+ end if;
+
while Present (Ent) loop
exit when Chars (Ent) = Name_Cursor;
Next_Entity (Ent);
-- a) a function call,
-- b) an identifier that is not a type,
- -- c) an attribute reference 'Old (within a postcondition)
- -- d) an unchecked conversion
+ -- c) an attribute reference 'Old (within a postcondition),
+ -- d) an unchecked conversion or a qualified expression with
+ -- the proper iterator type.
-- then it is an iteration over a container. It was classified as
-- a loop specification by the parser, and must be rewritten now
-- conversion is always an object.
if Nkind (DS_Copy) = N_Function_Call
+
or else (Is_Entity_Name (DS_Copy)
and then not Is_Type (Entity (DS_Copy)))
+
or else (Nkind (DS_Copy) = N_Attribute_Reference
and then Nam_In (Attribute_Name (DS_Copy),
- Name_Old, Name_Loop_Entry))
- or else Nkind (DS_Copy) = N_Unchecked_Type_Conversion
+ Name_Loop_Entry, Name_Old))
+
or else Has_Aspect (Etype (DS_Copy), Aspect_Iterable)
+
+ or else Nkind (DS_Copy) = N_Unchecked_Type_Conversion
+ or else (Nkind (DS_Copy) = N_Qualified_Expression
+ and then Is_Iterator (Etype (DS_Copy)))
then
-- This is an iterator specification. Rewrite it as such and
-- analyze it to capture function calls that may require
Set_Parent (DS_Copy, Parent (DS));
Preanalyze_Range (DS_Copy);
- -- Check for a call to Iterate ()
+ -- Check for a call to Iterate () or an expression with
+ -- an iterator type.
return
- Nkind (DS_Copy) = N_Function_Call
- and then Needs_Finalization (Etype (DS_Copy));
+ (Nkind (DS_Copy) = N_Function_Call
+ and then Needs_Finalization (Etype (DS_Copy)))
+ or else Is_Iterator (Etype (DS_Copy));
end;
end if;
end Is_Container_Iterator;
procedure Analyze_Input_Item (Input : Node_Id) is
Input_Id : Entity_Id;
+ Input_OK : Boolean := True;
begin
-- Null input list
E_Variable)
then
-- The input cannot denote states or objects declared
- -- within the related package (SPARK RM 7.1.5(4)). The
- -- only exceptions to this are generic formal parameters.
+ -- within the related package (SPARK RM 7.1.5(4)).
- if not Ekind_In (Input_Id, E_Generic_In_Out_Parameter,
- E_Generic_In_Parameter)
- and then Within_Scope (Input_Id, Current_Scope)
- then
- Error_Msg_Name_1 := Chars (Pack_Id);
- SPARK_Msg_NE
- ("input item & cannot denote a visible object or "
- & "state of package %", Input, Input_Id);
+ if Within_Scope (Input_Id, Current_Scope) then
+
+ -- Do not consider generic formal parameters or their
+ -- respective mappings to generic formals. Even though
+ -- the formals appear within the scope of the package,
+ -- it is allowed for an initialization item to depend
+ -- on an input item.
+
+ if Ekind_In (Input_Id, E_Generic_In_Out_Parameter,
+ E_Generic_In_Parameter)
+ then
+ null;
+
+ elsif Ekind_In (Input_Id, E_Constant, E_Variable)
+ and then Present (Corresponding_Generic_Association
+ (Declaration_Node (Input_Id)))
+ then
+ null;
+
+ else
+ Input_OK := False;
+ Error_Msg_Name_1 := Chars (Pack_Id);
+ SPARK_Msg_NE
+ ("input item & cannot denote a visible object or "
+ & "state of package %", Input, Input_Id);
+ end if;
+ end if;
-- Detect a duplicate use of the same input item
-- (SPARK RM 7.1.5(5)).
- elsif Contains (Inputs_Seen, Input_Id) then
+ if Contains (Inputs_Seen, Input_Id) then
+ Input_OK := False;
SPARK_Msg_N ("duplicate input item", Input);
+ end if;
-- Input is legal, add it to the list of processed inputs
- else
+ if Input_OK then
Append_New_Elmt (Input_Id, Inputs_Seen);
if Ekind (Input_Id) = E_Abstract_State then
Discard_Node
(Compile_Time_Constraint_Error (N, Msg, Ent, Loc, Warn => Warn));
- if not Rep then
+ -- In GNATprove mode, do not replace the node with an exception raised.
+ -- In such a case, either the call to Compile_Time_Constraint_Error
+ -- issues an error which stops analysis, or it issues a warning in
+ -- a few cases where a suitable check flag is set for GNATprove to
+ -- generate a check message.
+
+ if not Rep or GNATprove_Mode then
return;
end if;
projects / gcc.git / commitdiff