Patchwork [Ada] Aspect / pragma SPARK_Mode

login
register
mail settings
Submitter Arnaud Charlet
Date July 5, 2013, 10:57 a.m.
Message ID <20130705105758.GA21830@adacore.com>
Download mbox | patch
Permalink /patch/257102/
State New
Headers show

Comments

Arnaud Charlet - July 5, 2013, 10:57 a.m.
This patch provides the initial implementation of aspect/pragma SPARK_Mode. It
is intended for formal verification and has no effect on generated code.

The semantics of the aspect/pragma are as follows:

   pragma SPARK_Mode [ (On | Off | Auto) ] ;

When used as a configuration pragma on a single file or a set of files, this
sets the mode of the units involved, in particular:

   On : all entities in the units should follow the SPARK 2014 language, and an
error will be generated if not, unless locally overriden via a local SPARK_Mode
pragma or aspect. On is the default if pragma SPARK_Mode is used without any
parameter.

    Off : the units are considered to be in Ada by default and therefore not
part of SPARK 2014 unless overriden locally. These units may be called by SPARK
units.

    Auto : this one is more on the tools side, so potentially not part of the
SPARK 2014 Reference Manual (TBD). The tools will automatically detect for each
entity whether the entity is in SPARK or in Ada and may also provide ways to
know which entities are in or out SPARK.

When used as a local pragma, you can use it in a restricted set of places, with
only On or Off valid values (no Auto), with the following semantic:

    * After package X is, to mark a whole package (spec+body) either in or out
SPARK.

    * After package body X is, to mark a whole package body in/out SPARK.

    * After a subprogram spec, to mark the subprogram (spec+body) in/out SPARK.

    * After a procedure|function X[...] is, to mark a subprogram body in/out
SPARK.

    * After the private keyword of a package spec to mark the whole private
part of a package spec in/out SPARK.

    * After the begin keyword of a package body to mark the elaboration
procedure of a package in/out SPARK.

When used anywhere else, an error should be generated.

A new aspect: SPARK_Mode [=> On|Off]; which can be used similarly to the
SPARK_Mode pragma to mark package spec/body and procedure spec/body as in/out
SPARK.

------------
-- Source --
------------

--  semantics.ads

package Semantics is
   pragma SPARK_Mode (Auto); --  Error, cannot use "Auto" in non-configuration
                             --  variant

   procedure Error_1
   with SPARK_Mode => Junk_Argument; --  Error, unrecognized argument

   procedure Error_2;
   pragma SPARK_Mode (Junk_Formal => Junk_Argument); --  Error, cannot have
                                                     --  associations

   procedure Error_3;
   pragma SPARK_Mode (One, Two, Three); --  Error, can have at most one arg

   package Error_4 is
      procedure Dummy;
   end Error_4;

   procedure Error_5;
   procedure Error_6;

   procedure Error_7;
   pragma SPARK_Mode (On);
   pragma SPARK_Mode (On); --  Error, duplicate pragma

   procedure Error_8 with SPARK_Mode => On;
   pragma SPARK_Mode (On); --  Error, duplicate aspect/pragma combination

   procedure Error_9;

   Obj : Integer;
   pragma SPARK_Mode (On); --  Error, not immediately within package

   package OK_1 is
      pragma SPARK_Mode (On);
   end OK_1;

   package OK_2 with SPARK_Mode => On is
   end OK_2;

   package OK_3 is
   private
      pragma SPARK_Mode (On);
   end OK_3;

   package OK_4 is
      procedure Dummy;
   end OK_4;

   procedure OK_5;
   pragma SPARK_Mode (On);

   procedure OK_6 with SPARK_Mode => On;

   procedure OK_7;
end Semantics;

--  semantics.adb

package body Semantics is
   procedure Error_1 is begin null; end Error_1;
   procedure Error_2 is begin null; end Error_2;
   procedure Error_3 is begin null; end Error_3;

   package body Error_4 is
      procedure Dummy is begin null; end Dummy;
      pragma SPARK_Mode (On); --  Error, not immediately within package
   end Error_4;

   procedure Error_5 is
      Obj : Integer;
      pragma SPARK_Mode (On); --  Error, not immediately within subprogram
   begin
      null;
   end Error_5;

   procedure Error_6 is
      Obj : Integer;
   begin
      Obj := 1234;
      pragma SPARK_Mode (On); --  Error, not immediately within subprogram
   end Error_6;

   procedure Error_7 is begin null; end Error_7;
   procedure Error_8 is begin null; end Error_8;

   procedure Error_9 is
      pragma SPARK_Mode (On);
      pragma SPARK_Mode (On); --  Error, duplicate pragma
   begin
      null;
   end Error_9;

   package body OK_4 is
      pragma SPARK_Mode (On);
      procedure Dummy is begin null; end Dummy;
   end OK_4;

   procedure OK_5 is begin null; end OK_5;
   procedure OK_6 is begin null; end OK_6;

   procedure OK_7 is
      pragma SPARK_Mode (On);
   begin
      null;
   end OK_7;
end Semantics;

--  monotonic_pairs.adb

procedure Monotonic_Pairs is
   package OK_1 is
      pragma SPARK_Mode (On);
   private
      pragma SPARK_Mode (Off);
   end OK_1;

   package OK_2 is
      procedure Dummy;
   end OK_2;

   package body OK_2 is
      pragma SPARK_Mode (On);
      procedure Dummy is begin null; end Dummy;
   begin
      pragma SPARK_Mode (Off);
   end OK_2;

   package OK_3 is
      pragma SPARK_Mode (On);
      procedure Dummy;
   end OK_3;

   package body OK_3 is
      pragma SPARK_Mode (Off);
      procedure Dummy is begin null; end Dummy;
   end OK_3;

   package OK_4 is
      procedure Dummy;
   private
      pragma SPARK_Mode (Off);
   end OK_4;

   package body OK_4 is
      pragma SPARK_Mode (On);  --  OK, Off applies to the private part only
      procedure Dummy is begin null; end Dummy;
   end OK_4;

   package OK_5 is
      procedure Dummy;
   private
      pragma SPARK_Mode (Off);
   end OK_5;

   package body OK_5 is
      procedure Dummy is begin null; end Dummy;
   begin
      pragma SPARK_Mode (On);  --  OK, Off applies to the private part only
   end OK_5;

   package OK_Subprograms is
      procedure OK_6;
      pragma SPARK_Mode (On);
   end OK_Subprograms;

   package body OK_Subprograms is
      procedure OK_6 is
         pragma SPARK_Mode (Off);
      begin null; end OK_6;
   end OK_Subprograms;

   package Error_1 is
      pragma SPARK_Mode (Off);
   private
      pragma SPARK_Mode (On);  --  Error
   end Error_1;

   package Error_2 is
      procedure Dummy;
   end Error_2;

   package body Error_2 is
      pragma SPARK_Mode (Off);
      procedure Dummy is begin null; end Dummy;
   begin
      pragma SPARK_Mode (On);  --  Error
   end Error_2;

   package Error_3 is
      pragma SPARK_Mode (Off);
      procedure Dummy;
   end Error_3;

   package body Error_3 is
      pragma SPARK_Mode (On);  --  Error
      procedure Dummy is begin null; end Dummy;
   end Error_3;

   package Error_Subprograms is
      procedure Error_4;
      pragma SPARK_Mode (Off);
   end Error_Subprograms;

   package body Error_Subprograms is
      procedure Error_4 is
         pragma SPARK_Mode (On);  --  Error
      begin null; end Error_4;
   end Error_Subprograms;
begin
   null;
end Monotonic_Pairs;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c semantics.adb
$ gcc -c monotonic_pairs.adb
semantics.adb:8:07: incorrect placement of pragma "Spark_Mode"
semantics.adb:13:07: incorrect placement of pragma "Spark_Mode"
semantics.adb:22:07: incorrect placement of pragma "Spark_Mode"
semantics.adb:30:07: pragma "Spark_Mode" duplicates pragma declared at line 29
semantics.ads:2:23: mode "Auto" can only apply to the configuration variant of
  pragma "Spark_Mode"
semantics.ads:6:23: invalid argument for aspect "Spark_Mode"
semantics.ads:9:23: pragma "Spark_Mode" does not permit identifier
  "Junk_Formal" here
semantics.ads:13:28: too many arguments for pragma "Spark_Mode"
semantics.ads:24:04: pragma "Spark_Mode" duplicates pragma declared at line 23
semantics.ads:27:04: pragma "Spark_Mode" duplicates pragma declared at line 26
semantics.ads:32:04: incorrect placement of pragma "Spark_Mode"
monotonic_pairs.adb:66:07: cannot define SPARK mode "On"
monotonic_pairs.adb:66:07: mode is less restrictive than mode "Off" defined at
  line 64
monotonic_pairs.adb:77:07: cannot define SPARK mode "On"
monotonic_pairs.adb:77:07: mode is less restrictive than mode "Off" defined at
  line 74
monotonic_pairs.adb:86:07: cannot define SPARK mode "On"
monotonic_pairs.adb:86:07: mode is less restrictive than mode "Off" defined at
  line 81
