From 24fd21c393d671989c45f53fcfb0f489d9ca768e Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 26 Oct 2015 12:31:06 +0100 Subject: [PATCH] [multiple changes] 2015-10-26 Yannick Moy * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Use character 'r' to denote a reference to a constant which may have variable input, and thus may be treated as a variable in GNATprove, instead of the character 'c' used for constants. 2015-10-26 Ed Schonberg * sem_util.adb (Object_Access_Level): Only aliased formals of functions have the accessibility level of the point of call; aliased formals of procedures have the same level as unaliased formals. (New_Copy_Tree): Add guard on copying itypes. From code reading. From-SVN: r229337 --- gcc/ada/ChangeLog | 15 +++ gcc/ada/lib-xref-spark_specific.adb | 144 ++++++++++++++++++---------- gcc/ada/sem_util.adb | 18 +++- 3 files changed, 123 insertions(+), 54 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 81c2c0b407b..f2deda17c4e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,18 @@ +2015-10-26 Yannick Moy + + * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Use character 'r' to + denote a reference to a constant which may have variable input, and + thus may be treated as a variable in GNATprove, instead of the + character 'c' used for constants. + +2015-10-26 Ed Schonberg + + * sem_util.adb (Object_Access_Level): Only aliased formals of + functions have the accessibility level of the point of call; + aliased formals of procedures have the same level as unaliased + formals. + (New_Copy_Tree): Add guard on copying itypes. From code reading. + 2015-10-26 Hristian Kirtchev * inline.adb: Minor reformatting. diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 7ed6f7b9101..a53942d59f9 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -272,9 +272,7 @@ package body SPARK_Specific is => Typ := Xref_Entity_Letters (Ekind (E)); - when E_Package_Body - | E_Subprogram_Body - => + when E_Package_Body | E_Subprogram_Body => Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E))); when E_Void => @@ -317,6 +315,16 @@ package body SPARK_Specific is function Get_Entity_Type (E : Entity_Id) return Character; -- Return a character representing the type of entity + function Is_Constant_Object_Without_Variable_Input + (E : Entity_Id) return Boolean; + -- Return True if E is known to have no variable input, as defined in + -- SPARK RM. + + function Is_Future_Scope_Entity + (E : Entity_Id; + S : Scope_Index) return Boolean; + -- Check whether entity E is in SPARK_Scope_Table at index S or higher + function Is_SPARK_Reference (E : Entity_Id; Typ : Character) return Boolean; @@ -327,11 +335,6 @@ package body SPARK_Specific is -- Return whether the entity or reference scope meets requirements for -- being an SPARK scope. - function Is_Future_Scope_Entity - (E : Entity_Id; - S : Scope_Index) return Boolean; - -- Check whether entity E is in SPARK_Scope_Table at index S or higher - function Lt (Op1 : Natural; Op2 : Natural) return Boolean; -- Comparison function for Sort call @@ -418,48 +421,47 @@ package body SPARK_Specific is return Scopes.Get (N).Num; end Get_Scope_Num; - ------------------------ - -- Is_SPARK_Reference -- - ------------------------ + ----------------------------------------------- + -- Is_Constant_Object_Without_Variable_Input -- + ----------------------------------------------- - function Is_SPARK_Reference - (E : Entity_Id; - Typ : Character) return Boolean + function Is_Constant_Object_Without_Variable_Input + (E : Entity_Id) return Boolean is + Result : Boolean; + begin - -- The only references of interest on callable entities are calls. On - -- non-callable entities, the only references of interest are reads - -- and writes. + case Ekind (E) is - if Ekind (E) in Overloadable_Kind then - return Typ = 's'; + -- A constant is known to have no variable input if its + -- initializing expression is static (a value which is + -- compile-time-known is not guaranteed to have no variable input + -- as defined in the SPARK RM). Otherwise, the constant may or not + -- have variable input. - -- Objects of Task type or protected type are not SPARK references + when E_Constant => + declare + Decl : Node_Id; + begin + if Present (Full_View (E)) then + Decl := Parent (Full_View (E)); + else + Decl := Parent (E); + end if; - elsif Present (Etype (E)) - and then Ekind (Etype (E)) in Concurrent_Kind - then - return False; + pragma Assert (Present (Expression (Decl))); + Result := Is_Static_Expression (Expression (Decl)); + end; - -- In all other cases, result is true for reference/modify cases, - -- and false for all other cases. + when E_Loop_Parameter | E_In_Parameter => + Result := True; - else - return Typ = 'r' or else Typ = 'm'; - end if; - end Is_SPARK_Reference; + when others => + Result := False; + end case; - -------------------- - -- Is_SPARK_Scope -- - -------------------- - - function Is_SPARK_Scope (E : Entity_Id) return Boolean is - begin - return Present (E) - and then not Is_Generic_Unit (E) - and then Renamed_Entity (E) = Empty - and then Get_Scope_Num (E) /= No_Scope; - end Is_SPARK_Scope; + return Result; + end Is_Constant_Object_Without_Variable_Input; ---------------------------- -- Is_Future_Scope_Entity -- @@ -511,6 +513,49 @@ package body SPARK_Specific is return False; end Is_Future_Scope_Entity; + ------------------------ + -- Is_SPARK_Reference -- + ------------------------ + + function Is_SPARK_Reference + (E : Entity_Id; + Typ : Character) return Boolean + is + begin + -- The only references of interest on callable entities are calls. On + -- non-callable entities, the only references of interest are reads + -- and writes. + + if Ekind (E) in Overloadable_Kind then + return Typ = 's'; + + -- Objects of Task type or protected type are not SPARK references + + elsif Present (Etype (E)) + and then Ekind (Etype (E)) in Concurrent_Kind + then + return False; + + -- In all other cases, result is true for reference/modify cases, + -- and false for all other cases. + + else + return Typ = 'r' or else Typ = 'm'; + end if; + end Is_SPARK_Reference; + + -------------------- + -- Is_SPARK_Scope -- + -------------------- + + function Is_SPARK_Scope (E : Entity_Id) return Boolean is + begin + return Present (E) + and then not Is_Generic_Unit (E) + and then Renamed_Entity (E) = Empty + and then Get_Scope_Num (E) /= No_Scope; + end Is_SPARK_Scope; + -------- -- Lt -- -------- @@ -819,12 +864,15 @@ 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. + -- References to constant objects without variable inputs (see + -- SPARK RM 3.3.1) 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. Other constants may + -- later be treated the same, up to GNATprove to decide based on + -- its flow analysis. - if Is_Constant_Object (Ref.Ent) then + if Is_Constant_Object_Without_Variable_Input (Ref.Ent) then Typ := 'c'; else Typ := Ref.Typ; @@ -1230,9 +1278,7 @@ package body SPARK_Specific is when N_Subprogram_Declaration => null; - when N_Entry_Body - | N_Subprogram_Body - => + when N_Entry_Body | N_Subprogram_Body => if not Is_Generic_Subprogram (Defining_Entity (N)) then Traverse_Subprogram_Body (N, Process, Inside_Stubs); end if; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 2332bb32ab7..464619a2061 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -15330,7 +15330,10 @@ package body Sem_Util is while Present (Elmt) loop Next_Elmt (Elmt); New_Itype := Node (Elmt); - Copy_Itype_With_Replacement (New_Itype); + + if Is_Itype (New_Itype) then + Copy_Itype_With_Replacement (New_Itype); + end if; Next_Elmt (Elmt); end loop; end; @@ -16041,10 +16044,15 @@ package body Sem_Util is return Type_Access_Level (Scope (E)) + 1; else - -- Aliased formals take their access level from the point of call. - -- This is smaller than the level of the subprogram itself. - - if Is_Formal (E) and then Is_Aliased (E) then + -- Aliased formals of functions take their access level from the + -- point of call, i.e. require a dynamic check. For static check + -- purposes, this is smaller than the level of the subprogram + -- itself. For procedures the aliased makes no difference. + + if Is_Formal (E) + and then Is_Aliased (E) + and then Ekind (Scope (E)) = E_Function + then return Type_Access_Level (Etype (E)); else -- 2.30.2