From 933aa0ac81ee62b104969294ce6ab117e1602968 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 18 Apr 2016 12:24:03 +0200 Subject: [multiple changes] 2016-04-18 Hristian Kirtchev * sem_res.adb (Is_Protected_Operation_Call): Add guards to account for a non-decorated selected component. 2016-04-18 Yannick Moy * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve implementation of Body_Has_SPARK_Mode_On. * sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_From_Annotation): New function replacing previous Get_SPARK_Mode_From_Pragma, that deals also with aspects. (Get_SPARK_Mode_Type): Make function internal again. * inline.adb, sem_ch7.adb, sem_util.adb: Use new Get_SPARK_Mode_From_Annotation. From-SVN: r235116 --- gcc/ada/ChangeLog | 16 ++++++++++++++++ gcc/ada/inline.adb | 3 ++- gcc/ada/sem_ch6.adb | 32 ++++++++++++++++++------------- gcc/ada/sem_ch7.adb | 7 ++++--- gcc/ada/sem_prag.adb | 54 +++++++++++++++++++++++++++++++++++----------------- gcc/ada/sem_prag.ads | 10 +++------- gcc/ada/sem_res.adb | 2 ++ gcc/ada/sem_util.adb | 2 +- 8 files changed, 84 insertions(+), 42 deletions(-) (limited to 'gcc/ada') diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9691433..fd8d79a 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,21 @@ 2016-04-18 Hristian Kirtchev + * sem_res.adb (Is_Protected_Operation_Call): + Add guards to account for a non-decorated selected component. + +2016-04-18 Yannick Moy + + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve + implementation of Body_Has_SPARK_Mode_On. + * sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_From_Annotation): + New function replacing previous Get_SPARK_Mode_From_Pragma, that + deals also with aspects. + (Get_SPARK_Mode_Type): Make function internal again. + * inline.adb, sem_ch7.adb, sem_util.adb: Use new + Get_SPARK_Mode_From_Annotation. + +2016-04-18 Hristian Kirtchev + * contracts.adb (Analyze_Object_Contract): Update references to SPARK RM. * freeze.adb (Freeze_Entity): Update references to SPARK RM. diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 9a7b375..b3b5aba 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1553,7 +1553,8 @@ package body Inline is elsif Present (Spec_Id) and then (No (SPARK_Pragma (Spec_Id)) - or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On) + or else + Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) /= On) then return False; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 17c2623..9563320 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -2292,11 +2292,7 @@ package body Sem_Ch6 is Item := First (Aspect_Specifications (N)); while Present (Item) loop if Get_Aspect_Id (Item) = Aspect_SPARK_Mode then - return No (Expression (Item)) - or else - (Nkind (Expression (Item)) = N_Identifier - and then - Get_SPARK_Mode_Type (Chars (Expression (Item))) = On); + return Get_SPARK_Mode_From_Annotation (Item) = On; end if; Next (Item); @@ -2308,18 +2304,28 @@ package body Sem_Ch6 is if Present (Decls) then Item := First (Decls); while Present (Item) loop - if Nkind (Item) = N_Pragma - and then Get_Pragma_Id (Item) = Pragma_SPARK_Mode - then - return Get_SPARK_Mode_From_Pragma (Item) = On; + + -- Pragmas that apply to a subprogram body are usually grouped + -- together. Look for a potential pragma SPARK_Mode among them. + + if Nkind (Item) = N_Pragma then + if Get_Pragma_Id (Item) = Pragma_SPARK_Mode then + return Get_SPARK_Mode_From_Annotation (Item) = On; + end if; + + -- Otherwise the first non-pragma declarative item terminates + -- the region where pragma SPARK_Mode may appear. + + else + exit; end if; Next (Item); end loop; end if; - -- Applicable SPARK_Mode is inherited from the enclosing subprogram - -- or package. + -- Otherwise, the applicable SPARK_Mode is inherited from the + -- enclosing subprogram or package. return SPARK_Mode = On; end Body_Has_SPARK_Mode_On; @@ -3849,9 +3855,9 @@ package body Sem_Ch6 is if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then if Present (SPARK_Pragma (Spec_Id)) then - if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off + if Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) = Off and then - Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On + Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = On then Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); Error_Msg_N ("incorrect application of SPARK_Mode#", N); diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index e182771..b332f20 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -777,9 +777,10 @@ package body Sem_Ch7 is if Present (SPARK_Pragma (Body_Id)) then if Present (SPARK_Aux_Pragma (Spec_Id)) then - if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off - and then - Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On + if Get_SPARK_Mode_From_Annotation (SPARK_Aux_Pragma (Spec_Id)) = + Off + and then + Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = On then Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); Error_Msg_N ("incorrect application of SPARK_Mode#", N); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index e951804..7be7172 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -235,6 +235,11 @@ package body Sem_Prag is -- original one, following the renaming chain) is returned. Otherwise the -- entity is returned unchanged. Should be in Einfo??? + function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type; + -- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram + -- Get_SPARK_Mode_From_Annotation. Convert a name into a corresponding + -- value of type SPARK_Mode_Type. + function Has_Extra_Parentheses (Clause : Node_Id) return Boolean; -- Subsidiary to the analysis of pragmas Depends and Refined_Depends. -- Determine whether dependency clause Clause is surrounded by extra @@ -20338,8 +20343,8 @@ package body Sem_Prag is -- Issue an error if the new mode is less restrictive than -- that of the context. - if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off - and then Get_SPARK_Mode_From_Pragma (N) = On + if Get_SPARK_Mode_From_Annotation (Context_Pragma) = Off + and then Get_SPARK_Mode_From_Annotation (N) = On then Error_Msg_N ("cannot change SPARK_Mode from Off to On", Err_N); @@ -20376,8 +20381,8 @@ package body Sem_Prag is -- Issue an error if the new mode is less restrictive -- than that of the initial declaration. - if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off - and then Get_SPARK_Mode_From_Pragma (N) = On + if Get_SPARK_Mode_From_Annotation (Entity_Pragma) = Off + and then Get_SPARK_Mode_From_Annotation (N) = On then Error_Msg_N ("incorrect use of SPARK_Mode", Err_N); Error_Msg_Sloc := Sloc (Entity_Pragma); @@ -27553,30 +27558,45 @@ package body Sem_Prag is end if; end Get_SPARK_Mode_Type; - -------------------------------- - -- Get_SPARK_Mode_From_Pragma -- - -------------------------------- + ------------------------------------ + -- Get_SPARK_Mode_From_Annotation -- + ------------------------------------ - function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type is - Args : List_Id; + function Get_SPARK_Mode_From_Annotation + (N : Node_Id) return SPARK_Mode_Type + is Mode : Node_Id; begin - pragma Assert (Nkind (N) = N_Pragma); - Args := Pragma_Argument_Associations (N); + if Nkind (N) = N_Aspect_Specification then + Mode := Expression (N); - -- Extract the mode from the argument list - - if Present (Args) then + else pragma Assert (Nkind (N) = N_Pragma); Mode := First (Pragma_Argument_Associations (N)); - return Get_SPARK_Mode_Type (Chars (Get_Pragma_Arg (Mode))); - -- If SPARK_Mode pragma has no argument, default is ON + if Present (Mode) then + Mode := Get_Pragma_Arg (Mode); + end if; + end if; + + -- Aspect or pragma SPARK_Mode specifies an explicit mode + + if Present (Mode) then + if Nkind (Mode) = N_Identifier then + return Get_SPARK_Mode_Type (Chars (Mode)); + + -- In case of a malformed aspect or pragma, return the default None + + else + return None; + end if; + + -- Otherwise the lack of an expression defaults SPARK_Mode to On else return On; end if; - end Get_SPARK_Mode_From_Pragma; + end Get_SPARK_Mode_From_Annotation; --------------------------- -- Has_Extra_Parentheses -- diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 063e7df..a78478e 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -397,13 +397,9 @@ package Sem_Prag is -- Context denotes the entity of the function, package or procedure where -- Prag resides. - function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type; - -- Given a pragma SPARK_Mode node, return corresponding mode id - - function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type; - -- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram - -- Get_SPARK_Mode_From_Pragma. Convert a name into a corresponding value - -- of type SPARK_Mode_Type. + function Get_SPARK_Mode_From_Annotation + (N : Node_Id) return SPARK_Mode_Type; + -- Given an aspect or pragma SPARK_Mode node, return corresponding mode id procedure Initialize; -- Initializes data structures used for pragma processing. Must be called diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 18794c8..c12356c 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6895,8 +6895,10 @@ package body Sem_Res is 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, diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 7bfe724..1146b9d 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -18645,7 +18645,7 @@ package body Sem_Util is null; elsif Present (SPARK_Pragma (Context)) then - SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Context)); + SPARK_Mode := Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Context)); end if; end Save_SPARK_Mode_And_Set; -- cgit v1.1