diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 2b8e6aeeb78..0a3c479415c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,23 @@ +2016-04-18 Yannick Moy + + * sem_util.adb (Apply_Compile_Time_Constraint_Error): Do not generate + raise node in GNATprove mode. + +2016-04-18 Hristian Kirtchev + + * 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 + + * 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 * osint-c.ads, osint-c.adb (Delete_C_File, Delete_H_File): New. diff --git a/gcc/ada/s-fileio.adb b/gcc/ada/s-fileio.adb index 99910f7423e..b8bc1ad2248 100644 --- a/gcc/ada/s-fileio.adb +++ b/gcc/ada/s-fileio.adb @@ -1057,8 +1057,12 @@ package body System.File_IO is 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 @@ -1230,8 +1234,12 @@ package body System.File_IO is 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, diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index b4e82783b2b..b29b73fb1c6 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -1795,7 +1795,15 @@ package body Sem_Ch5 is 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); @@ -2747,8 +2755,9 @@ package body Sem_Ch5 is -- 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 @@ -2758,13 +2767,19 @@ package body Sem_Ch5 is -- 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 @@ -3138,11 +3153,13 @@ package body Sem_Ch5 is 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; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 60d83179e9f..8d212fe76c2 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2826,6 +2826,7 @@ package body Sem_Prag is procedure Analyze_Input_Item (Input : Node_Id) is Input_Id : Entity_Id; + Input_OK : Boolean := True; begin -- Null input list @@ -2868,27 +2869,47 @@ package body Sem_Prag is 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 diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 348da03b26f..88973765a3a 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -599,7 +599,13 @@ package body Sem_Util is 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;