diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 13 | ||||
| -rw-r--r-- | gcc/ada/checks.adb | 7 | ||||
| -rw-r--r-- | gcc/ada/exp_aggr.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/exp_ch7.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/exp_ch9.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/par-prag.adb | 6 | ||||
| -rw-r--r-- | gcc/ada/sem_attr.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/sem_ch12.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 255 | ||||
| -rw-r--r-- | gcc/ada/sem_type.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 247 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 7 |
14 files changed, 292 insertions, 275 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 5be755baf5a..7cc7ff9d410 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,18 @@ 2016-04-19 Arnaud Charlet <charlet@adacore.com> + * sem_prag.adb, sem_attr.adb, par-prag.adb, exp_aggr.adb, sem_type.adb + sem_ch12.adb, sem_ch3.adb, exp_ch7.adb, exp_ch9.adb: Code cleanup. + * sem_res.adb, sem_util.ads, sem_util.adb (Is_OK_Volatile_Context): + Promoted from being a nested subprogram in Sem_Res.Resolve_Entity_Name + to publicly visible routine in Sem_Util. + +2016-04-19 Ed Schonberg <schonberg@adacore.com> + + * checks.adb (Apply_Parameter_Aliasing_Checks): Do not apply + the check if the type of the actual is By_Reference. + +2016-04-19 Arnaud Charlet <charlet@adacore.com> + * sem_res.adb (Within_Subprogram_Call): Detect also nodes that appear in entry calls. (Resolve_Actuals, Insert_Default): Propagate diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index e6eab0c3b0d..eca82d77818 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -2373,7 +2373,10 @@ package body Checks is -- Elementary types are always passed by value, therefore actuals of -- such types cannot lead to aliasing. An aggregate is an object in -- Ada 2012, but an actual that is an aggregate cannot overlap with - -- another actual. + -- another actual. A type that is By_Reference (such as an array of + -- controlled types) is not subject to the check because any update + -- will be done in place and a subsequent read will always see the + -- correct value, see RM 6.2 (12/3). if Nkind (Original_Actual (Actual_1)) = N_Aggregate or else @@ -2385,6 +2388,8 @@ package body Checks is elsif Is_Object_Reference (Original_Actual (Actual_1)) and then not Is_Elementary_Type (Etype (Original_Actual (Actual_1))) + and then + not Is_By_Reference_Type (Etype (Original_Actual (Actual_1))) then Actual_2 := Next_Actual (Actual_1); Formal_2 := Next_Formal (Formal_1); diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index 2ad72bdf5bf..cb97dca4d7c 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -4321,7 +4321,7 @@ package body Exp_Aggr is Decl : Node_Id; Typ : constant Entity_Id := Etype (N); Indexes : constant List_Id := New_List; - Num : Int; + Num : Nat; Sub_Agg : Node_Id; begin @@ -7085,7 +7085,7 @@ package body Exp_Aggr is Byte_Size : constant Int := UI_To_Int (Component_Size (Packed_Array)); -- The packed array type is a byte array - Packed_Num : Int; + Packed_Num : Nat; -- Number of components accumulated in current byte Comps : List_Id; diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 04f28a6da4d..daa5f91c668 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -6227,7 +6227,7 @@ package body Exp_Ch7 is procedure Preprocess_Components (Comps : Node_Id; - Num_Comps : out Int; + Num_Comps : out Nat; Has_POC : out Boolean); -- Examine all components in component list Comps, count all controlled -- components and determine whether at least one of them is per-object @@ -6265,7 +6265,7 @@ package body Exp_Ch7 is Decl_Id : Entity_Id; Decl_Typ : Entity_Id; Has_POC : Boolean; - Num_Comps : Int; + Num_Comps : Nat; procedure Process_Component_For_Adjust (Decl : Node_Id); -- Process the declaration of a single controlled component @@ -6679,7 +6679,7 @@ package body Exp_Ch7 is Jump_Block : Node_Id; Label : Node_Id; Label_Id : Entity_Id; - Num_Comps : Int; + Num_Comps : Nat; Stmts : List_Id; procedure Process_Component_For_Finalize @@ -7236,7 +7236,7 @@ package body Exp_Ch7 is procedure Preprocess_Components (Comps : Node_Id; - Num_Comps : out Int; + Num_Comps : out Nat; Has_POC : out Boolean) is Decl : Node_Id; diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 11b614b2483..faa1d8cafd0 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -10590,7 +10590,7 @@ package body Exp_Ch9 is End_Lab : Node_Id; Index : Pos := 1; Lab : Node_Id; - Num_Alts : Int; + Num_Alts : Nat; Num_Accept : Nat := 0; Proc : Node_Id; Time_Type : Entity_Id; diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index c317949d7c2..123f9090ff7 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -974,13 +974,13 @@ begin declare Slen : constant Natural := Natural (String_Length (S)); Options : String (1 .. Slen); - J : Natural; - Ptr : Natural; + J : Positive; + Ptr : Positive; begin J := 1; loop - C := Get_String_Char (S, Int (J)); + C := Get_String_Char (S, Pos (J)); if not In_Character_Range (C) then OK := False; diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 17f06f3e483..fa44c1d96d6 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -6041,7 +6041,7 @@ package body Sem_Attr is Start_String; for J in 1 .. String_Length (Full_Name) - 1 loop - Store_String_Char (Get_String_Char (Full_Name, Int (J))); + Store_String_Char (Get_String_Char (Full_Name, Pos (J))); end loop; Store_String_Chars ("'Type_Key"); diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 40433fd2e7a..084335c472d 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -15117,7 +15117,7 @@ package body Sem_Ch12 is T : constant Entity_Id := Entity (Prefix (Def)); Is_Fun : constant Boolean := (Ekind (Nam) = E_Function); F : Entity_Id; - Num_F : Int; + Num_F : Nat; OK : Boolean; begin diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index f41b8e99b0c..f2e111536cd 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -13871,8 +13871,8 @@ package body Sem_Ch3 is -- Inherit the discriminants of the parent type Add_Discriminants : declare - Num_Disc : Int; - Num_Gird : Int; + Num_Disc : Nat; + Num_Gird : Nat; begin Num_Disc := 0; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index e965976a691..289cfc8274a 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -21242,12 +21242,12 @@ package body Sem_Prag is declare Slen : constant Natural := Natural (String_Length (S)); Options : String (1 .. Slen); - J : Natural; + J : Positive; begin J := 1; loop - C := Get_String_Char (S, Int (J)); + C := Get_String_Char (S, Pos (J)); exit when not In_Character_Range (C); Options (J) := Get_Character (C); @@ -22592,14 +22592,14 @@ package body Sem_Prag is declare Slen : constant Natural := Natural (String_Length (S)); Options : String (1 .. Slen); - J : Natural; + J : Positive; begin -- Couldn't we use a for loop here over Options'Range??? J := 1; loop - C := Get_String_Char (S, Int (J)); + C := Get_String_Char (S, Pos (J)); -- This is a weird test, it skips setting validity -- checks entirely if any element of S is out of diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 0bac1eb1816..85bf0c40963 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6820,13 +6820,6 @@ package body Sem_Res is -- Determine whether node Context denotes an assignment statement or an -- object declaration whose expression is node Expr. - function Is_OK_Volatile_Context - (Context : Node_Id; - Obj_Ref : Node_Id) return Boolean; - -- Determine whether node Context denotes a "non-interfering context" - -- (as defined in SPARK RM 7.1.3(12)) where volatile reference Obj_Ref - -- can safely reside. - ---------------------------------------- -- Is_Assignment_Or_Object_Expression -- ---------------------------------------- @@ -6869,254 +6862,6 @@ package body Sem_Res is end if; end Is_Assignment_Or_Object_Expression; - ---------------------------- - -- Is_OK_Volatile_Context -- - ---------------------------- - - function Is_OK_Volatile_Context - (Context : Node_Id; - Obj_Ref : Node_Id) return Boolean - is - function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean; - -- Determine whether an arbitrary node denotes a call to a protected - -- entry, function or procedure in prefixed form where the prefix is - -- Obj_Ref. - - function Within_Check (Nod : Node_Id) return Boolean; - -- Determine whether an arbitrary node appears in a check node - - function Within_Subprogram_Call (Nod : Node_Id) return Boolean; - -- Determine whether an arbitrary node appears in a subprogram call - - function Within_Volatile_Function (Id : Entity_Id) return Boolean; - -- Determine whether an arbitrary entity appears in a volatile - -- function. - - --------------------------------- - -- Is_Protected_Operation_Call -- - --------------------------------- - - function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean is - Pref : Node_Id; - Subp : Node_Id; - - begin - -- A call to a protected operations retains its selected component - -- form as opposed to other prefixed calls that are transformed in - -- expanded names. - - if Nkind (Nod) = N_Selected_Component then - Pref := Prefix (Nod); - Subp := Selector_Name (Nod); - - return - Pref = Obj_Ref - and then Present (Etype (Pref)) - and then Is_Protected_Type (Etype (Pref)) - and then Is_Entity_Name (Subp) - and then Present (Entity (Subp)) - and then Ekind_In (Entity (Subp), E_Entry, - E_Entry_Family, - E_Function, - E_Procedure); - else - return False; - end if; - end Is_Protected_Operation_Call; - - ------------------ - -- Within_Check -- - ------------------ - - function Within_Check (Nod : Node_Id) return Boolean is - Par : Node_Id; - - begin - -- Climb the parent chain looking for a check node - - Par := Nod; - while Present (Par) loop - if Nkind (Par) in N_Raise_xxx_Error then - return True; - - -- Prevent the search from going too far - - elsif Is_Body_Or_Package_Declaration (Par) then - exit; - end if; - - Par := Parent (Par); - end loop; - - return False; - end Within_Check; - - ---------------------------- - -- Within_Subprogram_Call -- - ---------------------------- - - function Within_Subprogram_Call (Nod : Node_Id) return Boolean is - Par : Node_Id; - - begin - -- Climb the parent chain looking for a function or procedure call - - Par := Nod; - while Present (Par) loop - if Nkind_In (Par, N_Function_Call, - N_Procedure_Call_Statement, - N_Entry_Call_Statement) - then - return True; - - -- Prevent the search from going too far - - elsif Is_Body_Or_Package_Declaration (Par) then - exit; - end if; - - Par := Parent (Par); - end loop; - - return False; - end Within_Subprogram_Call; - - ------------------------------ - -- Within_Volatile_Function -- - ------------------------------ - - function Within_Volatile_Function (Id : Entity_Id) return Boolean is - Func_Id : Entity_Id; - - begin - -- Traverse the scope stack looking for a [generic] function - - Func_Id := Id; - while Present (Func_Id) and then Func_Id /= Standard_Standard loop - if Ekind_In (Func_Id, E_Function, E_Generic_Function) then - return Is_Volatile_Function (Func_Id); - end if; - - Func_Id := Scope (Func_Id); - end loop; - - return False; - end Within_Volatile_Function; - - -- Local variables - - Obj_Id : Entity_Id; - - -- Start of processing for Is_OK_Volatile_Context - - begin - -- The volatile object appears on either side of an assignment - - if Nkind (Context) = N_Assignment_Statement then - return True; - - -- The volatile object is part of the initialization expression of - -- another object. - - elsif Nkind (Context) = N_Object_Declaration - and then Present (Expression (Context)) - and then Expression (Context) = Obj_Ref - then - Obj_Id := Defining_Entity (Context); - - -- The volatile object acts as the initialization expression of an - -- extended return statement. This is valid context as long as the - -- function is volatile. - - if Is_Return_Object (Obj_Id) then - return Within_Volatile_Function (Obj_Id); - - -- Otherwise this is a normal object initialization - - else - return True; - end if; - - -- The volatile object acts as the name of a renaming declaration - - elsif Nkind (Context) = N_Object_Renaming_Declaration - and then Name (Context) = Obj_Ref - then - return True; - - -- The volatile object appears as an actual parameter in a call to an - -- instance of Unchecked_Conversion whose result is renamed. - - elsif Nkind (Context) = N_Function_Call - and then Is_Entity_Name (Name (Context)) - and then Is_Unchecked_Conversion_Instance (Entity (Name (Context))) - and then Nkind (Parent (Context)) = N_Object_Renaming_Declaration - then - return True; - - -- The volatile object is actually the prefix in a protected entry, - -- function, or procedure call. - - elsif Is_Protected_Operation_Call (Context) then - return True; - - -- The volatile object appears as the expression of a simple return - -- statement that applies to a volatile function. - - elsif Nkind (Context) = N_Simple_Return_Statement - and then Expression (Context) = Obj_Ref - then - return - Within_Volatile_Function (Return_Statement_Entity (Context)); - - -- The volatile object appears as the prefix of a name occurring - -- in a non-interfering context. - - elsif Nkind_In (Context, N_Attribute_Reference, - N_Explicit_Dereference, - N_Indexed_Component, - N_Selected_Component, - N_Slice) - and then Prefix (Context) = Obj_Ref - and then Is_OK_Volatile_Context - (Context => Parent (Context), - Obj_Ref => Context) - then - return True; - - -- The volatile object appears as the expression of a type conversion - -- occurring in a non-interfering context. - - elsif Nkind_In (Context, N_Type_Conversion, - N_Unchecked_Type_Conversion) - and then Expression (Context) = Obj_Ref - and then Is_OK_Volatile_Context - (Context => Parent (Context), - Obj_Ref => Context) - then - return True; - - -- Allow references to volatile objects in various checks. This is - -- not a direct SPARK 2014 requirement. - - elsif Within_Check (Context) then - return True; - - -- Assume that references to effectively volatile objects that appear - -- as actual parameters in a subprogram call are always legal. A full - -- legality check is done when the actuals are resolved. - - elsif Within_Subprogram_Call (Context) then - return True; - - -- Otherwise the context is not suitable for an effectively volatile - -- object. - - else - return False; - end if; - end Is_OK_Volatile_Context; - -- Local variables E : constant Entity_Id := Entity (N); diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb index eddc54b8baa..a648bfa5837 100644 --- a/gcc/ada/sem_type.adb +++ b/gcc/ada/sem_type.adb @@ -3029,7 +3029,7 @@ package body Sem_Type is Op_Name : constant Name_Id := Chars (Op); T : constant Entity_Id := Etype (New_S); New_F : Entity_Id; - Num : Int; + Num : Nat; Old_F : Entity_Id; T1 : Entity_Id; T2 : Entity_Id; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 29d2e42592d..d4a276ca5d8 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -13010,6 +13010,253 @@ package body Sem_Util is end if; end Is_OK_Variable_For_Out_Formal; + ---------------------------- + -- Is_OK_Volatile_Context -- + ---------------------------- + + function Is_OK_Volatile_Context + (Context : Node_Id; + Obj_Ref : Node_Id) return Boolean + is + function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean; + -- Determine whether an arbitrary node denotes a call to a protected + -- entry, function or procedure in prefixed form where the prefix is + -- Obj_Ref. + + function Within_Check (Nod : Node_Id) return Boolean; + -- Determine whether an arbitrary node appears in a check node + + function Within_Subprogram_Call (Nod : Node_Id) return Boolean; + -- Determine whether an arbitrary node appears in a procedure call + + function Within_Volatile_Function (Id : Entity_Id) return Boolean; + -- Determine whether an arbitrary entity appears in a volatile function + + --------------------------------- + -- Is_Protected_Operation_Call -- + --------------------------------- + + function Is_Protected_Operation_Call (Nod : Node_Id) return Boolean is + Pref : Node_Id; + Subp : Node_Id; + + begin + -- A call to a protected operations retains its selected component + -- form as opposed to other prefixed calls that are transformed in + -- expanded names. + + if Nkind (Nod) = N_Selected_Component then + Pref := Prefix (Nod); + Subp := Selector_Name (Nod); + + return + Pref = Obj_Ref + and then Present (Etype (Pref)) + and then Is_Protected_Type (Etype (Pref)) + and then Is_Entity_Name (Subp) + and then Present (Entity (Subp)) + and then Ekind_In (Entity (Subp), E_Entry, + E_Entry_Family, + E_Function, + E_Procedure); + else + return False; + end if; + end Is_Protected_Operation_Call; + + ------------------ + -- Within_Check -- + ------------------ + + function Within_Check (Nod : Node_Id) return Boolean is + Par : Node_Id; + + begin + -- Climb the parent chain looking for a check node + + Par := Nod; + while Present (Par) loop + if Nkind (Par) in N_Raise_xxx_Error then + return True; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Par) then + exit; + end if; + + Par := Parent (Par); + end loop; + + return False; + end Within_Check; + + ---------------------------- + -- Within_Subprogram_Call -- + ---------------------------- + + function Within_Subprogram_Call (Nod : Node_Id) return Boolean is + Par : Node_Id; + + begin + -- Climb the parent chain looking for a function or procedure call + + Par := Nod; + while Present (Par) loop + if Nkind_In (Par, N_Function_Call, + N_Procedure_Call_Statement, + N_Entry_Call_Statement) + then + return True; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Par) then + exit; + end if; + + Par := Parent (Par); + end loop; + + return False; + end Within_Subprogram_Call; + + ------------------------------ + -- Within_Volatile_Function -- + ------------------------------ + + function Within_Volatile_Function (Id : Entity_Id) return Boolean is + Func_Id : Entity_Id; + + begin + -- Traverse the scope stack looking for a [generic] function + + Func_Id := Id; + while Present (Func_Id) and then Func_Id /= Standard_Standard loop + if Ekind_In (Func_Id, E_Function, E_Generic_Function) then + return Is_Volatile_Function (Func_Id); + end if; + + Func_Id := Scope (Func_Id); + end loop; + + return False; + end Within_Volatile_Function; + + -- Local variables + + Obj_Id : Entity_Id; + + -- Start of processing for Is_OK_Volatile_Context + + begin + -- The volatile object appears on either side of an assignment + + if Nkind (Context) = N_Assignment_Statement then + return True; + + -- The volatile object is part of the initialization expression of + -- another object. + + elsif Nkind (Context) = N_Object_Declaration + and then Present (Expression (Context)) + and then Expression (Context) = Obj_Ref + then + Obj_Id := Defining_Entity (Context); + + -- The volatile object acts as the initialization expression of an + -- extended return statement. This is valid context as long as the + -- function is volatile. + + if Is_Return_Object (Obj_Id) then + return Within_Volatile_Function (Obj_Id); + + -- Otherwise this is a normal object initialization + + else + return True; + end if; + + -- The volatile object acts as the name of a renaming declaration + + elsif Nkind (Context) = N_Object_Renaming_Declaration + and then Name (Context) = Obj_Ref + then + return True; + + -- The volatile object appears as an actual parameter in a call to an + -- instance of Unchecked_Conversion whose result is renamed. + + elsif Nkind (Context) = N_Function_Call + and then Is_Entity_Name (Name (Context)) + and then Is_Unchecked_Conversion_Instance (Entity (Name (Context))) + and then Nkind (Parent (Context)) = N_Object_Renaming_Declaration + then + return True; + + -- The volatile object is actually the prefix in a protected entry, + -- function, or procedure call. + + elsif Is_Protected_Operation_Call (Context) then + return True; + + -- The volatile object appears as the expression of a simple return + -- statement that applies to a volatile function. + + elsif Nkind (Context) = N_Simple_Return_Statement + and then Expression (Context) = Obj_Ref + then + return + Within_Volatile_Function (Return_Statement_Entity (Context)); + + -- The volatile object appears as the prefix of a name occurring in a + -- non-interfering context. + + elsif Nkind_In (Context, N_Attribute_Reference, + N_Explicit_Dereference, + N_Indexed_Component, + N_Selected_Component, + N_Slice) + and then Prefix (Context) = Obj_Ref + and then Is_OK_Volatile_Context + (Context => Parent (Context), + Obj_Ref => Context) + then + return True; + + -- The volatile object appears as the expression of a type conversion + -- occurring in a non-interfering context. + + elsif Nkind_In (Context, N_Type_Conversion, + N_Unchecked_Type_Conversion) + and then Expression (Context) = Obj_Ref + and then Is_OK_Volatile_Context + (Context => Parent (Context), + Obj_Ref => Context) + then + return True; + + -- Allow references to volatile objects in various checks. This is + -- not a direct SPARK 2014 requirement. + + elsif Within_Check (Context) then + return True; + + -- Assume that references to effectively volatile objects that appear + -- as actual parameters in a subprogram call are always legal. A full + -- legality check is done when the actuals are resolved. + + elsif Within_Subprogram_Call (Context) then + return True; + + -- Otherwise the context is not suitable for an effectively volatile + -- object. + + else + return False; + end if; + end Is_OK_Volatile_Context; + ------------------------------------ -- Is_Package_Contract_Annotation -- ------------------------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index df475ccb8b1..4575077fead 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1474,6 +1474,13 @@ package Sem_Util is -- the Is_Variable sense) with an untagged type target are considered view -- conversions and hence variables. + function Is_OK_Volatile_Context + (Context : Node_Id; + Obj_Ref : Node_Id) return Boolean; + -- Determine whether node Context denotes a "non-interfering context" (as + -- defined in SPARK RM 7.1.3(12)) where volatile reference Obj_Ref can + -- safely reside. + function Is_Package_Contract_Annotation (Item : Node_Id) return Boolean; -- Determine whether aspect specification or pragma Item is one of the -- following package contract annotations: |