From 8fdafe44be001fa59172d7a28626d4babdc24b7b Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 27 Jan 2014 17:39:57 +0100 Subject: [multiple changes] 2014-01-27 Thomas Quinot * exp_ch7.adb: Minor reformatting. 2014-01-27 Robert Dewar * opt.adb (SPARK_Mode): Default for library units is None rather than Off. * opt.ads: Remove AUTO from SPARK_Mode_Type SPARK_Mode_Type is no longer ordered. * sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Remove AUTO possibility. * snames.ads-tmpl (Name_Auto): Removed, no longer used. 2014-01-27 Robert Dewar * par-ch5.adb (P_Sequence_Of_Statements): Make entry in Suspicious_Labels table if we have identifier; followed by loop or block. * par-endh.adb (Evaluate_End_Entry): Search Suspicious_Labels table. * par.adb (Suspicious_Labels): New table. 2014-01-27 Robert Dewar * exp_aggr.adb (Check_Bounds): Reason is range check, not length check. 2014-01-27 Yannick Moy * get_spark_xrefs.adb (Get_SPARK_Xrefs): Accept new type 'c' for reference. * lib-xref-spark_specific.adb (Is_Global_Constant): Remove useless function now. (Add_SPARK_Xrefs): Include references to constants. * spark_xrefs.ads Document new character 'c' for references to constants. 2014-01-27 Thomas Quinot * exp_smem.adb (Add_Write_After): For a function call, insert write as an after action in a transient scope. From-SVN: r207140 --- gcc/ada/ChangeLog | 42 +++++++++++++++++++++++ gcc/ada/exp_aggr.adb | 2 +- gcc/ada/exp_ch7.adb | 2 +- gcc/ada/exp_smem.adb | 21 ++++++++---- gcc/ada/get_spark_xrefs.adb | 1 + gcc/ada/lib-xref-spark_specific.adb | 37 ++++++++------------- gcc/ada/opt.adb | 2 +- gcc/ada/opt.ads | 6 ++-- gcc/ada/par-ch5.adb | 18 ++++++++++ gcc/ada/par-endh.adb | 66 ++++++++++++++++++++++++++++++++----- gcc/ada/par.adb | 60 +++++++++++++++++++++++++++++++++ gcc/ada/sem_prag.adb | 53 +++++------------------------ gcc/ada/snames.ads-tmpl | 1 - gcc/ada/spark_xrefs.ads | 2 ++ 14 files changed, 223 insertions(+), 90 deletions(-) (limited to 'gcc') diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 3cebcd0..f50f691 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,47 @@ 2014-01-27 Thomas Quinot + * exp_ch7.adb: Minor reformatting. + +2014-01-27 Robert Dewar + + * opt.adb (SPARK_Mode): Default for library units is None rather + than Off. + * opt.ads: Remove AUTO from SPARK_Mode_Type SPARK_Mode_Type is + no longer ordered. + * sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Remove AUTO + possibility. + * snames.ads-tmpl (Name_Auto): Removed, no longer used. + +2014-01-27 Robert Dewar + + * par-ch5.adb (P_Sequence_Of_Statements): Make entry in + Suspicious_Labels table if we have identifier; followed by loop + or block. + * par-endh.adb (Evaluate_End_Entry): Search Suspicious_Labels table. + * par.adb (Suspicious_Labels): New table. + +2014-01-27 Robert Dewar + + * exp_aggr.adb (Check_Bounds): Reason is range check, not + length check. + +2014-01-27 Yannick Moy + + * get_spark_xrefs.adb (Get_SPARK_Xrefs): Accept new type 'c' for + reference. + * lib-xref-spark_specific.adb (Is_Global_Constant): Remove useless + function now. + (Add_SPARK_Xrefs): Include references to constants. + * spark_xrefs.ads Document new character 'c' for references to + constants. + +2014-01-27 Thomas Quinot + + * exp_smem.adb (Add_Write_After): For a function call, insert write as + an after action in a transient scope. + +2014-01-27 Thomas Quinot + * exp_smem.adb (Expand_Shared_Passive_Variable): For a reference to a shared variable as an OUT formal in a call to an init proc, the 'Read call must be emitted after, not before, the call. diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index 6c5104b..6518e5b 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -4141,7 +4141,7 @@ package body Exp_Aggr is Insert_Action (N, Make_Raise_Constraint_Error (Loc, Condition => Cond, - Reason => CE_Length_Check_Failed)); + Reason => CE_Range_Check_Failed)); end if; end Check_Bounds; diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 7479436..ed3dc4c 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -3612,7 +3612,7 @@ package body Exp_Ch7 is -- This procedure is called each time a transient block has to be inserted -- that is to say for each call to a function with unconstrained or tagged -- result. It creates a new scope on the stack scope in order to enclose - -- all transient variables generated + -- all transient variables generated. procedure Establish_Transient_Scope (N : Node_Id; Sec_Stack : Boolean) is Loc : constant Source_Ptr := Sloc (N); diff --git a/gcc/ada/exp_smem.adb b/gcc/ada/exp_smem.adb index 2b83105..7fb40c4 100644 --- a/gcc/ada/exp_smem.adb +++ b/gcc/ada/exp_smem.adb @@ -25,6 +25,7 @@ with Atree; use Atree; with Einfo; use Einfo; +with Exp_Ch7; use Exp_Ch7; with Exp_Ch9; use Exp_Ch9; with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; @@ -58,8 +59,10 @@ package body Exp_Smem is procedure Add_Write_After (N : Node_Id); -- Insert a Shared_Var_WOpen call for variable after the node Insert_Node, -- as recorded by On_Lhs_Of_Assignment (where it points to the assignment - -- statement) or Is_Out_Actual (where it points to the procedure call - -- statement). + -- statement) or Is_Out_Actual (where it points to the subprogram call). + -- When Insert_Node is a function call, establish a transient scope around + -- the expression, and insert the write as an after-action of the transient + -- scope. procedure Build_Full_Name (E : Entity_Id; N : out String_Id); -- Build the fully qualified string name of a shared variable @@ -191,12 +194,18 @@ package body Exp_Smem is procedure Add_Write_After (N : Node_Id) is Loc : constant Source_Ptr := Sloc (N); - Ent : constant Node_Id := Entity (N); - + Ent : constant Entity_Id := Entity (N); + Par : constant Node_Id := Insert_Node; begin if Present (Shared_Var_Procs_Instance (Ent)) then - Insert_After_And_Analyze (Insert_Node, - Build_Shared_Var_Proc_Call (Loc, Ent, Name_Write)); + if Nkind (Insert_Node) = N_Function_Call then + Establish_Transient_Scope (Insert_Node, Sec_Stack => False); + Store_After_Actions_In_Scope (New_List ( + Build_Shared_Var_Proc_Call (Loc, Ent, Name_Write))); + else + Insert_After_And_Analyze (Par, + Build_Shared_Var_Proc_Call (Loc, Ent, Name_Write)); + end if; end if; end Add_Write_After; diff --git a/gcc/ada/get_spark_xrefs.adb b/gcc/ada/get_spark_xrefs.adb index 92964b3..ea1f1b4 100644 --- a/gcc/ada/get_spark_xrefs.adb +++ b/gcc/ada/get_spark_xrefs.adb @@ -455,6 +455,7 @@ begin pragma Assert (Rtype = 'r' or else + Rtype = 'c' or else Rtype = 'm' or else Rtype = 's'); diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 9328be8..0b32aad 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -334,10 +334,6 @@ package body SPARK_Specific is S : Scope_Index) return Boolean; -- Check whether entity E is in SPARK_Scope_Table at index S or higher - function Is_Global_Constant (E : Entity_Id) return Boolean; - -- Return True if E is a global constant for which we should ignore - -- reads in SPARK. - function Lt (Op1 : Natural; Op2 : Natural) return Boolean; -- Comparison function for Sort call @@ -440,14 +436,6 @@ package body SPARK_Specific is if Ekind (E) in Overloadable_Kind then return Typ = 's'; - -- References to constant objects are not considered in SPARK - -- section, as these will be translated as constants in the - -- intermediate language for formal verification, and should - -- therefore never appear in frame conditions. - - elsif Is_Constant_Object (E) then - return False; - -- Objects of Task type or protected type are not SPARK references elsif Present (Etype (E)) @@ -526,16 +514,6 @@ package body SPARK_Specific is return False; end Is_Future_Scope_Entity; - ------------------------ - -- Is_Global_Constant -- - ------------------------ - - function Is_Global_Constant (E : Entity_Id) return Boolean is - begin - return Ekind (E) = E_Constant - and then Ekind_In (Scope (E), E_Package, E_Package_Body); - end Is_Global_Constant; - -------- -- Lt -- -------- @@ -726,7 +704,6 @@ package body SPARK_Specific is and then SPARK_References (Ref.Typ) and then Is_SPARK_Scope (Ref.Ent_Scope) and then Is_SPARK_Scope (Ref.Ref_Scope) - and then not Is_Global_Constant (Ref.Ent) and then Is_SPARK_Reference (Ref.Ent, Ref.Typ) -- Discard references from unknown scopes, e.g. generic scopes @@ -805,6 +782,7 @@ package body SPARK_Specific is declare Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno)); Ref : Xref_Key renames Ref_Entry.Key; + Typ : Character; begin -- If this assertion fails, the scope which we are looking for is @@ -844,6 +822,17 @@ package body SPARK_Specific is Col := Int (Get_Column_Number (Ref_Entry.Def)); end if; + -- References to constant objects are considered specially in + -- SPARK section, because these will be translated as constants in + -- the intermediate language for formal verification, and should + -- therefore never appear in frame conditions. + + if Is_Constant_Object (Ref.Ent) then + Typ := 'c'; + else + Typ := Ref.Typ; + end if; + SPARK_Xref_Table.Append ( (Entity_Name => Ref_Name, Entity_Line => Line, @@ -852,7 +841,7 @@ package body SPARK_Specific is File_Num => Dependency_Num (Ref.Lun), Scope_Num => Get_Scope_Num (Ref.Ref_Scope), Line => Int (Get_Logical_Line_Number (Ref.Loc)), - Rtype => Ref.Typ, + Rtype => Typ, Col => Int (Get_Column_Number (Ref.Loc)))); end; end loop; diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb index 383f5f4..30623ea 100644 --- a/gcc/ada/opt.adb +++ b/gcc/ada/opt.adb @@ -186,7 +186,7 @@ package body Opt is Assertions_Enabled := False; Assume_No_Invalid_Values := False; Check_Policy_List := Empty; - SPARK_Mode := Off; + SPARK_Mode := None; SPARK_Mode_Pragma := Empty; end if; diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 28d1220..344caaf 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1264,9 +1264,9 @@ package Opt is -- GNAT -- Set True if a pragma Short_Descriptors applies to the current unit. - type SPARK_Mode_Type is (None, Off, Auto, On); - pragma Ordered (SPARK_Mode_Type); - -- Possible legal modes that can be set by aspect/pragma SPARK_Mode + type SPARK_Mode_Type is (None, Off, On); + -- Possible legal modes that can be set by aspect/pragma SPARK_Mode, as + -- well as the value None, which indicates no such pragma/aspect applies. SPARK_Mode : SPARK_Mode_Type := None; -- GNAT diff --git a/gcc/ada/par-ch5.adb b/gcc/ada/par-ch5.adb index e20cf11..8992f15 100644 --- a/gcc/ada/par-ch5.adb +++ b/gcc/ada/par-ch5.adb @@ -506,6 +506,24 @@ package body Ch5 is Scan; -- past semicolon Statement_Required := False; + -- Here is the special test for a suspicious label, more + -- accurately a suspicious name, which we think perhaps + -- should have been a label. If next token is one of + -- LOOP, FOR, WHILE, DECLARE, BEGIN, then make an entry + -- in the suspicious label table. + + if Token = Tok_Loop or else + Token = Tok_For or else + Token = Tok_While or else + Token = Tok_Declare or else + Token = Tok_Begin + then + Suspicious_Labels.Append + ((Proc_Call => Id_Node, + Semicolon_Loc => Prev_Token_Ptr, + Start_Token => Token_Ptr)); + end if; + -- Check for case of "go to" in place of "goto" elsif Token = Tok_Identifier diff --git a/gcc/ada/par-endh.adb b/gcc/ada/par-endh.adb index e6d4e19..e41e7a3 100644 --- a/gcc/ada/par-endh.adb +++ b/gcc/ada/par-endh.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2012, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -711,17 +711,67 @@ package body Endh is ------------------------ procedure Evaluate_End_Entry (SS_Index : Nat) is + STE : Scope_Table_Entry renames Scope.Table (SS_Index); + begin - Column_OK := (End_Column = Scope.Table (SS_Index).Ecol); + Column_OK := (End_Column = STE.Ecol); - Token_OK := (End_Type = Scope.Table (SS_Index).Etyp or else - (End_Type = E_Name and then - Scope.Table (SS_Index).Etyp >= E_Name)); + Token_OK := (End_Type = STE.Etyp + or else (End_Type = E_Name and then STE.Etyp >= E_Name)); Label_OK := End_Labl_Present - and then - (Same_Label (End_Labl, Scope.Table (SS_Index).Labl) - or else Scope.Table (SS_Index).Labl = Error); + and then (Same_Label (End_Labl, STE.Labl) + or else STE.Labl = Error); + + -- Special case to consider. Suppose we have the suspicious label case, + -- e.g. a situation like: + + -- My_Label; + -- declare + -- ... + -- begin + -- ... + -- end My_Label; + + -- This is the case where we want to use the entry in the suspicous + -- label table to flag the semicolon saying it should be a colon. + + -- Label_OK will be false because the label does not match (we have + -- My_Label on the end line, and the generated name for the scope). Also + -- End_Labl_Present will be True. + + if not Label_OK + and then End_Labl_Present + and then not Comes_From_Source (Scope.Table (SS_Index).Labl) + then + -- Here is where we will search the suspicious labels table + + for J in 1 .. Suspicious_Labels.Last loop + declare + SLE : Suspicious_Label_Entry renames + Suspicious_Labels.Table (J); + begin + -- See if character name of label matches + + if Chars (Name (SLE.Proc_Call)) = Chars (End_Labl) + + -- And first token of loop/block identifies this entry + + and then SLE.Start_Token = STE.Sloc + then + -- We have the special case, issue the error message + + Error_Msg -- CODEFIX + (""";"" should be "":""", SLE.Semicolon_Loc); + + -- And indicate we consider the Label OK after all + + Label_OK := True; + exit; + end if; + end; + end loop; + end if; -- Compute setting of Syntax_OK. We definitely have a syntax error -- if the Token does not match properly or if P_End_Scan detected diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb index 6788692..7e69166d 100644 --- a/gcc/ada/par.adb +++ b/gcc/ada/par.adb @@ -535,6 +535,66 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is Table_Increment => 100, Table_Name => "Scope"); + ------------------------------------------ + -- Table for Handling Suspicious Labels -- + ------------------------------------------ + + -- This is a special data structure which is used to deal very spefifically + -- with the following error case + + -- label; + -- loop + -- ... + -- end loop label; + + -- Similar cases apply to FOR, WHILE, DECLARE, or BEGIN + + -- In each case the opening line looks like a procedure call because of + -- the semicolon. And the end line looks illegal because of an unexpected + -- label. If we did nothing special, we would just diagnose the label on + -- the end as unexpected. But that does not help point to the real error + -- which is that the semicolon after label should be a colon. + + -- To deal with this, we build an entry in the Suspicious_Labels table + -- whenever we encounter an identifier followed by a semicolon, followed + -- by one of LOOP, FOR, WHILE, DECLARE, BEGIN. Then this entry is used to + -- issue the right message when we hit the END that confirms that this was + -- a bad label. + + type Suspicious_Label_Entry is record + Proc_Call : Node_Id; + -- Node for the procedure call statement built for the label; construct + + Semicolon_Loc : Source_Ptr; + -- Location of the possibly wrong semicolon + + Start_Token : Source_Ptr; + -- Source location of the LOOP, FOR, WHILE, DECLARE, BEGIN token + end record; + + package Suspicious_Labels is new Table.Table ( + Table_Component_Type => Suspicious_Label_Entry, + Table_Index_Type => Int, + Table_Low_Bound => 1, + Table_Initial => 50, + Table_Increment => 100, + Table_Name => "Suspicious_Labels"); + + -- Now when we are about to issue a message complaining about an END label + -- that should not be there because it appears to end a construct that has + -- no label, we first search the suspicious labels table entry, using the + -- source location stored in the scope table as a key. If we find a match, + -- then we check that the label on the end matches the name in the call, + -- and if so, we issue a message saying the semicolon should be a colon. + + -- Quite a bit of work, but really helpful in the case where it helps, and + -- the need for this is based on actual experience with tracking down this + -- kind of error (the eye often easily mistakes semicolon for colon!) + + -- Note: we actually have enough information to patch up the tree, but + -- this may not be worth the effort! Also we could deal with the same + -- situation for EXIT with a label, but for now don't bother with that! + --------------------------------- -- Parsing Routines by Chapter -- --------------------------------- diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 85d5049..1d0c96f 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -18587,7 +18587,7 @@ package body Sem_Prag is -- SPARK_Mode -- ---------------- - -- pragma SPARK_Mode [(On | Off | Auto)]; + -- pragma SPARK_Mode [(On | Off)]; when Pragma_SPARK_Mode => Do_SPARK_Mode : declare Body_Id : Entity_Id; @@ -18609,9 +18609,6 @@ package body Sem_Prag is procedure Check_Library_Level_Entity (E : Entity_Id); -- Verify that pragma is applied to library-level entity E - function Get_SPARK_Mode_Name (Id : SPARK_Mode_Type) return Name_Id; - -- Convert a value of type SPARK_Mode_Type to corresponding name - ------------------------------ -- Check_Pragma_Conformance -- ------------------------------ @@ -18623,15 +18620,13 @@ package body Sem_Prag is -- New mode less restrictive than the established mode - if Get_SPARK_Mode_From_Pragma (Old_Pragma) < Mode_Id then - Error_Msg_Name_1 := Mode; - Error_Msg_N ("cannot define 'S'P'A'R'K mode %", Arg1); - - Error_Msg_Name_1 := Get_SPARK_Mode_Name (SPARK_Mode); - Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma); + if Get_SPARK_Mode_From_Pragma (Old_Pragma) = Off + and then Mode_Id = On + then Error_Msg_N - ("\mode is less restrictive than mode " - & "% defined #", Arg1); + ("cannot change 'S'P'A'R'K_Mode from Off to On", Arg1); + Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma); + Error_Msg_N ("\'S'P'A'R'K_Mode was set to Off#", Arg1); raise Pragma_Exit; end if; end if; @@ -18665,28 +18660,6 @@ package body Sem_Prag is end if; end Check_Library_Level_Entity; - ------------------------- - -- Get_SPARK_Mode_Name -- - ------------------------- - - function Get_SPARK_Mode_Name - (Id : SPARK_Mode_Type) return Name_Id - is - begin - if Id = On then - return Name_On; - elsif Id = Off then - return Name_Off; - elsif Id = Auto then - return Name_Auto; - - -- Mode "None" should never be used in error message generation - - else - raise Program_Error; - end if; - end Get_SPARK_Mode_Name; - -- Start of processing for Do_SPARK_Mode begin @@ -18697,7 +18670,7 @@ package body Sem_Prag is -- Check the legality of the mode (no argument = ON) if Arg_Count = 1 then - Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_Auto); + Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off); Mode := Chars (Get_Pragma_Arg (Arg1)); else Mode := Name_On; @@ -18732,14 +18705,6 @@ package body Sem_Prag is -- The pragma applies to a [library unit] subprogram or package else - -- Mode "Auto" can only be used in a configuration pragma - - if Mode_Id = Auto then - Error_Pragma_Arg - ("mode `Auto` is only allowed when pragma % appears as " - & "a configuration pragma", Arg1); - end if; - -- Verify the placement of the pragma with respect to package -- or subprogram declarations and detect duplicates. @@ -23513,8 +23478,6 @@ package body Sem_Prag is return On; elsif N = Name_Off then return Off; - elsif N = Name_Auto then - return Auto; -- Any other argument is erroneous diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 6321d46..a018dc9 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -688,7 +688,6 @@ package Snames is Name_Assertion : constant Name_Id := N + $; Name_Assertions : constant Name_Id := N + $; Name_Attribute_Name : constant Name_Id := N + $; - Name_Auto : constant Name_Id := N + $; Name_Body_File_Name : constant Name_Id := N + $; Name_Boolean_Entry_Barriers : constant Name_Id := N + $; Name_By_Any : constant Name_Id := N + $; diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index e7df033..b17d799 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -177,6 +177,7 @@ package SPARK_Xrefs is -- m = modification -- r = reference + -- c = reference to constant object -- s = subprogram reference in a static call -- Special entries for reads and writes to memory reference a special @@ -229,6 +230,7 @@ package SPARK_Xrefs is Rtype : Character; -- Indicates type of reference, using code used in ALI file: -- r = reference + -- c = reference to constant object -- m = modification -- s = call -- cgit v1.1