From a9e892d0750958d33f76f3900c45863c7c0d0fd1 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 8 Jul 2013 09:41:19 +0200 Subject: [PATCH] [multiple changes] 2013-07-08 Hristian Kirtchev * sem_prag.adb (Analyze_Pragma): Remove variable Unit_Prag. Remove the check on duplicate mode for the configuration form of the pragma. (Redefinition_Error): Removed. 2013-07-08 Robert Dewar * lib.ads, gnat_rm.texi, einfo.ads, sem_ch13.adb: Minor reformatting and editing. From-SVN: r200753 --- gcc/ada/ChangeLog | 12 +++++++ gcc/ada/einfo.ads | 3 +- gcc/ada/gnat_rm.texi | 36 +++++++++++++-------- gcc/ada/lib.ads | 2 +- gcc/ada/sem_ch13.adb | 4 ++- gcc/ada/sem_prag.adb | 77 +++++--------------------------------------- 6 files changed, 48 insertions(+), 86 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index a6a808faa56..faa1556df30 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,15 @@ +2013-07-08 Hristian Kirtchev + + * sem_prag.adb (Analyze_Pragma): Remove + variable Unit_Prag. Remove the check on duplicate mode for the + configuration form of the pragma. + (Redefinition_Error): Removed. + +2013-07-08 Robert Dewar + + * lib.ads, gnat_rm.texi, einfo.ads, sem_ch13.adb: Minor reformatting + and editing. + 2013-07-08 Ed Schonberg * sem_prag.adb (Analyze_PPC_In_Decl_Part): In ASIS mode, diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 0df28805618..a99812117b8 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -1,7 +1,6 @@ ------------------------------------------------------------------------------ -- -- -- GNAT COMPILER COMPONENTS -- --- -- -- E I N F O -- -- -- -- S p e c -- @@ -3760,7 +3759,7 @@ package Einfo is -- SPARK_Mode_Pragmas (Node32) -- Present in the entities of subprogram specs and bodies as well as in -- package specs and bodies. Points to a list of SPARK_Mode pragmas that --- apply to the related construct. +-- apply to the related construct. Add note of what this is used for ??? -- Spec_Entity (Node19) -- Defined in package body entities. Points to corresponding package diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 4b0c37c34d0..d59ac49cb49 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -6028,8 +6028,8 @@ SPARK_Mode is used without an argument. @item @code{Off}: The units are considered to be in Ada by default and therefore not -part of SPARK 2014 unless overridden locally. These units may be called by SPARK -2014 units. +part of SPARK 2014 unless overridden locally. These units may be called by +SPARK 2014 units. @item @code{Auto}: The formal verification tools will automatically detect whether @@ -6045,28 +6045,38 @@ Pragma SPARK_Mode can be used as a local pragma with the following semantics: Auto cannot be used as a mode argument. @item -When the pragma appears immediately within the visible declarations of a -package, it marks the whole package (spec and body) in or out of SPARK 2014. +When the pragma at the start of the visible declarations (preceded only +by other pragmas) of a package declaration, it marks the whole package +(declaration and body) in or out of SPARK 2014. @item -When the pragma appears immediately within the private declarations of a -package, it marks the private part in or out of SPARK 2014. +When the pragma appears at the start of the private declarations of a +package (only other pragmas can appear between the @code{private} keyword +and the @code{SPARK_Mode} pragma, it marks the private part in or +out of SPARK 2014 (overriding the mode for the public part). @item -When the pragma appears immediately within the declarations of a package body, -it marks the whole body in or out of SPARK 2014. +When the pragma appears immediately at the start of the declarations of a +package body (preceded only by other pragmas), +it marks the whole body in or out of SPARK 2014 (overriding the default +mode copied from the declaration). @item -When the pragma appears immediately within the elaboration statements of a -package body, it marks the statements in or out of SPARK 2014. +When the pragma appears at the start of the elaboration statements of +a package body (only other pragmas can appear between the @code{begin} +keyword and the @code{SPARK_Mode} pragma, +it marks the elaboration statements in or out of SPARK 2014, overriding +the default mode of the package body). @item -When the pragma appears after a subprogram declaration, it marks the whole +When the pragma appears after a subprogram declaration (with only other +pragmas intervening), it marks the whole subprogram (spec and body) in or out of SPARK 2014. @item -When the pragma appears immediately within the declarations of a subprogram -body, it marks the whole body in or out of SPARK 2014. +When the pragma appears at the start of the declarations of a subprogram +body (preceded only by other pragmas), it marks the whole body in or out +of SPARK 2014, overriding the default mode set by the declaration. @item Any other use of the pragma is illegal. diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads index eb10a8bd210..ac1945e6ecc 100644 --- a/gcc/ada/lib.ads +++ b/gcc/ada/lib.ads @@ -373,7 +373,7 @@ package Lib is -- SPARK_Mode_Pragma -- Pointer to the configuration pragma SPARK_Mode that applies to the - -- whole unit. + -- whole unit. Add note of what this is used for ??? -- Unit_File_Name -- The name of the source file containing the unit. Set when the entry diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 2cb3d29dc66..abf415f7bb1 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1809,7 +1809,9 @@ package body Sem_Ch13 is end loop; end if; - -- Build the precondition/postcondition pragma. + -- Build the precondition/postcondition pragma + + -- Add note about why we do NOT need Copy_Tree here ??? Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 16bccace7ee..dff2a21923f 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -16354,16 +16354,6 @@ package body Sem_Prag is function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id; -- Convert a value of type SPARK_Mode_Id into a corresponding name - procedure Redefinition_Error (Mode : SPARK_Mode_Id); - -- Emit an error on an attempt to redefine existing mode Mode. The - -- message is associated with the first argument of the current - -- pragma. - - procedure Redefinition_Error (Prag : Node_Id); - -- Emit an error on an attempt to redefine the mode of Prag. The - -- message is associated with the first argument of the current - -- pragma. - ------------------ -- Chain_Pragma -- ------------------ @@ -16474,41 +16464,14 @@ package body Sem_Prag is end if; end Get_SPARK_Mode_Name; - ------------------------ - -- Redefinition_Error -- - ------------------------ - - procedure Redefinition_Error (Mode : SPARK_Mode_Id) is - begin - Error_Msg_Name_1 := Get_SPARK_Mode_Name (Mode); - Error_Msg_N - ("cannot redefine 'S'P'A'R'K mode, already set to %", Arg1); - end Redefinition_Error; - - ------------------------ - -- Redefinition_Error -- - ------------------------ - - procedure Redefinition_Error (Prag : Node_Id) is - Mode : constant Name_Id := - Chars (Get_Pragma_Arg (First - (Pragma_Argument_Associations (Prag)))); - begin - Error_Msg_Name_1 := Mode; - Error_Msg_Sloc := Sloc (Prag); - Error_Msg_N - ("cannot redefine 'S'P'A'R'K mode, already set to % #", Arg1); - end Redefinition_Error; - -- Local variables - Body_Id : Entity_Id; - Context : Node_Id; - Mode : Name_Id; - Mode_Id : SPARK_Mode_Id; - Spec_Id : Entity_Id; - Stmt : Node_Id; - Unit_Prag : Node_Id; + Body_Id : Entity_Id; + Context : Node_Id; + Mode : Name_Id; + Mode_Id : SPARK_Mode_Id; + Spec_Id : Entity_Id; + Stmt : Node_Id; -- Start of processing for SPARK_Mode @@ -16536,38 +16499,14 @@ package body Sem_Prag is if No (Context) then Check_Valid_Configuration_Pragma; - - -- Set the global mode - - if Global_SPARK_Mode = None then - Global_SPARK_Mode := Mode_Id; - - -- Catch an attempt to redefine an existing global mode by - -- using multiple configuration files. - - elsif Global_SPARK_Mode /= Mode_Id then - Redefinition_Error (Global_SPARK_Mode); - end if; + Global_SPARK_Mode := Mode_Id; -- When the pragma is placed before the declaration of a unit, it -- configures the whole unit. elsif Nkind (Context) = N_Compilation_Unit then Check_Valid_Configuration_Pragma; - - Unit_Prag := SPARK_Mode_Pragma (Current_Sem_Unit); - - -- Set the unit mode - - if No (Unit_Prag) then - Set_SPARK_Mode_Pragma (Current_Sem_Unit, N); - - -- Catch an attempt to redefine the unit mode by using multiple - -- pragmas declared in the same region. - - else - Redefinition_Error (Unit_Prag); - end if; + Set_SPARK_Mode_Pragma (Current_Sem_Unit, N); -- The pragma applies to a [library unit] subprogram or package -- 2.30.2