+2014-01-27 Thomas Quinot <quinot@adacore.com>
+
+ * exp_ch7.adb: Minor reformatting.
+
+2014-01-27 Robert Dewar <dewar@adacore.com>
+
+ * 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 <dewar@adacore.com>
+
+ * 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 <dewar@adacore.com>
+
+ * exp_aggr.adb (Check_Bounds): Reason is range check, not
+ length check.
+
+2014-01-27 Yannick Moy <moy@adacore.com>
+
+ * 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 <quinot@adacore.com>
+
+ * 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 <quinot@adacore.com>
* exp_smem.adb (Expand_Shared_Passive_Variable): For a reference
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;
-- 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);
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;
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
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;
pragma Assert
(Rtype = 'r' or else
+ Rtype = 'c' or else
Rtype = 'm' or else
Rtype = 's');
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
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))
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 --
--------
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
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
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,
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;
Assertions_Enabled := False;
Assume_No_Invalid_Values := False;
Check_Policy_List := Empty;
- SPARK_Mode := Off;
+ SPARK_Mode := None;
SPARK_Mode_Pragma := Empty;
end if;
-- 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
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
-- --
-- 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- --
------------------------
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
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 --
---------------------------------
-- 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;
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 --
------------------------------
-- 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;
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
-- 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;
-- 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.
return On;
elsif N = Name_Off then
return Off;
- elsif N = Name_Auto then
- return Auto;
-- Any other argument is erroneous
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 + $;
-- 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
Rtype : Character;
-- Indicates type of reference, using code used in ALI file:
-- r = reference
+ -- c = reference to constant object
-- m = modification
-- s = call
projects / thirdparty / gcc.git / commitdiff