monotonic_pairs.adb:97:10: cannot define SPARK mode "On"
monotonic_pairs.adb:97:10: mode is less restrictive than mode "Off" defined at
  line 92

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-07-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry for SPARK_Mode in table Canonical_Aspect.
	* aspects.ads: Add an entry for SPARK_Mode in tables Aspect_Id,
	Aspect_Argument, Aspect_Names.
	* atree.adb (Node32): New routine.
	(Set_Node32): New routine.
	* atree.ads (Node32): New routine.
	(Set_Node32): New routine.
	* einfo.adb: Node32 is now used as SPARK_Mode_Pragmas.
	(Set_SPARK_Mode_Pragmas): New routine.
	(SPARK_Mode_Pragmas): New routine.
	(Write_Field32_Name): Add and entry for SPARK_Modes.
	* einfo.ads: Add attribute SPARK_Mode_Pragmas along with usage
	in various entities.
	(Set_SPARK_Mode_Pragmas): New routine and
	pragma Inline.
	(SPARK_Mode_Pragmas): New routine and pragma Inline.
	* gnat_rm.texi: Add sections explaining the syntax and semantics
	of aspect/pragma SPARK_Mode.
	* gnat_ugn.texi: Add pragma SPARK_Mode to the list of
	configuration pragmas.
	* lib.adb (Set_SPARK_Mode_Pragma): New routine.
	(SPARK_Mode_Pragma): New routine.
	* lib.ads: Alphabetize the comments on fields of record
	Unit_Record. Add new field SPARK_Mode_Pragma along with
	comment on its usage. Update the layout of record Unit_Record.
	(Set_SPARK_Mode_Pragma): New routine and pragma Inline.
	(SPARK_Mode_Pragma): New routine and pragma Inline.
	* lib-load.adb (Create_Dummy_Package_Unit): Initialize
	field SPARK_Mode_Pragma.
	(Load_Main_Source): Initialize field SPARK_Mode_Pragma.
	(Load_Unit): Initialize field SPARK_Mode_Pragma.
	* lib-writ.adb (Add_Preprocessing_Dependency): Initialize field
	SPARK_Mode_Pragma.
	(Ensure_System_Dependency): Initialize field SPARK_Mode_Pragma.
	* opt.ads: Alphabetize verification flags. Store the
	compilation-wide SPARK mode in variable Global_SPARK_Mode.
	* par-prag.adb: Pragma SPARK_Mode does not need special processing
	by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
	SPARK_Mode into a pragma.
	(Check_Aspect_At_Freeze_Point): Aspect SPARK_Mode does not need
	delayed processing.
	* sem_prag.adb: Add an entry for SPARK_Mode in table Sig_Flags.
	(Analyze_Pragma): Add processing for pragma SPARK_Mode.
	(Get_SPARK_Mode_Id): New routine.
	(Is_Elaboration_SPARK_Mode): New routine.
	(Is_Private_SPARK_Mode): New routine.
	* sem_prag.ads (Get_SPARK_Mode_Id): New routine.
	(Is_Elaboration_SPARK_Mode): New routine.
	(Is_Private_SPARK_Mode): New routine.
	* sinfo.ads: Update the comment on the usage of field Next_Pragma.
	* snames.ads-tmpl: Add new predefined name for SPARK_Mode and
	Auto. Add new pragma Id for SPARK_Mode.
	* types.ads: Add new type SPARK_Mode_Id.

Patch

Index: lib.adb
===================================================================
--- lib.adb	(revision 200688)
+++ lib.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -166,6 +166,11 @@ 
       return Units.Table (U).Source_Index;
    end Source_Index;
 
+   function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id is
+   begin
+      return Units.Table (U).SPARK_Mode_Pragma;
+   end SPARK_Mode_Pragma;
+
    function Unit_File_Name (U : Unit_Number_Type) return File_Name_Type is
    begin
       return Units.Table (U).Unit_File_Name;
@@ -254,6 +259,11 @@ 
       Units.Table (U).OA_Setting := C;
    end Set_OA_Setting;
 
+   procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id) is
+   begin
+      Units.Table (U).SPARK_Mode_Pragma := N;
+   end Set_SPARK_Mode_Pragma;
+
    procedure Set_Unit_Name (U : Unit_Number_Type; N : Unit_Name_Type) is
    begin
       Units.Table (U).Unit_Name := N;
Index: lib.ads
===================================================================
--- lib.ads	(revision 200688)
+++ lib.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -265,38 +265,6 @@ 
    --  The first entry in the table, subscript Main_Unit, is for the main file.
    --  Each entry in this units table contains the following data.
 
-   --    Unit_File_Name
-   --      The name of the source file containing the unit. Set when the entry
-   --      is created by a call to Lib.Load, and then cannot be changed.
-
-   --    Source_Index
-   --      The index in the source file table of the corresponding source file.
-   --      Set when the entry is created by a call to Lib.Load and then cannot
-   --      be changed.
-
-   --    Munit_Index
-   --      The index of the unit within the file for multiple unit per file
-   --      mode. Set to zero in normal single unit per file mode.
-
-   --    Error_Location
-   --      This is copied from the Sloc field of the Enode argument passed
-   --      to Load_Unit. It refers to the enclosing construct which caused
-   --      this unit to be loaded, e.g. most typically the with clause that
-   --      referenced the unit, and is used for error handling in Par.Load.
-
-   --    Expected_Unit
-   --      This is the expected unit name for a file other than the main unit,
-   --      since these are cases where we load the unit using Lib.Load and we
-   --      know the unit that is expected. It must be the same as Unit_Name
-   --      if it is set (see test in Par.Load). Expected_Unit is set to
-   --      No_Name for the main unit.
-
-   --    Unit_Name
-   --      The name of the unit. Initialized to No_Name by Lib.Load, and then
-   --      set by the parser when the unit is parsed to the unit name actually
-   --      found in the file (which should, in the absence of errors) be the
-   --      same name as Expected_Unit.
-
    --    Cunit
    --      Pointer to the N_Compilation_Unit node. Initially set to Empty by
    --      Lib.Load, and then reset to the required node by the parser when
