+2013-07-08 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * 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 <dewar@adacore.com>
+
+ * lib.ads, gnat_rm.texi, einfo.ads, sem_ch13.adb: Minor reformatting
+ and editing.
+
2013-07-08 Ed Schonberg <schonberg@adacore.com>
* sem_prag.adb (Analyze_PPC_In_Decl_Part): In ASIS mode,
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
--- --
-- E I N F O --
-- --
-- S p e c --
-- 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
@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
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.
-- 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
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 (
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 --
------------------
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
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
projects / thirdparty / gcc.git / commitdiff
