diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 29 | ||||
| -rw-r--r-- | gcc/ada/opt.ads | 56 | ||||
| -rw-r--r-- | gcc/ada/sem_ch12.adb | 30 | ||||
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 19 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 16 | ||||
| -rw-r--r-- | gcc/ada/sem_ch7.adb | 6 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 291 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 147 | ||||
| -rw-r--r-- | gcc/ada/sem_util.ads | 9 |
9 files changed, 391 insertions, 212 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index affb324903b..8bed0123c2e 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,32 @@ +2014-08-04 Hristian Kirtchev <kirtchev@adacore.com> + + * opt.ads Alphabetize various global flags. New flag + Ignore_Pragma_SPARK_Mode along with a comment on usage. + * sem_ch6.adb (Analyze_Generic_Subprogram_Body): + Pragma SPARK_Mode is now allowed in generic units. + (Analyze_Subprogram_Body_Helper): Do not verify the compatibility + between the SPARK_Mode of a spec and that of a body when inside + a generic. + * sem_ch7.adb (Analyze_Package_Body_Helper): Do not verify the + compatibility between the SPARK_Mode of a spec and that of a + body when inside a generic. + * sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): + Pragma SPARK_Mode is now allowed in generic units. + (Analyze_Package_Instantiation): Save and restore the value of + flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set + the governing SPARK_Mode before analyzing the instance. + (Analyze_Subprogram_Instantiation): Save and restore the value + of flag Ignore_ Pragma_SPARK_Mode in a stack-like fasion. Set + the governing SPARK_Mode before analyzing the instance. + * sem_ch13.adb (Analyze_Aspect_Specifications): Emulate the + placement of a source pragma when inserting the generated pragma + for aspect SPARK_Mode. + * sem_prag.adb (Analyze_Pragma): Reimplement the handling of + pragma SPARK_Mode to allow for generics and their respective + instantiations. + * sem_util.ads, sem_util.adb (Check_SPARK_Mode_In_Generic): Removed. + (Set_Ignore_Pragma_SPARK_Mode): New routine. + 2014-08-04 Eric Botcazou <ebotcazou@adacore.com> * gcc-interface/decl.c (gnat_to_gnu_entity) <E_Component>: Deal with diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index f056f3985d1..2e00d4aa995 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -648,6 +648,20 @@ package Opt is -- GNAT -- Disable generation of ALI file + Follow_Links_For_Files : Boolean := False; + -- PROJECT MANAGER + -- Set to True (-eL) to process the project files in trusted mode. If + -- Follow_Links is False, it is assumed that the project doesn't contain + -- any file duplicated through symbolic links (although the latter are + -- still valid if they point to a file which is outside of the project), + -- and that no directory has a name which is a valid source name. + + Follow_Links_For_Dirs : Boolean := False; + -- PROJECT MANAGER + -- Set to True if directories can be links in this project, and therefore + -- additional system calls must be performed to ensure that we always see + -- the same full name for each directory. + Force_Checking_Of_Elaboration_Flags : Boolean := False; -- GNATBIND -- True if binding with forced checking of the elaboration flags @@ -657,6 +671,13 @@ package Opt is -- GNATMAKE, GPRMAKE, GPRBUILD -- Set to force recompilations even when the objects are up-to-date. + Front_End_Inlining : Boolean := False; + -- GNAT + -- Set True to activate inlining by front-end expansion (even on GCC + -- targets, where inlining is normally handled by the back end). Set by + -- the flag -gnatN (which is now considered obsolescent, since the GCC + -- back end can do a better job of inlining than the front end these days. + Full_Path_Name_For_Brief_Errors : Boolean := False; -- PROJECT MANAGER -- When True, in Brief_Output mode, each error message line @@ -684,6 +705,10 @@ package Opt is -- True when switch -gnateG is used. When True, create in a file -- <source>.prep, if the source is preprocessed. + Generate_SCIL : Boolean := False; + -- GNAT + -- Set True to activate SCIL code generation. + Generate_SCO : Boolean := False; -- GNAT -- True when switch -fdump-scos (or -gnateS) is used. When True, Source @@ -728,6 +753,12 @@ package Opt is -- default value appropriate to the system (in Osint.Initialize), and then -- reset if a command line switch is used to change the setting. + Ignore_Pragma_SPARK_Mode : Boolean := False; + -- GNAT + -- Set True to ignore the semantics and effects of pragma SPARK_Mode when + -- the pragma appears inside an instance whose enclosing context is subject + -- to SPARK_Mode "off". + Ignore_Rep_Clauses : Boolean := False; -- GNAT -- Set True to ignore all representation clauses. Useful when compiling @@ -798,35 +829,10 @@ package Opt is -- then elaboration flag checks are to be generated in the binder -- generated file. - Generate_SCIL : Boolean := False; - -- GNAT - -- Set True to activate SCIL code generation. - Invalid_Value_Used : Boolean := False; -- GNAT -- Set True if a valid Invalid_Value attribute is encountered - Follow_Links_For_Files : Boolean := False; - -- PROJECT MANAGER - -- Set to True (-eL) to process the project files in trusted mode. If - -- Follow_Links is False, it is assumed that the project doesn't contain - -- any file duplicated through symbolic links (although the latter are - -- still valid if they point to a file which is outside of the project), - -- and that no directory has a name which is a valid source name. - - Follow_Links_For_Dirs : Boolean := False; - -- PROJECT MANAGER - -- Set to True if directories can be links in this project, and therefore - -- additional system calls must be performed to ensure that we always see - -- the same full name for each directory. - - Front_End_Inlining : Boolean := False; - -- GNAT - -- Set True to activate inlining by front-end expansion (even on GCC - -- targets, where inlining is normally handled by the back end). Set by - -- the flag -gnatN (which is now considered obsolescent, since the GCC - -- back end can do a better job of inlining than the front end these days. - Inline_Processing_Required : Boolean := False; -- GNAT -- Set True if inline processing is required. Inline processing is required diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index ee6a1d978b4..73533a2107f 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3342,8 +3342,6 @@ package body Sem_Ch12 is Set_Parent_Spec (New_N, Save_Parent); Rewrite (N, New_N); - Check_SPARK_Mode_In_Generic (N); - -- The aspect specifications are not attached to the tree, and must -- be copied and attached to the generic copy explicitly. @@ -3532,6 +3530,9 @@ package body Sem_Ch12 is Needs_Body : Boolean; Inline_Now : Boolean := False; + Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; + -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit + Save_Style_Check : constant Boolean := Style_Check; -- Save style check mode for restore on exit @@ -3771,6 +3772,12 @@ package body Sem_Ch12 is goto Leave; else + -- If the instance or its context is subject to SPARK_Mode "off", + -- set the global flag which signals Analyze_Pragma to ignore all + -- SPARK_Mode pragmas within the instance. + + Set_Ignore_Pragma_SPARK_Mode (N); + Gen_Decl := Unit_Declaration_Node (Gen_Unit); -- Initialize renamings map, for error checking, and the list that @@ -3835,9 +3842,7 @@ package body Sem_Ch12 is Set_Visible_Declarations (Act_Spec, Renaming_List); end if; - Act_Decl := - Make_Package_Declaration (Loc, - Specification => Act_Spec); + Act_Decl := Make_Package_Declaration (Loc, Specification => Act_Spec); -- Propagate the aspect specifications from the package declaration -- template to the instantiated version of the package declaration. @@ -4277,6 +4282,7 @@ package body Sem_Ch12 is Set_Defining_Identifier (N, Act_Decl_Id); end if; + Ignore_Pragma_SPARK_Mode := Save_IPSM; Style_Check := Save_Style_Check; -- Check that if N is an instantiation of System.Dim_Float_IO or @@ -4311,6 +4317,7 @@ package body Sem_Ch12 is Restore_Env; end if; + Ignore_Pragma_SPARK_Mode := Save_IPSM; Style_Check := Save_Style_Check; end Analyze_Package_Instantiation; @@ -4865,6 +4872,9 @@ package body Sem_Ch12 is -- Local variables + Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; + -- Save flag Ignore_Pragma_SPARK_Mode for restore on exit + Vis_Prims_List : Elist_Id := No_Elist; -- List of primitives made temporarily visible in the instantiation -- to match the visibility of the formal type @@ -4929,6 +4939,12 @@ package body Sem_Ch12 is Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit); else + -- If the instance or its context is subject to SPARK_Mode "off", + -- set the global flag which signals Analyze_Pragma to ignore all + -- SPARK_Mode pragmas within the instance. + + Set_Ignore_Pragma_SPARK_Mode (N); + Set_Entity (Gen_Id, Gen_Unit); Set_Is_Instantiated (Gen_Unit); @@ -5139,6 +5155,8 @@ package body Sem_Ch12 is Env_Installed := False; Generic_Renamings.Set_Last (0); Generic_Renamings_HTable.Reset; + + Ignore_Pragma_SPARK_Mode := Save_IPSM; end if; <<Leave>> @@ -5155,6 +5173,8 @@ package body Sem_Ch12 is if Env_Installed then Restore_Env; end if; + + Ignore_Pragma_SPARK_Mode := Save_IPSM; end Analyze_Subprogram_Instantiation; ------------------------- diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index ca52755190b..dc226b37ec4 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2418,11 +2418,11 @@ package body Sem_Ch13 is Expression => Relocate_Node (Expr))), Pragma_Name => Name_SPARK_Mode); - -- When the aspect appears on a package body, insert the - -- generated pragma at the top of the body declarations to - -- emulate the behavior of a source pragma. + -- When the aspect appears on a package or a subprogram + -- body, insert the generated pragma at the top of the body + -- declarations to emulate the behavior of a source pragma. - if Nkind (N) = N_Package_Body then + if Nkind_In (N, N_Package_Body, N_Subprogram_Body) then Decorate (Aspect, Aitem); Decls := Declarations (N); @@ -2435,11 +2435,14 @@ package body Sem_Ch13 is Prepend_To (Decls, Aitem); goto Continue; - -- When the aspect is associated with package declaration, - -- insert the generated pragma at the top of the visible - -- declarations to emulate the behavior of a source pragma. + -- When the aspect is associated with a [generic] package + -- declaration, insert the generated pragma at the top of + -- the visible declarations to emulate the behavior of a + -- source pragma. - elsif Nkind (N) = N_Package_Declaration then + elsif Nkind_In (N, N_Generic_Package_Declaration, + N_Package_Declaration) + then Decorate (Aspect, Aitem); Decls := Visible_Declarations (Specification (N)); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 09978735d6e..a6014b14ec6 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1251,8 +1251,6 @@ package body Sem_Ch6 is end loop; end; - Check_SPARK_Mode_In_Generic (N); - Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Body_Id, True); @@ -3743,11 +3741,12 @@ package body Sem_Ch6 is Analyze_Declarations (Declarations (N)); - -- After declarations have been analyzed, the body has been set - -- its final value of SPARK_Mode. Check that SPARK_Mode for body - -- is consistent with SPARK_Mode for spec. + -- Verify that the SPARK_Mode of the body agrees with that of its spec - if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then + if not Inside_A_Generic + and then 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 and then @@ -3757,7 +3756,7 @@ package body Sem_Ch6 is Error_Msg_N ("incorrect application of SPARK_Mode#", N); Error_Msg_Sloc := Sloc (SPARK_Pragma (Spec_Id)); Error_Msg_NE - ("\value Off was set for SPARK_Mode on&#", N, Spec_Id); + ("\value Off was set for SPARK_Mode on & #", N, Spec_Id); end if; elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then @@ -3767,7 +3766,8 @@ package body Sem_Ch6 is Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id)); Error_Msg_N ("incorrect application of SPARK_Mode#", N); Error_Msg_Sloc := Sloc (Spec_Id); - Error_Msg_NE ("\no value was set for SPARK_Mode on&#", N, Spec_Id); + Error_Msg_NE + ("\no value was set for SPARK_Mode on & #", N, Spec_Id); end if; end if; diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index c018c1cc9b0..583621f96e7 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -437,11 +437,9 @@ package body Sem_Ch7 is Inspect_Deferred_Constant_Completion (Declarations (N)); end if; - -- After declarations have been analyzed, the body has been set to have - -- the final value of SPARK_Mode. Check that the SPARK_Mode for the body - -- is consistent with the SPARK_Mode for the spec. + -- Verify that the SPARK_Mode of the body agrees with that of its spec - if Present (SPARK_Pragma (Body_Id)) then + if not Inside_A_Generic and then 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 diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0b2accfc126..d6de6a7d1de 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -19116,13 +19116,6 @@ package body Sem_Prag is -- pragma SPARK_Mode [(On | Off)]; when Pragma_SPARK_Mode => Do_SPARK_Mode : declare - Body_Id : Entity_Id; - Context : Node_Id; - Mode : Name_Id; - Mode_Id : SPARK_Mode_Type; - Spec_Id : Entity_Id; - Stmt : Node_Id; - procedure Check_Pragma_Conformance (Context_Pragma : Node_Id; Entity_Pragma : Node_Id; @@ -19163,7 +19156,7 @@ package body Sem_Prag is -- New mode less restrictive than the established mode if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off - and then Mode_Id = On + and then Get_SPARK_Mode_From_Pragma (N) = On then Error_Msg_N ("cannot change SPARK_Mode from Off to On", Arg1); @@ -19176,7 +19169,7 @@ package body Sem_Prag is if Present (Entity) then if Present (Entity_Pragma) then if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off - and then Mode_Id = On + and then Get_SPARK_Mode_From_Pragma (N) = On then Error_Msg_N ("incorrect use of SPARK_Mode", Arg1); Error_Msg_Sloc := Sloc (Entity_Pragma); @@ -19224,9 +19217,36 @@ package body Sem_Prag is end if; end Check_Library_Level_Entity; + -- Local variables + + Body_Id : Entity_Id; + Context : Node_Id; + Inst_Id : Entity_Id; + Mode : Name_Id; + Mode_Id : SPARK_Mode_Type; + Spec_Id : Entity_Id; + Stmt : Node_Id; + -- Start of processing for Do_SPARK_Mode begin + -- When a SPARK_Mode pragma appears inside an instantiation whose + -- enclosing context has SPARK_Mode set to "off", the pragma has + -- no semantic effect. + + if Ignore_Pragma_SPARK_Mode then + Rewrite (N, Make_Null_Statement (Loc)); + Analyze (N); + return; + + -- Do not analyze the pragma when it appears inside a generic + -- because the semantic information of the related context is + -- scarce. + + elsif Inside_A_Generic then + return; + end if; + GNAT_Pragma; Check_No_Identifiers; Check_At_Most_N_Arguments (1); @@ -19243,15 +19263,15 @@ package body Sem_Prag is Mode_Id := Get_SPARK_Mode_Type (Mode); Context := Parent (N); - -- Packages and subprograms declared in a generic unit cannot be - -- subject to the pragma. + -- Handle a compilation unit with configuration pragmas - if Inside_A_Generic then - Error_Pragma ("incorrect placement of pragma% in a generic"); + if Nkind (Context) = N_Compilation_Unit_Aux then + Context := Parent (Context); + end if; -- The pragma appears in a configuration pragmas file - elsif No (Context) then + if No (Context) then Check_Valid_Configuration_Pragma; if Present (SPARK_Mode_Pragma) then @@ -19263,29 +19283,63 @@ package body Sem_Prag is SPARK_Mode_Pragma := N; SPARK_Mode := Mode_Id; - -- When the pragma is placed before the declaration of a unit, it - -- configures the whole unit. + -- The pragma applies to a compilation unit elsif Nkind (Context) = N_Compilation_Unit then - Check_Valid_Configuration_Pragma; - if Nkind (Unit (Context)) in N_Generic_Declaration - or else (Present (Library_Unit (Context)) - and then Nkind (Unit (Library_Unit (Context))) in - N_Generic_Declaration) - then - Error_Pragma ("incorrect placement of pragma% in a generic"); - end if; + -- The pragma acts as a configuration pragma - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; + -- pragma SPARK_Mode ...; + -- package Pack is ...; - -- The pragma applies to a [library unit] subprogram or package + if List_Containing (N) = Context_Items (Context) then + Check_Valid_Configuration_Pragma; + SPARK_Mode_Pragma := N; + SPARK_Mode := Mode_Id; - else - -- Verify the placement of the pragma with respect to package - -- or subprogram declarations and detect duplicates. + -- The pragma applies to a package instantiation that acts as a + -- compilation unit. + + -- package Inst is new Gen ...; + -- pragma SPARK_Mode ...; + + elsif Nkind (Unit (Context)) = N_Package_Instantiation then + Inst_Id := Defining_Entity (Instance_Spec (Unit (Context))); + Check_Library_Level_Entity (Inst_Id); + Check_Pragma_Conformance + (Context_Pragma => SPARK_Mode_Pragma, + Entity_Pragma => Empty, + Entity => Empty); + + Set_SPARK_Pragma (Inst_Id, N); + Set_SPARK_Pragma_Inherited (Inst_Id, False); + -- Otherwise the pragma applies to a subprogram instantiation + -- that acts as a compilation unit. + + else + Spec_Id := Defining_Entity (Unit (Context)); + Inst_Id := Related_Instance (Spec_Id); + Check_Library_Level_Entity (Spec_Id); + Check_Pragma_Conformance + (Context_Pragma => SPARK_Mode_Pragma, + Entity_Pragma => Empty, + Entity => Empty); + + Set_SPARK_Pragma (Spec_Id, N); + Set_SPARK_Pragma_Inherited (Spec_Id, False); + + if Present (Inst_Id) then + Set_SPARK_Pragma (Inst_Id, N); + Set_SPARK_Pragma_Inherited (Inst_Id, False); + end if; + end if; + + -- Otherwise the placement of the pragma within the tree dictates + -- its associated construct. Inspect the declarative list where + -- the pragma resides to find a potential construct. + + else Stmt := Prev (N); while Present (Stmt) loop @@ -19299,28 +19353,32 @@ package body Sem_Prag is raise Pragma_Exit; end if; - elsif Nkind (Stmt) in N_Generic_Declaration then - Error_Pragma - ("incorrect placement of pragma% on a generic"); + -- The pragma is associated with a package or subprogram + -- instantiation that does not act as a compilation unit. - -- The pragma applies to a package declaration + -- package Inst is new Gen ...; + -- pragma SPARK_Mode ...; - elsif Nkind (Stmt) = N_Package_Declaration then - Spec_Id := Defining_Entity (Stmt); - Check_Library_Level_Entity (Spec_Id); + elsif Nkind_In (Stmt, N_Function_Instantiation, + N_Package_Instantiation, + N_Procedure_Instantiation) + then + Inst_Id := Defining_Entity (Instance_Spec (Stmt)); + Check_Library_Level_Entity (Inst_Id); Check_Pragma_Conformance - (Context_Pragma => SPARK_Pragma (Spec_Id), + (Context_Pragma => SPARK_Mode_Pragma, Entity_Pragma => Empty, Entity => Empty); - Set_SPARK_Pragma (Spec_Id, N); - Set_SPARK_Pragma_Inherited (Spec_Id, False); - Set_SPARK_Aux_Pragma (Spec_Id, N); - Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True); + Set_SPARK_Pragma (Inst_Id, N); + Set_SPARK_Pragma_Inherited (Inst_Id, False); return; -- The pragma applies to a subprogram declaration + -- procedure Proc ...; + -- pragma SPARK_Mode ..; + elsif Nkind (Stmt) = N_Subprogram_Declaration then Spec_Id := Defining_Entity (Stmt); Check_Library_Level_Entity (Spec_Id); @@ -19338,8 +19396,9 @@ package body Sem_Prag is elsif not Comes_From_Source (Stmt) then null; - -- The pragma does not apply to a legal construct, issue an - -- error and stop the analysis. + -- Otherwise the pragma does not apply to a legal construct + -- or it does not appear at the top of a declarative or a + -- statement list. Issue an error and stop the analysis. else Pragma_Misplaced; @@ -19349,59 +19408,18 @@ package body Sem_Prag is Stmt := Prev (Stmt); end loop; - -- Handle all cases where the pragma is actually an aspect and - -- applies to a library-level package spec, body or subprogram. - - -- function F ... with SPARK_Mode => ...; - -- package P with SPARK_Mode => ...; - -- package body P with SPARK_Mode => ... is - - -- The following circuitry simply prepares the proper context - -- for the general pragma processing mechanism below. - - if Nkind (Context) = N_Compilation_Unit_Aux then - Context := Unit (Parent (Context)); - - if Nkind_In (Context, N_Package_Declaration, - N_Subprogram_Declaration) - then - Context := Specification (Context); - end if; - end if; - - -- The pragma is at the top level of a package spec - - -- package P is - -- pragma SPARK_Mode; - - -- or - - -- package P is - -- ... - -- private - -- pragma SPARK_Mode; + -- The pragma appears within package declarations if Nkind (Context) = N_Package_Specification then Spec_Id := Defining_Entity (Context); + Check_Library_Level_Entity (Spec_Id); - -- Pragma applies to private part - - if List_Containing (N) = Private_Declarations (Context) then - Check_Library_Level_Entity (Spec_Id); - Check_Pragma_Conformance - (Context_Pragma => Empty, - Entity_Pragma => SPARK_Pragma (Spec_Id), - Entity => Spec_Id); - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; - - Set_SPARK_Aux_Pragma (Spec_Id, N); - Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False); + -- The pragma is at the top of the visible declarations - -- Pragma applies to public part + -- package Pack is + -- pragma SPARK_Mode ...; - else - Check_Library_Level_Entity (Spec_Id); + if List_Containing (N) = Visible_Declarations (Context) then Check_Pragma_Conformance (Context_Pragma => SPARK_Pragma (Spec_Id), Entity_Pragma => Empty, @@ -19413,28 +19431,29 @@ package body Sem_Prag is Set_SPARK_Pragma_Inherited (Spec_Id, False); Set_SPARK_Aux_Pragma (Spec_Id, N); Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True); - end if; - -- The pragma appears as an aspect on a subprogram. + -- The pragma is at the top of the private declarations - -- function F ... with SPARK_Mode => ...; + -- package Pack is + -- private + -- pragma SPARK_Mode ...; - elsif Nkind_In (Context, N_Function_Specification, - N_Procedure_Specification) - then - Spec_Id := Defining_Entity (Context); - Check_Library_Level_Entity (Spec_Id); - Check_Pragma_Conformance - (Context_Pragma => SPARK_Pragma (Spec_Id), - Entity_Pragma => Empty, - Entity => Empty); - Set_SPARK_Pragma (Spec_Id, N); - Set_SPARK_Pragma_Inherited (Spec_Id, False); + else + Check_Pragma_Conformance + (Context_Pragma => Empty, + Entity_Pragma => SPARK_Pragma (Spec_Id), + Entity => Spec_Id); + SPARK_Mode_Pragma := N; + SPARK_Mode := Mode_Id; - -- Pragma is immediately within a package body + Set_SPARK_Aux_Pragma (Spec_Id, N); + Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False); + end if; - -- package body P is - -- pragma SPARK_Mode; + -- The pragma appears at the top of package body declarations + + -- package body Pack is + -- pragma SPARK_Mode ...; elsif Nkind (Context) = N_Package_Body then Spec_Id := Corresponding_Spec (Context); @@ -19452,9 +19471,33 @@ package body Sem_Prag is Set_SPARK_Aux_Pragma (Body_Id, N); Set_SPARK_Aux_Pragma_Inherited (Body_Id, True); - -- Pragma is immediately within a subprogram body + -- The pragma appears at the top of package body statements + + -- package body Pack is + -- begin + -- pragma SPARK_Mode; + + elsif Nkind (Context) = N_Handled_Sequence_Of_Statements + and then Nkind (Parent (Context)) = N_Package_Body + then + Context := Parent (Context); + Spec_Id := Corresponding_Spec (Context); + Body_Id := Defining_Entity (Context); + Check_Library_Level_Entity (Body_Id); + Check_Pragma_Conformance + (Context_Pragma => Empty, + Entity_Pragma => SPARK_Pragma (Body_Id), + Entity => Body_Id); + SPARK_Mode_Pragma := N; + SPARK_Mode := Mode_Id; + + Set_SPARK_Aux_Pragma (Body_Id, N); + Set_SPARK_Aux_Pragma_Inherited (Body_Id, False); + + -- The pragma appears at the top of subprogram body + -- declarations. - -- function F ... is + -- procedure Proc ... is -- pragma SPARK_Mode; elsif Nkind (Context) = N_Subprogram_Body then @@ -19471,11 +19514,16 @@ package body Sem_Prag is Check_Library_Level_Entity (Body_Id); + -- The body is a completion of a previous declaration + if Present (Spec_Id) then Check_Pragma_Conformance (Context_Pragma => SPARK_Pragma (Body_Id), Entity_Pragma => SPARK_Pragma (Spec_Id), Entity => Spec_Id); + + -- The body acts as spec + else Check_Pragma_Conformance (Context_Pragma => SPARK_Pragma (Body_Id), @@ -19489,29 +19537,6 @@ package body Sem_Prag is Set_SPARK_Pragma (Body_Id, N); Set_SPARK_Pragma_Inherited (Body_Id, False); - -- The pragma applies to the statements of a package body - - -- package body P is - -- begin - -- pragma SPARK_Mode; - - elsif Nkind (Context) = N_Handled_Sequence_Of_Statements - and then Nkind (Parent (Context)) = N_Package_Body - then - Context := Parent (Context); - Spec_Id := Corresponding_Spec (Context); - Body_Id := Defining_Entity (Context); - Check_Library_Level_Entity (Body_Id); - Check_Pragma_Conformance - (Context_Pragma => Empty, - Entity_Pragma => SPARK_Pragma (Body_Id), - Entity => Body_Id); - SPARK_Mode_Pragma := N; - SPARK_Mode := Mode_Id; - - Set_SPARK_Aux_Pragma (Body_Id, N); - Set_SPARK_Aux_Pragma_Inherited (Body_Id, False); - -- The pragma does not apply to a legal construct, issue error else diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 832c320b903..107ce11e0ce 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -3078,31 +3078,6 @@ package body Sem_Util is end if; end Check_Result_And_Post_State; - --------------------------------- - -- Check_SPARK_Mode_In_Generic -- - --------------------------------- - - procedure Check_SPARK_Mode_In_Generic (N : Node_Id) is - Aspect : Node_Id; - - begin - -- Try to find aspect SPARK_Mode and flag it as illegal - - if Has_Aspects (N) then - Aspect := First (Aspect_Specifications (N)); - while Present (Aspect) loop - if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then - Error_Msg_Name_1 := Name_SPARK_Mode; - Error_Msg_N - ("incorrect placement of aspect % on a generic", Aspect); - exit; - end if; - - Next (Aspect); - end loop; - end if; - end Check_SPARK_Mode_In_Generic; - ------------------------------ -- Check_Unprotected_Access -- ------------------------------ @@ -16481,6 +16456,128 @@ package body Sem_Util is Set_Entity (N, Val); end Set_Entity_With_Checks; + ---------------------------------- + -- Set_Ignore_Pragma_SPARK_Mode -- + ---------------------------------- + + procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id) is + procedure Set_SPARK_Mode (Expr : Node_Id); + -- Set flag Ignore_Pragma_SPARK_Mode based on the argument of aspect or + -- pragma SPARK_Mode denoted by Expr. + + -------------------- + -- Set_SPARK_Mode -- + -------------------- + + procedure Set_SPARK_Mode (Expr : Node_Id) is + begin + -- When pragma SPARK_Mode with argument "off" applies to an instance, + -- all SPARK_Mode pragmas within the instance are ignored. + + if Present (Expr) + and then Nkind (Expr) = N_Identifier + and then Chars (Expr) = Name_Off + then + Ignore_Pragma_SPARK_Mode := True; + end if; + end Set_SPARK_Mode; + + -- Local variables + + Aspects : constant List_Id := Aspect_Specifications (N); + Context : constant Node_Id := Parent (N); + Args : List_Id; + Aspect : Node_Id; + Decl : Node_Id; + + -- Start of processing for Set_Ignore_Pragma_SPARK_Mode + + begin + -- When the enclosing context of the instance has SPARK_Mode "off", all + -- SPARK_Mode pragmas within the instance are ignored. Note that there + -- is no point in checking whether the instantiation itself carries + -- aspect/pragma SPARK_Mode because it is either illegal ("on") or has + -- no effect ("off"). + + if SPARK_Mode = Off then + Ignore_Pragma_SPARK_Mode := True; + return; + end if; + + -- Inspect the aspects of the instantiation and locate SPARK_Mode. Note + -- that the aspect form of SPARK_Mode precedes a potentially duplicate + -- pragma. + + if Present (Aspects) then + Aspect := First (Aspects); + while Present (Aspect) loop + if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then + Set_SPARK_Mode (Expression (Aspect)); + return; + end if; + + Next (Aspect); + end loop; + end if; + + -- Peek ahead of the instance and locate pragma SPARK_Mode. Even though + -- the pragma is analyzed after the instance, its mode must be known now + -- as it governs the legality of SPARK_Mode pragmas within the instance. + + Decl := Empty; + + -- The instance is a compilation unit, the pragma appears on the + -- Pragmas_After list. + + if Present (Context) + and then Nkind (Context) = N_Compilation_Unit + and then Present (Aux_Decls_Node (Context)) + and then Present (Pragmas_After (Aux_Decls_Node (Context))) + then + Decl := First (Pragmas_After (Aux_Decls_Node (Context))); + + -- The instance is part of a declarative list, the pragma appears after + -- the instance. + + elsif Is_List_Member (N) then + Decl := Next (N); + end if; + + -- Inspect all declarations following the instance + + while Present (Decl) loop + if Nkind (Decl) = N_Pragma then + if Get_Pragma_Id (Decl) = Pragma_SPARK_Mode then + Args := Pragma_Argument_Associations (Decl); + + -- The pragma argument dictates the mode + + if Present (Args) then + Set_SPARK_Mode (Get_Pragma_Arg (First (Args))); + end if; + + -- Only the first SPARK_Mode following the instance is + -- considered, any extra (illegal) pragmas are ignored. + + exit; + end if; + + -- Skip internally generated code + + elsif not Comes_From_Source (Decl) then + null; + + -- Otherwise a source construct exhaust the range where the pragma + -- may appear. + + else + exit; + end if; + + Next (Decl); + end loop; + end Set_Ignore_Pragma_SPARK_Mode; + ------------------------ -- Set_Name_Entity_Id -- ------------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 025b0cfbbe8..9ac981e2f60 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -327,10 +327,6 @@ package Sem_Util is -- and post-state. Prag is a [refined] postcondition or a contract-cases -- pragma. Result_Seen is set when the pragma mentions attribute 'Result. - procedure Check_SPARK_Mode_In_Generic (N : Node_Id); - -- Given a generic package [body] or a generic subprogram [body], inspect - -- the aspect specifications (if any) and flag SPARK_Mode as illegal. - procedure Check_Unprotected_Access (Context : Node_Id; Expr : Node_Id); @@ -1841,6 +1837,11 @@ package Sem_Util is -- If restriction No_Implementation_Identifiers is set, then it checks -- that the entity is not implementation defined. + procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id); + -- Determine whether [the enclosing context of] package or subprogram N is + -- subject to pragma SPARK_Mode with mode "off". If this is the case, set + -- global flag Ignore_Pragma_SPARK_Mode to True. + procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id); pragma Inline (Set_Name_Entity_Id); -- Sets the Entity_Id value associated with the given name, which is the |