@@ -320,6 +288,19 @@ 
    --      checks specified (as the result of using the -gnatE compilation
    --      option or a pragma Elaboration_Checks (Dynamic).
 
+   --    Error_Location
+   --      This is copied from the Sloc field of the Enode argument passed
+   --      to Load_Unit. It refers to the enclosing construct which caused
+   --      this unit to be loaded, e.g. most typically the with clause that
+   --      referenced the unit, and is used for error handling in Par.Load.
+
+   --    Expected_Unit
+   --      This is the expected unit name for a file other than the main unit,
+   --      since these are cases where we load the unit using Lib.Load and we
+   --      know the unit that is expected. It must be the same as Unit_Name
+   --      if it is set (see test in Par.Load). Expected_Unit is set to
+   --      No_Name for the main unit.
+
    --    Fatal_Error
    --      A flag that is initialized to False, and gets set to True if a fatal
    --      error occurs during the processing of a unit. A fatal error is one
@@ -335,6 +316,10 @@ 
    --      code is to be generated. This includes the unit explicitly compiled,
    --      together with its specification, and any subunits.
 
+   --    Has_Allocator
+   --      This flag is set if a subprogram unit has an allocator after the
+   --      BEGIN (it is used to set the AB flag in the M ALI line).
+
    --    Has_RACW
    --      A Boolean flag, initially set to False when a unit entry is created,
    --      and set to True if the unit defines a remote access to class wide
@@ -366,9 +351,9 @@ 
    --      that the default affinity is to be used (and is also used for
    --      entries that do not correspond to possible main programs).
 
-   --    Has_Allocator
-   --      This flag is set if a subprogram unit has an allocator after the
-   --      BEGIN (it is used to set the AB flag in the M ALI line).
+   --    Munit_Index
+   --      The index of the unit within the file for multiple unit per file
+   --      mode. Set to zero in normal single unit per file mode.
 
    --    OA_Setting
    --      This is a character field containing L if Optimize_Alignment mode
@@ -381,6 +366,25 @@ 
    --      routine which increments the current value and returns it. This
    --      serial number is separate for each unit.
 
+   --    Source_Index
+   --      The index in the source file table of the corresponding source file.
+   --      Set when the entry is created by a call to Lib.Load and then cannot
+   --      be changed.
+
+   --    SPARK_Mode_Pragma
+   --      Pointer to the configuration pragma SPARK_Mode that applies to the
+   --      whole unit.
+
+   --    Unit_File_Name
+   --      The name of the source file containing the unit. Set when the entry
+   --      is created by a call to Lib.Load, and then cannot be changed.
+
+   --    Unit_Name
+   --      The name of the unit. Initialized to No_Name by Lib.Load, and then
+   --      set by the parser when the unit is parsed to the unit name actually
+   --      found in the file (which should, in the absence of errors) be the
+   --      same name as Expected_Unit.
+
    --    Version
    --      This field holds the version of the unit, which is computed as
    --      the exclusive or of the checksums of this unit, and all its
@@ -404,43 +408,45 @@ 
    Default_Main_CPU : constant Int := -1;
    --  Value used in Main_CPU field to indicate default main affinity
 
-   function Cunit            (U : Unit_Number_Type) return Node_Id;
-   function Cunit_Entity     (U : Unit_Number_Type) return Entity_Id;
-   function Dependency_Num   (U : Unit_Number_Type) return Nat;
-   function Dynamic_Elab     (U : Unit_Number_Type) return Boolean;
-   function Error_Location   (U : Unit_Number_Type) return Source_Ptr;
-   function Expected_Unit    (U : Unit_Number_Type) return Unit_Name_Type;
-   function Fatal_Error      (U : Unit_Number_Type) return Boolean;
-   function Generate_Code    (U : Unit_Number_Type) return Boolean;
-   function Ident_String     (U : Unit_Number_Type) return Node_Id;
-   function Has_Allocator    (U : Unit_Number_Type) return Boolean;
-   function Has_RACW         (U : Unit_Number_Type) return Boolean;
-   function Is_Compiler_Unit (U : Unit_Number_Type) return Boolean;
-   function Loading          (U : Unit_Number_Type) return Boolean;
-   function Main_CPU         (U : Unit_Number_Type) return Int;
-   function Main_Priority    (U : Unit_Number_Type) return Int;
-   function Munit_Index      (U : Unit_Number_Type) return Nat;
-   function OA_Setting       (U : Unit_Number_Type) return Character;
-   function Source_Index     (U : Unit_Number_Type) return Source_File_Index;
-   function Unit_File_Name   (U : Unit_Number_Type) return File_Name_Type;
-   function Unit_Name        (U : Unit_Number_Type) return Unit_Name_Type;
+   function Cunit             (U : Unit_Number_Type) return Node_Id;
+   function Cunit_Entity      (U : Unit_Number_Type) return Entity_Id;
+   function Dependency_Num    (U : Unit_Number_Type) return Nat;
+   function Dynamic_Elab      (U : Unit_Number_Type) return Boolean;
+   function Error_Location    (U : Unit_Number_Type) return Source_Ptr;
+   function Expected_Unit     (U : Unit_Number_Type) return Unit_Name_Type;
+   function Fatal_Error       (U : Unit_Number_Type) return Boolean;
+   function Generate_Code     (U : Unit_Number_Type) return Boolean;
+   function Ident_String      (U : Unit_Number_Type) return Node_Id;
+   function Has_Allocator     (U : Unit_Number_Type) return Boolean;
+   function Has_RACW          (U : Unit_Number_Type) return Boolean;
+   function Is_Compiler_Unit  (U : Unit_Number_Type) return Boolean;
+   function Loading           (U : Unit_Number_Type) return Boolean;
+   function Main_CPU          (U : Unit_Number_Type) return Int;
+   function Main_Priority     (U : Unit_Number_Type) return Int;
+   function Munit_Index       (U : Unit_Number_Type) return Nat;
+   function OA_Setting        (U : Unit_Number_Type) return Character;
+   function Source_Index      (U : Unit_Number_Type) return Source_File_Index;
+   function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id;
+   function Unit_File_Name    (U : Unit_Number_Type) return File_Name_Type;
+   function Unit_Name         (U : Unit_Number_Type) return Unit_Name_Type;
    --  Get value of named field from given units table entry
 
-   procedure Set_Cunit            (U : Unit_Number_Type; N : Node_Id);
-   procedure Set_Cunit_Entity     (U : Unit_Number_Type; E : Entity_Id);
-   procedure Set_Dynamic_Elab     (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Error_Location   (U : Unit_Number_Type; W : Source_Ptr);
-   procedure Set_Fatal_Error      (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Generate_Code    (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Has_RACW         (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Has_Allocator    (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Is_Compiler_Unit (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Ident_String     (U : Unit_Number_Type; N : Node_Id);
-   procedure Set_Loading          (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Main_CPU         (U : Unit_Number_Type; P : Int);
-   procedure Set_Main_Priority    (U : Unit_Number_Type; P : Int);
-   procedure Set_OA_Setting       (U : Unit_Number_Type; C : Character);
-   procedure Set_Unit_Name        (U : Unit_Number_Type; N : Unit_Name_Type);
+   procedure Set_Cunit             (U : Unit_Number_Type; N : Node_Id);
+   procedure Set_Cunit_Entity      (U : Unit_Number_Type; E : Entity_Id);
+   procedure Set_Dynamic_Elab      (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Error_Location    (U : Unit_Number_Type; W : Source_Ptr);
+   procedure Set_Fatal_Error       (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Generate_Code     (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Has_RACW          (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Has_Allocator     (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Is_Compiler_Unit  (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Ident_String      (U : Unit_Number_Type; N : Node_Id);
+   procedure Set_Loading           (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Main_CPU          (U : Unit_Number_Type; P : Int);
+   procedure Set_Main_Priority     (U : Unit_Number_Type; P : Int);
+   procedure Set_OA_Setting        (U : Unit_Number_Type; C : Character);
+   procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id);
+   procedure Set_Unit_Name         (U : Unit_Number_Type; N : Unit_Name_Type);
    --  Set value of named field for given units table entry. Note that we
    --  do not have an entry for each possible field, since some of the fields
    --  can only be set by specialized interfaces (defined below).
@@ -707,34 +713,37 @@ 
    pragma Inline (Set_Main_CPU);
    pragma Inline (Set_Main_Priority);
    pragma Inline (Set_OA_Setting);
+   pragma Inline (Set_SPARK_Mode_Pragma);
    pragma Inline (Set_Unit_Name);
    pragma Inline (Source_Index);
+   pragma Inline (SPARK_Mode_Pragma);
    pragma Inline (Unit_File_Name);
    pragma Inline (Unit_Name);
 
    type Unit_Record is record
-      Unit_File_Name   : File_Name_Type;
-      Unit_Name        : Unit_Name_Type;
-      Munit_Index      : Nat;
-      Expected_Unit    : Unit_Name_Type;
-      Source_Index     : Source_File_Index;
-      Cunit            : Node_Id;
-      Cunit_Entity     : Entity_Id;
-      Dependency_Num   : Int;
-      Ident_String     : Node_Id;
-      Main_Priority    : Int;
-      Main_CPU         : Int;
-      Serial_Number    : Nat;
-      Version          : Word;
-      Error_Location   : Source_Ptr;
-      Fatal_Error      : Boolean;
-      Generate_Code    : Boolean;
-      Has_RACW         : Boolean;
-      Is_Compiler_Unit : Boolean;
-      Dynamic_Elab     : Boolean;
-      Loading          : Boolean;
-      Has_Allocator    : Boolean;
-      OA_Setting       : Character;
+      Unit_File_Name    : File_Name_Type;
+      Unit_Name         : Unit_Name_Type;
+      Munit_Index       : Nat;
+      Expected_Unit     : Unit_Name_Type;
+      Source_Index      : Source_File_Index;
+      Cunit             : Node_Id;
+      Cunit_Entity      : Entity_Id;
+      Dependency_Num    : Int;
+      Ident_String      : Node_Id;
+      Main_Priority     : Int;
+      Main_CPU          : Int;
+      Serial_Number     : Nat;
+      Version           : Word;
+      Error_Location    : Source_Ptr;
+      Fatal_Error       : Boolean;
+      Generate_Code     : Boolean;
+      Has_RACW          : Boolean;
+      Is_Compiler_Unit  : Boolean;
+      Dynamic_Elab      : Boolean;
+      Loading           : Boolean;
+      Has_Allocator     : Boolean;
+      OA_Setting        : Character;
+      SPARK_Mode_Pragma : Node_Id;
    end record;
 
    --  The following representation clause ensures that the above record
@@ -742,31 +751,32 @@ 
    --  written by Tree_Gen, we do not write uninitialized values to the file.
 
    for Unit_Record use record
-      Unit_File_Name   at  0 range 0 .. 31;
-      Unit_Name        at  4 range 0 .. 31;
-      Munit_Index      at  8 range 0 .. 31;
-      Expected_Unit    at 12 range 0 .. 31;
-      Source_Index     at 16 range 0 .. 31;
-      Cunit            at 20 range 0 .. 31;
-      Cunit_Entity     at 24 range 0 .. 31;
-      Dependency_Num   at 28 range 0 .. 31;
-      Ident_String     at 32 range 0 .. 31;
-      Main_Priority    at 36 range 0 .. 31;
-      Main_CPU         at 40 range 0 .. 31;
-      Serial_Number    at 44 range 0 .. 31;
-      Version          at 48 range 0 .. 31;
-      Error_Location   at 52 range 0 .. 31;
-      Fatal_Error      at 56 range 0 ..  7;
-      Generate_Code    at 57 range 0 ..  7;
-      Has_RACW         at 58 range 0 ..  7;
-      Dynamic_Elab     at 59 range 0 ..  7;
-      Is_Compiler_Unit at 60 range 0 ..  7;
-      OA_Setting       at 61 range 0 ..  7;
-      Loading          at 62 range 0 ..  7;
-      Has_Allocator    at 63 range 0 ..  7;
+      Unit_File_Name    at  0 range 0 .. 31;
+      Unit_Name         at  4 range 0 .. 31;
+      Munit_Index       at  8 range 0 .. 31;
+      Expected_Unit     at 12 range 0 .. 31;
+      Source_Index      at 16 range 0 .. 31;
+      Cunit             at 20 range 0 .. 31;
+      Cunit_Entity      at 24 range 0 .. 31;
+      Dependency_Num    at 28 range 0 .. 31;
+      Ident_String      at 32 range 0 .. 31;
+      Main_Priority     at 36 range 0 .. 31;
+      Main_CPU          at 40 range 0 .. 31;
+      Serial_Number     at 44 range 0 .. 31;
+      Version           at 48 range 0 .. 31;
+      Error_Location    at 52 range 0 .. 31;
+      Fatal_Error       at 56 range 0 ..  7;
+      Generate_Code     at 57 range 0 ..  7;
+      Has_RACW          at 58 range 0 ..  7;
+      Dynamic_Elab      at 59 range 0 ..  7;
+      Is_Compiler_Unit  at 60 range 0 ..  7;
+      OA_Setting        at 61 range 0 ..  7;
+      Loading           at 62 range 0 ..  7;
+      Has_Allocator     at 63 range 0 ..  7;
+      SPARK_Mode_Pragma at 64 range 0 .. 31;
    end record;
 
-   for Unit_Record'Size use 64 * 8;
+   for Unit_Record'Size use 68 * 8;
    --  This ensures that we did not leave out any fields
 
    package Units is new Table.Table (
Index: gnat_rm.texi
===================================================================
--- gnat_rm.texi	(revision 200704)
+++ gnat_rm.texi	(working copy)
@@ -232,6 +232,7 @@ 
 * Pragma Source_File_Name::
 * Pragma Source_File_Name_Project::
 * Pragma Source_Reference::
+* Pragma SPARK_Mode::
 * Pragma Static_Elaboration_Desired::
 * Pragma Stream_Convert::
 * Pragma Style_Checks::
@@ -290,6 +291,7 @@ 
 * Aspect Shared::
 * Aspect Simple_Storage_Pool::
 * Aspect Simple_Storage_Pool_Type::
+* Aspect SPARK_Mode::
 * Aspect Suppress_Debug_Info::
 * Aspect Test_Case::
 * Aspect Universal_Aliasing::
@@ -1044,6 +1046,7 @@ 
 * Pragma Source_File_Name::
 * Pragma Source_File_Name_Project::
 * Pragma Source_Reference::
+* Pragma SPARK_Mode::
 * Pragma Static_Elaboration_Desired::
 * Pragma Stream_Convert::
 * Pragma Style_Checks::
@@ -5996,6 +5999,80 @@ 
 string expression other than a string literal.  This is because its value
 is needed for error messages issued by all phases of the compiler.
 
+@node Pragma SPARK_Mode
+@unnumberedsec Pragma SPARK_Mode
+@findex SPARK_Mode
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma SPARK_Mode [ (On | Off | Auto) ] ;
+@end smallexample
+
+@noindent
+This pragma is used to designate whether a contract and its implementation must
+follow the SPARK 2014 programming language syntactic and semantic rules. The
+pragma is intended for use with formal verification tools and has no effect on
+the generated code.
+
+When used as a configuration pragma over a whole compilation or in a particular
+compilation unit, it sets the mode of the units involved, in particular:
+
+@itemize @bullet
+
+@item
+@code{On}: All entities in the units must follow the SPARK 2014 language, and
+an error will be generated if not, unless locally overridden by a local
+SPARK_Mode pragma or aspect. @code{On} is the default mode when pragma
+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.
+
+@item
+@code{Auto}: The formal verification tools will automatically detect whether
+each entity is in SPARK 2014 or in Ada.
+
+@end itemize
+
+Pragma SPARK_Mode can be used as a local pragma with the following semantics:
+
+@itemize @bullet
+
+@item
+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.
+
+@item
+When the pragma appears immediately within the private declarations of a
+package, it marks the private part in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the declarations of a package body,
+it marks the whole body in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the elaboration statements of a
+package body, it marks the statements in or out of SPARK 2014.
+
+@item
+When the pragma appears after a subprogram declaration, 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.
+
+@item
+Any other use of the pragma is illegal.
+
+@end itemize
+
 @node Pragma Static_Elaboration_Desired
 @unnumberedsec Pragma Static_Elaboration_Desired
 @findex Static_Elaboration_Desired
@@ -6048,8 +6125,7 @@ 
 subtype, and whose returned type must be the type given as the first
 argument to the pragma.
 
-The meaning of the @var{Read}
-parameter is that if a stream attribute directly
+The meaning of the @var{Read} parameter is that if a stream attribute directly
 or indirectly specifies reading of the type given as the first parameter,
 then a value of the type given as the argument to the Read function is
 read from the stream, and then the Read function is used to convert this
@@ -7180,6 +7256,7 @@ 
 * Aspect Shared::
 * Aspect Simple_Storage_Pool::
 * Aspect Simple_Storage_Pool_Type::
+* Aspect SPARK_Mode::
 * Aspect Suppress_Debug_Info::
 * Aspect Test_Case::
 * Aspect Universal_Aliasing::
@@ -7433,6 +7510,12 @@ 
 @noindent
 This aspect is equivalent to pragma @code{Simple_Storage_Pool_Type}.
 
+@node Aspect SPARK_Mode
+@unnumberedsec Aspect SPARK_Mode
+@findex SPARK_Mode
+@noindent
+This aspect is equivalent to pragma @code{SPARK_Mode}.
+
 @node Aspect Suppress_Debug_Info
 @unnumberedsec Aspect Suppress_Debug_Info
 @findex Suppress_Debug_Info
Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 200690)
+++ sinfo.ads	(working copy)
@@ -1539,6 +1539,10 @@ 
    --      Used by processing for Pre/Postcondition pragmas to store a list of
    --      pragmas associated with the spec of a subprogram (see Sem_Prag for
    --      details).
+   --
+   --      Used by processing for pragma SPARK_Mode to store multiple pragmas
+   --      the apply to the same construct. These are visible/private mode for
+   --      a package spec and declarative/statement mode for package body.
 
    --  Next_Rep_Item (Node5-Sem)
    --    Present in pragma nodes, attribute definition nodes, enumeration rep
Index: lib-writ.adb
===================================================================
--- lib-writ.adb	(revision 200688)
+++ lib-writ.adb	(working copy)
@@ -71,28 +71,29 @@ 
    begin
       Units.Increment_Last;
       Units.Table (Units.Last) :=
-        (Unit_File_Name   => File_Name (S),
-         Unit_Name        => No_Unit_Name,
-         Expected_Unit    => No_Unit_Name,
-         Source_Index     => S,
-         Cunit            => Empty,
-         Cunit_Entity     => Empty,
-         Dependency_Num   => 0,
-         Dynamic_Elab     => False,
-         Fatal_Error      => False,
-         Generate_Code    => False,
-         Has_Allocator    => False,
-         Has_RACW         => False,
-         Is_Compiler_Unit => False,
-         Ident_String     => Empty,
-         Loading          => False,
-         Main_Priority    => -1,
-         Main_CPU         => -1,
-         Munit_Index      => 0,
-         Serial_Number    => 0,
-         Version          => 0,
-         Error_Location   => No_Location,
-         OA_Setting       => 'O');
+        (Unit_File_Name    => File_Name (S),
+         Unit_Name         => No_Unit_Name,
+         Expected_Unit     => No_Unit_Name,
+         Source_Index      => S,
+         Cunit             => Empty,
+         Cunit_Entity      => Empty,
+         Dependency_Num    => 0,
+         Dynamic_Elab      => False,
+         Fatal_Error       => False,
+         Generate_Code     => False,
+         Has_Allocator     => False,
+         Has_RACW          => False,
+         Is_Compiler_Unit  => False,
+         Ident_String      => Empty,
+         Loading           => False,
+         Main_Priority     => -1,
+         Main_CPU          => -1,
+         Munit_Index       => 0,
+         Serial_Number     => 0,
+         Version           => 0,
+         Error_Location    => No_Location,
+         OA_Setting        => 'O',
+         SPARK_Mode_Pragma => Empty);
    end Add_Preprocessing_Dependency;
 
    ------------------------------
@@ -128,28 +129,29 @@ 
 
       Units.Increment_Last;
       Units.Table (Units.Last) := (
-        Unit_File_Name   => System_Fname,
-        Unit_Name        => System_Uname,
-        Expected_Unit    => System_Uname,
-        Source_Index     => System_Source_File_Index,
-        Cunit            => Empty,
-        Cunit_Entity     => Empty,
-        Dependency_Num   => 0,
-        Dynamic_Elab     => False,
-        Fatal_Error      => False,
-        Generate_Code    => False,
-        Has_Allocator    => False,
-        Has_RACW         => False,
-        Is_Compiler_Unit => False,
-        Ident_String     => Empty,
-        Loading          => False,
-        Main_Priority    => -1,
-        Main_CPU         => -1,
-        Munit_Index      => 0,
-        Serial_Number    => 0,
-        Version          => 0,
-        Error_Location   => No_Location,
-        OA_Setting       => 'O');
+        Unit_File_Name    => System_Fname,
+        Unit_Name         => System_Uname,
+        Expected_Unit     => System_Uname,
+        Source_Index      => System_Source_File_Index,
+        Cunit             => Empty,
+        Cunit_Entity      => Empty,
+        Dependency_Num    => 0,
+        Dynamic_Elab      => False,
+        Fatal_Error       => False,
+        Generate_Code     => False,
+        Has_Allocator     => False,
+        Has_RACW          => False,
+        Is_Compiler_Unit  => False,
+        Ident_String      => Empty,
+        Loading           => False,
+        Main_Priority     => -1,
+        Main_CPU          => -1,
+        Munit_Index       => 0,
+        Serial_Number     => 0,
+        Version           => 0,
+        Error_Location    => No_Location,
+        OA_Setting        => 'O',
+        SPARK_Mode_Pragma => Empty);
 
       --  Parse system.ads so that the checksum is set right
       --  Style checks are not applied.
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 200688)
+++ einfo.adb	(working copy)
@@ -246,7 +246,7 @@ 
 
    --    Thunk_Entity                    Node31
 
-   --    (unused)                        Node32
+   --    SPARK_Mode_Pragmas              Node32
 
    --    (unused)                        Node33
 
@@ -2825,6 +2825,21 @@ 
       return Ureal21 (Id);
    end Small_Value;
 
+   function SPARK_Mode_Pragmas (Id : E) return N is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Function,         --  subprogram variants
+                       E_Generic_Function,
+                       E_Generic_Procedure,
+                       E_Procedure,
+                       E_Subprogram_Body)
+           or else
+         Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      return Node32 (Id);
+   end SPARK_Mode_Pragmas;
+
    function Spec_Entity (Id : E) return E is
    begin
       pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
@@ -5469,6 +5484,22 @@ 
       Set_Ureal21 (Id, V);
    end Set_Small_Value;
 
+   procedure Set_SPARK_Mode_Pragmas (Id : E; V : N) is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Function,         --  subprogram variants
+                       E_Generic_Function,
+                       E_Generic_Procedure,
+                       E_Procedure,
+                       E_Subprogram_Body)
+           or else
+         Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+
+      Set_Node32 (Id, V);
+   end Set_SPARK_Mode_Pragmas;
+
    procedure Set_Spec_Entity (Id : E; V : E) is
    begin
       pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
@@ -9149,6 +9180,16 @@ 
    procedure Write_Field32_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+         when E_Function                                   |
+              E_Generic_Function                           |
+              E_Generic_Package                            |
+              E_Generic_Procedure                          |
+              E_Package                                    |
+              E_Package_Body                               |
+              E_Procedure                                  |
+              E_Subprogram_Body                            =>
+            Write_Str ("SPARK_Mode_Pragmas");
+
          when others                                       =>
             Write_Str ("Field32??");
       end case;
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 200688)
+++ einfo.ads	(working copy)
@@ -3757,6 +3757,11 @@ 
 --       Small of the type, either as given in a representation clause, or
 --       as computed (as a power of two) by the compiler.
 
+--    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.
+
 --    Spec_Entity (Node19)
 --       Defined in package body entities. Points to corresponding package
 --       spec entity. Also defined in subprogram body parameters in the
@@ -5394,6 +5399,7 @@ 
    --    Subprograms_For_Type                (Node29)
    --    Corresponding_Equality              (Node30)   (implicit /= only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Elaboration_Entity_Required         (Flag174)
    --    Default_Expressions_Processed       (Flag108)
@@ -5591,6 +5597,7 @@ 
    --    Abstract_States                     (Elist25)
    --    Package_Instantiation               (Node26)
    --    Current_Use_Clause                  (Node27)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Discard_Names                       (Flag88)
@@ -5621,6 +5628,7 @@ 
    --    Last_Entity                         (Node20)
    --    Scope_Depth_Value                   (Uint22)
    --    Finalizer                           (Node24)   (non-generic case only)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Has_Anonymous_Master                (Flag253)
    --    Scope_Depth                         (synth)
@@ -5667,6 +5675,7 @@ 
    --    Extra_Formals                       (Node28)
    --    Static_Initialization               (Node30)   (init_proc only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Delay_Cleanups                      (Flag114)
    --    Discard_Names                       (Flag88)
@@ -5837,6 +5846,7 @@ 
    --    Last_Entity                         (Node20)
    --    Scope_Depth_Value                   (Uint22)
    --    Extra_Formals                       (Node28)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Scope_Depth                         (synth)
 
    --  E_Subprogram_Type
@@ -6531,6 +6541,7 @@ 
    function Size_Depends_On_Discriminant        (Id : E) return B;
    function Size_Known_At_Compile_Time          (Id : E) return B;
    function Small_Value                         (Id : E) return R;
+   function SPARK_Mode_Pragmas                  (Id : E) return N;
    function Spec_Entity                         (Id : E) return E;
    function Static_Elaboration_Desired          (Id : E) return B;
    function Static_Initialization               (Id : E) return N;
@@ -7145,6 +7156,7 @@ 
    procedure Set_Size_Depends_On_Discriminant    (Id : E; V : B := True);
    procedure Set_Size_Known_At_Compile_Time      (Id : E; V : B := True);
    procedure Set_Small_Value                     (Id : E; V : R);
+   procedure Set_SPARK_Mode_Pragmas              (Id : E; V : N);
    procedure Set_Spec_Entity                     (Id : E; V : E);
    procedure Set_Static_Elaboration_Desired      (Id : E; V : B);
    procedure Set_Static_Initialization           (Id : E; V : N);
@@ -7891,6 +7903,7 @@ 
    pragma Inline (Size_Depends_On_Discriminant);
    pragma Inline (Size_Known_At_Compile_Time);
    pragma Inline (Small_Value);
+   pragma Inline (SPARK_Mode_Pragmas);
    pragma Inline (Spec_Entity);
    pragma Inline (Static_Elaboration_Desired);
    pragma Inline (Static_Initialization);
@@ -8305,6 +8318,7 @@ 
    pragma Inline (Set_Size_Depends_On_Discriminant);
    pragma Inline (Set_Size_Known_At_Compile_Time);
    pragma Inline (Set_Small_Value);
+   pragma Inline (Set_SPARK_Mode_Pragmas);
    pragma Inline (Set_Spec_Entity);
    pragma Inline (Set_Static_Elaboration_Desired);
    pragma Inline (Set_Static_Initialization);
Index: types.ads
===================================================================
--- types.ads	(revision 200690)
+++ types.ads	(working copy)
@@ -876,4 +876,12 @@ 
      SE_Empty_Storage_Pool ..
      SE_Object_Too_Large;
 
+   ----------------------------------------
+   -- Types Used for SPARK Mode Handling --
+   ----------------------------------------
+
+   type SPARK_Mode_Id is (None, SPARK_Off, SPARK_Auto, SPARK_On);
+   --  Type used to represent all legal modes that can be set by aspect/pragma
+   --  SPARK_Mode.
+
 end Types;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 200704)
+++ sem_prag.adb	(working copy)
@@ -213,6 +213,11 @@ 
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
+   function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id;
+   --  Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
+   --  Get_SPARK_Mode_Id. Convert a name into a corresponding value of type
+   --  SPARK_Mode_Id.
+
    function Original_Name (N : Node_Id) return Name_Id;
    --  N is a pragma node or aspect specification node. This function returns
    --  the name of the pragma or aspect in original source form, taking into
@@ -16315,6 +16320,351 @@ 
          when Pragma_Source_Reference =>
             GNAT_Pragma;
 
+         ----------------
+         -- SPARK_Mode --
+         ----------------
+
+         --  pragma SPARK_Mode (On | Off | Auto);
+
+         when Pragma_SPARK_Mode => SPARK_Mod : declare
+            procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id);
+            --  Associate a SPARK_Mode pragma with the context where it lives.
+            --  If the context is a package spec or a body, the routine checks
+            --  the consistency between modes of visible/private declarations
+            --  and body declarations/statements.
+
+            procedure Check_Conformance
+              (Governing_Id : Entity_Id;
+               New_Id       : Entity_Id);
+            --  Verify the "monotonicity" of SPARK modes between two entities.
+            --  The order of modes is Off < Auto < On. Governing_Id establishes
+            --  the mode of the context. New_Id attempts to redefine the known
+            --  mode.
+
+            procedure Check_Pragma_Conformance
+              (Governing_Mode : Node_Id;
+               New_Mode       : Node_Id);
+            --  Verify the "monotonicity" of two SPARK_Mode pragmas. The order
+            --  of modes is Off < Auto < On. Governing_Mode is the established
+            --  mode dictated by the context. New_Mode attempts to redefine the
+            --  governing mode.
+
+            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 --
+            ------------------
+
+            procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id) is
+               Existing_Prag : constant Node_Id :=
+                                 SPARK_Mode_Pragmas (Context);
+            begin
+               --  The context does not have a prior mode defined
+
+               if No (Existing_Prag) then
+                  Set_SPARK_Mode_Pragmas (Context, Prag);
+
+               --  Chain the new mode on the list of SPARK_Mode pragmas. Verify
+               --  the consistency between the existing mode and the new one.
+
+               else
+                  Set_Next_Pragma (Existing_Prag, Prag);
+
+                  Check_Pragma_Conformance
+                    (Governing_Mode => Existing_Prag,
+                     New_Mode       => Prag);
+               end if;
+            end Chain_Pragma;
+
+            -----------------------
+            -- Check_Conformance --
+            -----------------------
+
+            procedure Check_Conformance
+              (Governing_Id : Entity_Id;
+               New_Id       : Entity_Id)
+            is
+               Gov_Prag : constant Node_Id :=
+                            SPARK_Mode_Pragmas (Governing_Id);
+               New_Prag : constant Node_Id := SPARK_Mode_Pragmas (New_Id);
+
+            begin
+               --  Nothing to do when one or both entities lack a mode
+
+               if No (Gov_Prag) or else No (New_Prag) then
+                  return;
+               end if;
+
+               --  Do not compare the modes of a package spec and body when the
+               --  spec mode appears in the private part. In this case the spec
+               --  mode does not affect the body.
+
+               if Ekind_In (Governing_Id, E_Generic_Package, E_Package)
+                 and then Ekind (New_Id) = E_Package_Body
+                 and then Is_Private_SPARK_Mode (Gov_Prag)
+               then
+                  null;
+
+               --  Test the pragmas
+
+               else
+                  Check_Pragma_Conformance
+                    (Governing_Mode => Gov_Prag,
+                     New_Mode       => New_Prag);
+               end if;
+            end Check_Conformance;
+
+            ------------------------------
+            -- Check_Pragma_Conformance --
+            ------------------------------
+
+            procedure Check_Pragma_Conformance
+              (Governing_Mode : Node_Id;
+               New_Mode       : Node_Id)
+            is
+               Gov_M : constant SPARK_Mode_Id :=
+                         Get_SPARK_Mode_Id (Governing_Mode);
+               New_M : constant SPARK_Mode_Id := Get_SPARK_Mode_Id (New_Mode);
+
+            begin
+               --  The new mode is less restrictive than the established mode
+
+               if Gov_M < New_M then
+                  Error_Msg_Name_1 := Get_SPARK_Mode_Name (New_M);
+                  Error_Msg_N ("cannot define 'S'P'A'R'K mode %", New_Mode);
+
+                  Error_Msg_Name_1 := Get_SPARK_Mode_Name (Gov_M);
+                  Error_Msg_Sloc   := Sloc (Governing_Mode);
+                  Error_Msg_N
+                    ("\mode is less restrictive than mode % defined #",
+                     New_Mode);
+               end if;
+            end Check_Pragma_Conformance;
+
+            -------------------------
+            -- Get_SPARK_Mode_Name --
+            -------------------------
+
+            function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id is
+            begin
+               if Id = SPARK_On then
+                  return Name_On;
+               elsif Id = SPARK_Off then
+                  return Name_Off;
+               elsif Id = SPARK_Auto then
+                  return Name_Auto;
+
+               --  Mode "None" should never be used in error message generation
+
+               else
+                  raise Program_Error;
+               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;
+
+         --  Start of processing for SPARK_Mode
+
+         begin
+            GNAT_Pragma;
+            Check_No_Identifiers;
+            Check_At_Most_N_Arguments (1);
+
+            --  Check the legality of the mode
+
+            if Arg_Count = 1 then
+               Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_Auto);
+               Mode := Chars (Get_Pragma_Arg (Arg1));
+
+            --  A SPARK_Mode without an argument defaults to "On"
+
+            else
+               Mode := Name_On;
+            end if;
+
+            Mode_Id := Get_SPARK_Mode_Id (Mode);
+            Context := Parent (N);
+
+            --  The pragma appears in a configuration file
+
+            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;
+
+            --  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;
+
+            --  The pragma applies to a [library unit] subprogram or package
+
+            else
+               --  Mode "Auto" cannot be used in nested subprograms or packages
+
+               if Mode_Id = SPARK_Auto then
+                  Error_Pragma_Arg
+                    ("mode `Auto` can only apply to the configuration variant "
+                     & "of pragma %", Arg1);
+               end if;
+
+               --  Verify the placement of the pragma with respect to package
+               --  or subprogram declarations and detect duplicates.
+
+               Stmt := Prev (N);
+               while Present (Stmt) loop
+
+                  --  Skip prior pragmas, but check for duplicates
+
+                  if Nkind (Stmt) = N_Pragma then
+                     if Pragma_Name (Stmt) = Pname then
+                        Error_Msg_Name_1 := Pname;
+                        Error_Msg_Sloc   := Sloc (Stmt);
+                        Error_Msg_N
+                          ("pragma % duplicates pragma declared #", N);
+                     end if;
+
+                  --  Skip internally generated code
+
+                  elsif not Comes_From_Source (Stmt) then
+                     null;
+
+                  --  The pragma applies to a package or subprogram declaration
+
+                  elsif Nkind_In (Stmt, N_Generic_Package_Declaration,
+                                        N_Generic_Subprogram_Declaration,
+                                        N_Package_Declaration,
+                                        N_Subprogram_Declaration)
+                  then
+                     Spec_Id := Defining_Unit_Name (Specification (Stmt));
+                     Chain_Pragma (Spec_Id, N);
+                     return;
+
+                  --  The pragma does not apply to a legal construct, issue an
+                  --  error and stop the analysis.
+
+                  else
+                     Pragma_Misplaced;
+                     exit;
+                  end if;
+
+                  Stmt := Prev (Stmt);
+               end loop;
+
+               --  If we get here, then we ran out of preceding statements. The
+               --  pragma is immediately within a body.
+
+               if Nkind_In (Context, N_Package_Body,
+                                     N_Subprogram_Body)
+               then
+                  Spec_Id := Corresponding_Spec (Context);
+
+                  if Nkind (Context) = N_Subprogram_Body then
+                     Context := Specification (Context);
+                  end if;
+
+                  Body_Id := Defining_Unit_Name (Context);
+
+                  Chain_Pragma (Body_Id, N);
+                  Check_Conformance (Spec_Id, Body_Id);
+
+               --  The pragma is at the top level of a package spec
+
+               elsif Nkind (Context) = N_Package_Specification then
+                  Spec_Id := Defining_Unit_Name (Context);
+                  Chain_Pragma (Spec_Id, N);
+
+               --  The pragma applies to the statements of a package body
+
+               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_Unit_Name (Context);
+
+                  Chain_Pragma (Body_Id, N);
+                  Check_Conformance (Spec_Id, Body_Id);
+
+               --  The pragma does not apply to a legal construct, issue an
+               --  error.
+
+               else
+                  Pragma_Misplaced;
+               end if;
+            end if;
+         end SPARK_Mod;
+
          --------------------------------
          -- Static_Elaboration_Desired --
          --------------------------------
@@ -18268,6 +18618,43 @@ 
       return Result;
    end Get_Base_Subprogram;
 
+   -----------------------
+   -- Get_SPARK_Mode_Id --
+   -----------------------
+
+   function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id is
+   begin
+      if N = Name_On then
+         return SPARK_On;
+      elsif N = Name_Off then
+         return SPARK_Off;
+      elsif N = Name_Auto then
+         return SPARK_Auto;
+
+      --  Any other argument is erroneous
+
+      else
+         raise Program_Error;
+      end if;
+   end Get_SPARK_Mode_Id;
+
+   -----------------------
+   -- Get_SPARK_Mode_Id --
+   -----------------------
+
+   function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id is
+      Mode : Node_Id;
+
+   begin
+      pragma Assert
+        (Nkind (N) = N_Pragma
+          and then Present (Pragma_Argument_Associations (N)));
+
+      Mode := First (Pragma_Argument_Associations (N));
+
+      return Get_SPARK_Mode_Id (Chars (Get_Pragma_Arg (Mode)));
+   end Get_SPARK_Mode_Id;
+
    ----------------
    -- Initialize --
    ----------------
@@ -18332,11 +18719,33 @@ 
    --  Start of processing for Is_Config_Static_String
 
    begin
+      Name_Len := 0;
 
-      Name_Len := 0;
       return Add_Config_Static_String (Arg);
    end Is_Config_Static_String;
 
+   -------------------------------
+   -- Is_Elaboration_SPARK_Mode --
+   -------------------------------
+
+   function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean is
+   begin
+      pragma Assert
+        (Nkind (N) = N_Pragma
+          and then Pragma_Name (N) = Name_SPARK_Mode
+          and then Is_List_Member (N));
+
+      --  Pragma SPARK_Mode affects the elaboration of a package body when it
+      --  appears in the statement part of the body.
+
+      return
+         Present (Parent (N))
+           and then Nkind (Parent (N)) = N_Handled_Sequence_Of_Statements
+           and then List_Containing (N) = Statements (Parent (N))
+           and then Present (Parent (Parent (N)))
+           and then Nkind (Parent (Parent (N))) = N_Package_Body;
+   end Is_Elaboration_SPARK_Mode;
+
    -----------------------------------------
    -- Is_Non_Significant_Pragma_Reference --
    -----------------------------------------
@@ -18524,6 +18933,7 @@ 
       Pragma_Source_File_Name               => -1,
       Pragma_Source_File_Name_Project       => -1,
       Pragma_Source_Reference               => -1,
+      Pragma_SPARK_Mode                     =>  0,
       Pragma_Storage_Size                   => -1,
       Pragma_Storage_Unit                   => -1,
       Pragma_Static_Elaboration_Desired     => -1,
@@ -18682,6 +19092,26 @@ 
       end if;
    end Is_Pragma_String_Literal;
 
+   ---------------------------
+   -- Is_Private_SPARK_Mode --
+   ---------------------------
+
+   function Is_Private_SPARK_Mode (N : Node_Id) return Boolean is
+   begin
+      pragma Assert
+        (Nkind (N) = N_Pragma
+          and then Pragma_Name (N) = Name_SPARK_Mode
+          and then Is_List_Member (N));
+
+      --  For pragma SPARK_Mode to be private, it has to appear in the private
+      --  declarations of a package.
+
+      return
+        Present (Parent (N))
+          and then Nkind (Parent (N)) = N_Package_Specification
+          and then List_Containing (N) = Private_Declarations (Parent (N));
+   end Is_Private_SPARK_Mode;
+
    -----------------------------
    -- Is_Valid_Assertion_Kind --
    -----------------------------
Index: sem_prag.ads
===================================================================
--- sem_prag.ads	(revision 200688)
+++ sem_prag.ads	(working copy)
@@ -113,6 +113,9 @@ 
    --  True have their analysis delayed until after the main program is parsed
    --  and analyzed.
 
+   function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id;
+   --  Given a pragma SPARK_Mode node, return the corresponding mode id
+
    procedure Initialize;
    --  Initializes data structures used for pragma processing. Must be called
    --  before analyzing each new main source program.
@@ -127,6 +130,10 @@ 
    --  length, and then returns True. If it is not of the correct form, then an
    --  appropriate error message is posted, and False is returned.
 
+   function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean;
+   --  Determine whether pragma SPARK_Mode appears in the statement part of a
+   --  package body.
+
    function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
    --  The node N is a node for an entity and the issue is whether the
    --  occurrence is a reference for the purposes of giving warnings about
@@ -143,6 +150,10 @@ 
    --  False is returned, then the argument is treated as an entity reference
    --  to the operator.
 
+   function Is_Private_SPARK_Mode (N : Node_Id) return Boolean;
+   --  Determine whether pragma SPARK_Mode appears in the private part of a
+   --  package.
+
    function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
    --  Returns True if Nam is one of the names recognized as a valid assertion
    --  kind by the Assertion_Policy pragma. Note that the 'Class cases are
Index: gnat_ugn.texi
===================================================================
--- gnat_ugn.texi	(revision 200705)
+++ gnat_ugn.texi	(working copy)
@@ -11611,6 +11611,7 @@ 
    Short_Circuit_And_Or
    Source_File_Name
    Source_File_Name_Project
+   SPARK_Mode
    Style_Checks
    Suppress
    Suppress_Exception_Locations
Index: aspects.adb
===================================================================
--- aspects.adb	(revision 200688)
+++ aspects.adb	(working copy)
@@ -403,6 +403,7 @@ 
     Aspect_Simple_Storage_Pool_Type     => Aspect_Simple_Storage_Pool_Type,
     Aspect_Size                         => Aspect_Size,
     Aspect_Small                        => Aspect_Small,
+    Aspect_SPARK_Mode                   => Aspect_SPARK_Mode,
     Aspect_Static_Predicate             => Aspect_Predicate,
     Aspect_Storage_Pool                 => Aspect_Storage_Pool,
     Aspect_Storage_Size                 => Aspect_Storage_Size,
Index: aspects.ads
===================================================================
--- aspects.ads	(revision 200688)
+++ aspects.ads	(working copy)
@@ -116,6 +116,7 @@ 
       Aspect_Simple_Storage_Pool,           -- GNAT
       Aspect_Size,
       Aspect_Small,
+      Aspect_SPARK_Mode,                    -- GNAT
       Aspect_Static_Predicate,
       Aspect_Storage_Pool,
       Aspect_Storage_Size,
@@ -322,6 +323,7 @@ 
       Aspect_Simple_Storage_Pool     => Name,
       Aspect_Size                    => Expression,
       Aspect_Small                   => Expression,
+      Aspect_SPARK_Mode              => Name,
       Aspect_Static_Predicate        => Expression,
       Aspect_Storage_Pool            => Name,
       Aspect_Storage_Size            => Expression,
@@ -423,6 +425,7 @@ 
       Aspect_Simple_Storage_Pool_Type     => Name_Simple_Storage_Pool_Type,
       Aspect_Size                         => Name_Size,
       Aspect_Small                        => Name_Small,
+      Aspect_SPARK_Mode                   => Name_SPARK_Mode,
       Aspect_Static_Predicate             => Name_Static_Predicate,
       Aspect_Storage_Pool                 => Name_Storage_Pool,
       Aspect_Storage_Size                 => Name_Storage_Size,
Index: lib-load.adb
===================================================================
--- lib-load.adb	(revision 200688)
+++ lib-load.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -206,28 +206,29 @@ 
       Unum := Units.Last;
 
       Units.Table (Unum) := (
-        Cunit            => Cunit,
-        Cunit_Entity     => Cunit_Entity,
-        Dependency_Num   => 0,
-        Dynamic_Elab     => False,
-        Error_Location   => Sloc (With_Node),
-        Expected_Unit    => Spec_Name,
-        Fatal_Error      => True,
-        Generate_Code    => False,
-        Has_Allocator    => False,
-        Has_RACW         => False,
-        Is_Compiler_Unit => False,
-        Ident_String     => Empty,
-        Loading          => False,
-        Main_Priority    => Default_Main_Priority,
-        Main_CPU         => Default_Main_CPU,
-        Munit_Index      => 0,
-        Serial_Number    => 0,
-        Source_Index     => No_Source_File,
-        Unit_File_Name   => Get_File_Name (Spec_Name, Subunit => False),
-        Unit_Name        => Spec_Name,
-        Version          => 0,
-        OA_Setting       => 'O');
+        Cunit             => Cunit,
+        Cunit_Entity      => Cunit_Entity,
+        Dependency_Num    => 0,
+        Dynamic_Elab      => False,
+        Error_Location    => Sloc (With_Node),
+        Expected_Unit     => Spec_Name,
+        Fatal_Error       => True,
+        Generate_Code     => False,
+        Has_Allocator     => False,
+        Has_RACW          => False,
+        Is_Compiler_Unit  => False,
+        Ident_String      => Empty,
+        Loading           => False,
+        Main_Priority     => Default_Main_Priority,
+        Main_CPU          => Default_Main_CPU,
+        Munit_Index       => 0,
+        Serial_Number     => 0,
+        Source_Index      => No_Source_File,
+        Unit_File_Name    => Get_File_Name (Spec_Name, Subunit => False),
+        Unit_Name         => Spec_Name,
+        Version           => 0,
+        OA_Setting        => 'O',
+        SPARK_Mode_Pragma => Empty);
 
       Set_Comes_From_Source_Default (Save_CS);
       Set_Error_Posted (Cunit_Entity);
@@ -312,28 +313,29 @@ 
          end if;
 
          Units.Table (Main_Unit) := (
-           Cunit            => Empty,
-           Cunit_Entity     => Empty,
-           Dependency_Num   => 0,
-           Dynamic_Elab     => False,
-           Error_Location   => No_Location,
-           Expected_Unit    => No_Unit_Name,
-           Fatal_Error      => False,
-           Generate_Code    => False,
-           Has_Allocator    => False,
-           Has_RACW         => False,
-           Is_Compiler_Unit => False,
-           Ident_String     => Empty,
-           Loading          => True,
-           Main_Priority    => Default_Main_Priority,
-           Main_CPU         => Default_Main_CPU,
-           Munit_Index      => 0,
-           Serial_Number    => 0,
-           Source_Index     => Main_Source_File,
-           Unit_File_Name   => Fname,
-           Unit_Name        => No_Unit_Name,
-           Version          => Version,
-           OA_Setting       => 'O');
+           Cunit             => Empty,
+           Cunit_Entity      => Empty,
+           Dependency_Num    => 0,
+           Dynamic_Elab      => False,
+           Error_Location    => No_Location,
+           Expected_Unit     => No_Unit_Name,
+           Fatal_Error       => False,
+           Generate_Code     => False,
+           Has_Allocator     => False,
+           Has_RACW          => False,
+           Is_Compiler_Unit  => False,
+           Ident_String      => Empty,
+           Loading           => True,
+           Main_Priority     => Default_Main_Priority,
+           Main_CPU          => Default_Main_CPU,
+           Munit_Index       => 0,
+           Serial_Number     => 0,
+           Source_Index      => Main_Source_File,
+           Unit_File_Name    => Fname,
+           Unit_Name         => No_Unit_Name,
+           Version           => Version,
+           OA_Setting        => 'O',
+           SPARK_Mode_Pragma => Empty);
       end if;
    end Load_Main_Source;
 
@@ -675,28 +677,29 @@ 
 
          if Src_Ind /= No_Source_File then
             Units.Table (Unum) := (
-              Cunit            => Empty,
-              Cunit_Entity     => Empty,
-              Dependency_Num   => 0,
-              Dynamic_Elab     => False,
-              Error_Location   => Sloc (Error_Node),
-              Expected_Unit    => Uname_Actual,
-              Fatal_Error      => False,
-              Generate_Code    => False,
-              Has_Allocator    => False,
-              Has_RACW         => False,
-              Is_Compiler_Unit => False,
-              Ident_String     => Empty,
-              Loading          => True,
-              Main_Priority    => Default_Main_Priority,
-              Main_CPU         => Default_Main_CPU,
-              Munit_Index      => 0,
-              Serial_Number    => 0,
-              Source_Index     => Src_Ind,
-              Unit_File_Name   => Fname,
-              Unit_Name        => Uname_Actual,
-              Version          => Source_Checksum (Src_Ind),
-              OA_Setting       => 'O');
+              Cunit             => Empty,
+              Cunit_Entity      => Empty,
+              Dependency_Num    => 0,
+              Dynamic_Elab      => False,
+              Error_Location    => Sloc (Error_Node),
+              Expected_Unit     => Uname_Actual,
+              Fatal_Error       => False,
+              Generate_Code     => False,
+              Has_Allocator     => False,
+              Has_RACW          => False,
+              Is_Compiler_Unit  => False,
+              Ident_String      => Empty,
+              Loading           => True,
+              Main_Priority     => Default_Main_Priority,
+              Main_CPU          => Default_Main_CPU,
+              Munit_Index       => 0,
+              Serial_Number     => 0,
+              Source_Index      => Src_Ind,
+              Unit_File_Name    => Fname,
+              Unit_Name         => Uname_Actual,
+              Version           => Source_Checksum (Src_Ind),
+              OA_Setting        => 'O',
+              SPARK_Mode_Pragma => Empty);
 
             --  Parse the new unit
 
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 200688)
+++ par-prag.adb	(working copy)
@@ -1262,6 +1262,7 @@ 
            Pragma_Short_Circuit_And_Or           |
            Pragma_Short_Descriptors              |
            Pragma_Simple_Storage_Pool_Type       |
+           Pragma_SPARK_Mode                     |
            Pragma_Storage_Size                   |
            Pragma_Storage_Unit                   |
            Pragma_Static_Elaboration_Desired     |
Index: atree.adb
===================================================================
--- atree.adb	(revision 200688)
+++ atree.adb	(working copy)
@@ -2532,6 +2532,12 @@ 
          return Node_Id (Nodes.Table (N + 5).Field7);
       end Node31;
 
+      function Node32 (N : Node_Id) return Node_Id is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         return Node_Id (Nodes.Table (N + 5).Field8);
+      end Node32;
+
       function List1 (N : Node_Id) return List_Id is
       begin
          pragma Assert (N <= Nodes.Last);
@@ -5243,6 +5249,12 @@ 
          Nodes.Table (N + 5).Field7 := Union_Id (Val);
       end Set_Node31;
 
+      procedure Set_Node32 (N : Node_Id; Val : Node_Id) is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         Nodes.Table (N + 5).Field8 := Union_Id (Val);
+      end Set_Node32;
+
       procedure Set_List1 (N : Node_Id; Val : List_Id) is
       begin
          pragma Assert (N <= Nodes.Last);
Index: atree.ads
===================================================================
--- atree.ads	(revision 200688)
+++ atree.ads	(working copy)
@@ -1174,6 +1174,9 @@ 
       function Node31 (N : Node_Id) return Node_Id;
       pragma Inline (Node31);
 
+      function Node32 (N : Node_Id) return Node_Id;
+      pragma Inline (Node32);
+
       function List1 (N : Node_Id) return List_Id;
       pragma Inline (List1);
 
@@ -2459,6 +2462,9 @@ 
       procedure Set_Node31 (N : Node_Id; Val : Node_Id);
       pragma Inline (Set_Node31);
 
+      procedure Set_Node32 (N : Node_Id; Val : Node_Id);
+      pragma Inline (Set_Node32);
+
       procedure Set_List1 (N : Node_Id; Val : List_Id);
       pragma Inline (Set_List1);
 
Index: opt.ads
===================================================================
--- opt.ads	(revision 200698)
+++ opt.ads	(working copy)
@@ -1970,6 +1970,21 @@ 
    -- Modes for Formal Verification --
    -----------------------------------
 
+   Frame_Condition_Mode : Boolean := False;
+   --  Specific mode to be used in combination with SPARK_Mode. If set to
+   --  true, ALI files containing the frame conditions (global effects) are
+   --  generated, and Why files are *not* generated. If not true, Why files
+   --  are generated. Set by debug flag -gnatd.G.
+
+   Formal_Extensions : Boolean := False;
+   --  When this flag is set, new aspects/pragmas/attributes are accepted,
+   --  whose main purpose is to facilitate formal verification. Set by debug
+   --  flag -gnatd.V.
+
+   Global_SPARK_Mode : SPARK_Mode_Id := None;
+   --  The mode applicable to the whole compilation. The global mode can be set
+   --  in a configuration file such as gnat.adc.
+
    SPARK_Mode : Boolean := False;
    --  Specific compiling mode targeting formal verification through the
    --  generation of Why code for those parts of the input code that belong to
@@ -1978,22 +1993,11 @@ 
    --  from the SPARK restriction defined in GNAT to detect violations of a
    --  subset of SPARK 2005 rules.
 
-   Frame_Condition_Mode : Boolean := False;
-   --  Specific mode to be used in combination with SPARK_Mode. If set to
-   --  true, ALI files containing the frame conditions (global effects) are
-   --  generated, and Why files are *not* generated. If not true, Why files
-   --  are generated. Set by debug flag -gnatd.G.
-
    SPARK_Strict_Mode : Boolean := False;
    --  Interpret compiler permissions as strictly as possible. E.g. base ranges
    --  for integers are limited to the strict minimum with this option. Set by
    --  debug flag -gnatd.D.
 
-   Formal_Extensions : Boolean := False;
-   --  When this flag is set, new aspects/pragmas/attributes are accepted,
-   --  whose main purpose is to facilitate formal verification. Set by debug
-   --  flag -gnatd.V.
-
    function Full_Expander_Active return Boolean;
    pragma Inline (Full_Expander_Active);
    --  Returns the value of (Expander_Active and not SPARK_Mode). This "flag"
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 200710)
+++ sem_ch13.adb	(working copy)
@@ -1659,6 +1659,16 @@ 
                   Insert_Delayed_Pragma (Aitem);
                   goto Continue;
 
+               --  SPARK_Mode
+
+               when Aspect_SPARK_Mode =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_SPARK_Mode);
+                  Delay_Required := False;
+
                --  Relative_Deadline
 
                when Aspect_Relative_Deadline =>
@@ -7390,6 +7400,7 @@ 
               Aspect_Postcondition        |
               Aspect_Pre                  |
               Aspect_Precondition         |
+              Aspect_SPARK_Mode           |
               Aspect_Test_Case     =>
             raise Program_Error;
 
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 200688)
+++ snames.ads-tmpl	(working copy)
@@ -436,6 +436,7 @@ 
    Name_Short_Descriptors              : constant Name_Id := N + $; -- GNAT
    Name_Source_File_Name               : constant Name_Id := N + $; -- GNAT
    Name_Source_File_Name_Project       : constant Name_Id := N + $; -- GNAT
+   Name_SPARK_Mode                     : constant Name_Id := N + $; -- GNAT
    Name_Style_Checks                   : constant Name_Id := N + $; -- GNAT
    Name_Suppress                       : constant Name_Id := N + $;
    Name_Suppress_Exception_Locations   : constant Name_Id := N + $; -- GNAT
@@ -673,6 +674,7 @@ 
    Name_Assertion                      : constant Name_Id := N + $;
    Name_Assertions                     : constant Name_Id := N + $;
    Name_Attribute_Name                 : constant Name_Id := N + $;
+   Name_Auto                           : constant Name_Id := N + $;
    Name_Body_File_Name                 : constant Name_Id := N + $;
    Name_Boolean_Entry_Barriers         : constant Name_Id := N + $;
    Name_By_Any                         : constant Name_Id := N + $;
@@ -1748,6 +1750,7 @@ 
       Pragma_Short_Descriptors,
       Pragma_Source_File_Name,
       Pragma_Source_File_Name_Project,
+      Pragma_SPARK_Mode,
       Pragma_Style_Checks,
       Pragma_Suppress,
       Pragma_Suppress_Exception_Locations,