===================================================================
@@ -2595,6 +2595,12 @@
return Node_Id (Nodes.Table (N + 5).Field8);
end Node32;
+ function Node33 (N : Node_Id) return Node_Id is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ return Node_Id (Nodes.Table (N + 5).Field9);
+ end Node33;
+
function List1 (N : Node_Id) return List_Id is
begin
pragma Assert (N <= Nodes.Last);
@@ -5336,6 +5342,12 @@
Nodes.Table (N + 5).Field8 := Union_Id (Val);
end Set_Node32;
+ procedure Set_Node33 (N : Node_Id; Val : Node_Id) is
+ begin
+ pragma Assert (Nkind (N) in N_Entity);
+ Nodes.Table (N + 5).Field9 := Union_Id (Val);
+ end Set_Node33;
+
procedure Set_List1 (N : Node_Id; Val : List_Id) is
begin
pragma Assert (N <= Nodes.Last);
===================================================================
@@ -1209,6 +1209,9 @@
function Node32 (N : Node_Id) return Node_Id;
pragma Inline (Node32);
+ function Node33 (N : Node_Id) return Node_Id;
+ pragma Inline (Node33);
+
function List1 (N : Node_Id) return List_Id;
pragma Inline (List1);
@@ -2509,6 +2512,9 @@
procedure Set_Node32 (N : Node_Id; Val : Node_Id);
pragma Inline (Set_Node32);
+ procedure Set_Node33 (N : Node_Id; Val : Node_Id);
+ pragma Inline (Set_Node33);
+
procedure Set_List1 (N : Node_Id; Val : List_Id);
pragma Inline (Set_List1);
===================================================================
@@ -248,9 +248,9 @@
-- Thunk_Entity Node31
- -- SPARK_Mode_Pragmas Node32
+ -- SPARK_Pragma Node32
- -- (unused) Node33
+ -- SPARK_Aux_Pragma Node33
-- (unused) Node34
@@ -554,9 +554,9 @@
-- May_Inherit_Delayed_Rep_Aspects Flag262
-- Has_Visible_Refinement Flag263
-- Has_Body_References Flag264
+ -- SPARK_Pragma_Inherited Flag265
+ -- SPARK_Aux_Pragma_Inherited Flag266
- -- (unused) Flag265
- -- (unused) Flag266
-- (unused) Flag267
-- (unused) Flag268
-- (unused) Flag269
@@ -2835,9 +2835,27 @@
return Ureal21 (Id);
end Small_Value;
- function SPARK_Mode_Pragmas (Id : E) return N is
+ function SPARK_Aux_Pragma (Id : E) return N is
begin
pragma Assert
+ (Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+ return Node33 (Id);
+ end SPARK_Aux_Pragma;
+
+ function SPARK_Aux_Pragma_Inherited (Id : E) return B is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+ return Flag266 (Id);
+ end SPARK_Aux_Pragma_Inherited;
+
+ function SPARK_Pragma (Id : E) return N is
+ begin
+ pragma Assert
(Ekind_In (Id, E_Function, -- subprogram variants
E_Generic_Function,
E_Generic_Procedure,
@@ -2848,8 +2866,23 @@
E_Package,
E_Package_Body));
return Node32 (Id);
- end SPARK_Mode_Pragmas;
+ end SPARK_Pragma;
+ function SPARK_Pragma_Inherited (Id : E) return B 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 Flag265 (Id);
+ end SPARK_Pragma_Inherited;
+
function Spec_Entity (Id : E) return E is
begin
pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
@@ -5527,9 +5560,29 @@
Set_Ureal21 (Id, V);
end Set_Small_Value;
- procedure Set_SPARK_Mode_Pragmas (Id : E; V : N) is
+ procedure Set_SPARK_Aux_Pragma (Id : E; V : N) is
begin
pragma Assert
+ (Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+
+ Set_Node33 (Id, V);
+ end Set_SPARK_Aux_Pragma;
+
+ procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is
+ begin
+ pragma Assert
+ (Ekind_In (Id, E_Generic_Package, -- package variants
+ E_Package,
+ E_Package_Body));
+
+ Set_Flag266 (Id, V);
+ end Set_SPARK_Aux_Pragma_Inherited;
+
+ procedure Set_SPARK_Pragma (Id : E; V : N) is
+ begin
+ pragma Assert
(Ekind_In (Id, E_Function, -- subprogram variants
E_Generic_Function,
E_Generic_Procedure,
@@ -5541,8 +5594,24 @@
E_Package_Body));
Set_Node32 (Id, V);
- end Set_SPARK_Mode_Pragmas;
+ end Set_SPARK_Pragma;
+ procedure Set_SPARK_Pragma_Inherited (Id : E; V : B := True) 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_Flag265 (Id, V);
+ end Set_SPARK_Pragma_Inherited;
+
procedure Set_Spec_Entity (Id : E; V : E) is
begin
pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
@@ -8227,6 +8296,8 @@
W ("Sec_Stack_Needed_For_Return", Flag167 (Id));
W ("Size_Depends_On_Discriminant", Flag177 (Id));
W ("Size_Known_At_Compile_Time", Flag92 (Id));
+ W ("SPARK_Aux_Pragma_Inherited", Flag266 (Id));
+ W ("SPARK_Pragma_Inherited", Flag265 (Id));
W ("Static_Elaboration_Desired", Flag77 (Id));
W ("Strict_Alignment", Flag145 (Id));
W ("Suppress_Elaboration_Warnings", Flag148 (Id));
@@ -9366,7 +9437,7 @@
E_Package_Body |
E_Procedure |
E_Subprogram_Body =>
- Write_Str ("SPARK_Mode_Pragmas");
+ Write_Str ("SPARK_Pragma");
when others =>
Write_Str ("Field32??");
@@ -9380,6 +9451,11 @@
procedure Write_Field33_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when E_Generic_Package |
+ E_Package |
+ E_Package_Body =>
+ Write_Str ("SPARK_Aux_Pragma");
+
when others =>
Write_Str ("Field33??");
end case;
===================================================================
@@ -3801,11 +3801,36 @@
-- Small of the type, either as given in a representation clause, or
-- as computed (as a power of two) by the compiler.
+-- SPARK_Aux_Pragma (Node33)
+-- Present in package spec and body entities. For a package spec entity
+-- it relates to the SPARK mode setting for the private part. This field
+-- points to the N_Pragma node that applies to the private part. This is
+-- either set with a local SPARK_Mode pragma in the private part or it is
+-- inherited from the SPARK mode that applies to the rest of the spec.
+-- For a package body, it similarly applies to the SPARK mode setting for
+-- the elaboration sequence after the BEGIN. In the case where the pragma
+-- is inherited, the SPARK_Aux_Pragma_Inherited flag is set in the
+-- package spec or body entity.
+
+-- SPARK_Aux_Pragma_Inherited (Flag266)
+-- Present in the entities of subprogram specs and bodies as well as
+-- in package specs and bodies. Set if the SPARK_Aux_Pragma field
+-- points to a pragma that is inherited, rather than a local one.
+
+-- SPARK_Pragma (Node32)
-- Present in the entities of subprogram specs and bodies as well as in
+-- package specs and bodies. Points to the N_Pragma node that applies to
+-- the spec or body. This is either set by a local SPARK_Mode pragma or
+-- is inherited from the context (from an outer scope for the spec case
+-- or from the spec for the body case). In the case where it is inherited
+-- the flag SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma
+-- is applicable.
+-- SPARK_Pragma_Inherited (Flag265)
+-- Present in the entities of subprogram specs and bodies as well as in
+-- package specs and bodies. Set if the SPARK_Pragma field points to a
+-- pragma that is inherited, rather than a local one.
+
-- Spec_Entity (Node19)
-- Defined in package body entities. Points to corresponding package
-- spec entity. Also defined in subprogram body parameters in the
@@ -5455,7 +5480,7 @@
-- Subprograms_For_Type (Node29)
-- Corresponding_Equality (Node30) (implicit /= only)
-- Thunk_Entity (Node31) (thunk case only)
- -- SPARK_Mode_Pragmas (Node32)
+ -- SPARK_Pragma (Node32)
-- Body_Needed_For_SAL (Flag40)
-- Elaboration_Entity_Required (Flag174)
-- Default_Expressions_Processed (Flag108)
@@ -5493,6 +5518,7 @@
-- Return_Present (Flag54)
-- Returns_By_Ref (Flag90)
-- Sec_Stack_Needed_For_Return (Flag167)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Uses_Sec_Stack (Flag95)
-- Address_Clause (synth)
-- First_Formal (synth)
@@ -5655,7 +5681,8 @@
-- Package_Instantiation (Node26)
-- Current_Use_Clause (Node27)
-- Finalizer (Node28) (non-generic case only)
- -- SPARK_Mode_Pragmas (Node32)
+ -- SPARK_Aux_Pragma (Node33)
+ -- SPARK_Pragma (Node32)
-- Delay_Subprogram_Descriptors (Flag50)
-- Body_Needed_For_SAL (Flag40)
-- Discard_Names (Flag88)
@@ -5674,6 +5701,8 @@
-- Is_Private_Descendant (Flag53)
-- Is_Visible_Lib_Unit (Flag116)
-- Renamed_In_Spec (Flag231) (non-generic case only)
+ -- SPARK_Aux_Pragma_Inherited (Flag266)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Static_Elaboration_Desired (Flag77) (non-generic case only)
-- Has_Null_Abstract_State (synth)
-- Is_Wrapper_Package (synth) (non-generic case only)
@@ -5688,9 +5717,12 @@
-- Scope_Depth_Value (Uint22)
-- Contract (Node24)
-- Finalizer (Node28) (non-generic case only)
- -- SPARK_Mode_Pragmas (Node32)
+ -- SPARK_Aux_Pragma (Node33)
+ -- SPARK_Pragma (Node32)
-- Delay_Subprogram_Descriptors (Flag50)
-- Has_Anonymous_Master (Flag253)
+ -- SPARK_Aux_Pragma_Inherited (Flag266)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Scope_Depth (synth)
-- E_Private_Type
@@ -5735,7 +5767,7 @@
-- Extra_Formals (Node28)
-- Static_Initialization (Node30) (init_proc only)
-- Thunk_Entity (Node31) (thunk case only)
- -- SPARK_Mode_Pragmas (Node32)
+ -- SPARK_Pragma (Node32)
-- Body_Needed_For_SAL (Flag40)
-- Delay_Cleanups (Flag114)
-- Discard_Names (Flag88)
@@ -5774,6 +5806,7 @@
-- No_Return (Flag113)
-- Requires_Overriding (Flag213) (non-generic case only)
-- Sec_Stack_Needed_For_Return (Flag167)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Address_Clause (synth)
-- First_Formal (synth)
-- First_Formal_With_Extras (synth)
@@ -5907,7 +5940,8 @@
-- Scope_Depth_Value (Uint22)
-- Contract (Node24)
-- Extra_Formals (Node28)
- -- SPARK_Mode_Pragmas (Node32)
+ -- SPARK_Pragma (Node32)
+ -- SPARK_Pragma_Inherited (Flag265)
-- Scope_Depth (synth)
-- E_Subprogram_Type
@@ -6609,7 +6643,10 @@
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 SPARK_Aux_Pragma (Id : E) return N;
+ function SPARK_Aux_Pragma_Inherited (Id : E) return B;
+ function SPARK_Pragma (Id : E) return N;
+ function SPARK_Pragma_Inherited (Id : E) return B;
function Spec_Entity (Id : E) return E;
function Static_Elaboration_Desired (Id : E) return B;
function Static_Initialization (Id : E) return N;
@@ -7232,7 +7269,10 @@
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_SPARK_Aux_Pragma (Id : E; V : N);
+ procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True);
+ procedure Set_SPARK_Pragma (Id : E; V : N);
+ procedure Set_SPARK_Pragma_Inherited (Id : E; V : B := True);
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);
@@ -7994,7 +8034,10 @@
pragma Inline (Size_Depends_On_Discriminant);
pragma Inline (Size_Known_At_Compile_Time);
pragma Inline (Small_Value);
- pragma Inline (SPARK_Mode_Pragmas);
+ pragma Inline (SPARK_Aux_Pragma);
+ pragma Inline (SPARK_Aux_Pragma_Inherited);
+ pragma Inline (SPARK_Pragma);
+ pragma Inline (SPARK_Pragma_Inherited);
pragma Inline (Spec_Entity);
pragma Inline (Static_Elaboration_Desired);
pragma Inline (Static_Initialization);
@@ -8414,7 +8457,10 @@
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_SPARK_Aux_Pragma);
+ pragma Inline (Set_SPARK_Aux_Pragma_Inherited);
+ pragma Inline (Set_SPARK_Pragma);
+ pragma Inline (Set_SPARK_Pragma_Inherited);
pragma Inline (Set_Spec_Entity);
pragma Inline (Set_Static_Elaboration_Desired);
pragma Inline (Set_Static_Initialization);
===================================================================
@@ -166,11 +166,6 @@
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;
@@ -259,11 +254,6 @@
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;
===================================================================
@@ -371,10 +371,6 @@
-- 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. Add note of what this is used for ???
-
-- 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.
@@ -426,7 +422,6 @@
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
@@ -445,7 +440,6 @@
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
@@ -749,10 +743,8 @@
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);
===================================================================
@@ -1,5 +1,5 @@
------------------------------------------------------------------------------
+-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- O P T --
@@ -1272,6 +1272,11 @@
-- GNAT
-- Current SPARK mode setting
+ SPARK_Mode_Pragma : Node_Id := Empty;
+ -- GNAT
+ -- If the current SPARK_Mode (above) was set by a pragma, this records
+ -- the pragma that set this mode.
+
SPARK_Switches_File_Name : String_Ptr := null;
-- GNAT
-- Set to non-null file name by use of the -gnates switch to specify
@@ -1909,8 +1914,13 @@
-- start of analyzing each unit.
SPARK_Mode_Config : SPARK_Mode_Type := None;
+ -- GNAT
-- The setting of SPARK_Mode from configuration pragmas
+ SPARK_Mode_Pragma_Config : Node_Id := Empty;
+ -- If a SPARK_Mode pragma appeared in the configuration pragmas (setting
+ -- SPARK_Mode_Config appropriately), then this points to the N_Pragma node.
+
Use_VADS_Size_Config : Boolean;
-- GNAT
-- This is the value of the configuration switch that controls the use of
@@ -2056,6 +2066,7 @@
Polling_Required : Boolean;
Short_Descriptors : Boolean;
SPARK_Mode : SPARK_Mode_Type;
+ SPARK_Mode_Pragma : Node_Id;
Use_VADS_Size : Boolean;
end record;
===================================================================
@@ -478,6 +478,9 @@
Save_SPARK_Mode : SPARK_Mode_Type;
-- Setting of SPARK_Mode on entry to restore on exit
+ Save_SPARK_Mode_Pragma : Node_Id;
+ -- Setting of SPARK_Mode_Pragma on entry to restore on exit
+
Is_Transient : Boolean;
-- Marks transient scopes (see Exp_Ch7 body for details)
===================================================================
@@ -2162,15 +2162,15 @@
-- it is and the mode is Off, the package body is considered to be in
-- regular Ada and does not require refinement.
- elsif Mode_Is_Off (SPARK_Mode_Pragmas (Body_Id)) then
+ elsif Mode_Is_Off (SPARK_Pragma (Body_Id)) then
return False;
-- The body's SPARK_Mode may be inherited from a similar pragma that
-- appears in the private declarations of the spec. The pragma we are
- -- interested appears as the second entry in SPARK_Mode_Pragmas.
+ -- interested appears as the second entry in SPARK_Pragma.
- elsif Present (SPARK_Mode_Pragmas (Spec_Id))
- and then Mode_Is_Off (Next_Pragma (SPARK_Mode_Pragmas (Spec_Id)))
+ elsif Present (SPARK_Pragma (Spec_Id))
+ and then Mode_Is_Off (Next_Pragma (SPARK_Pragma (Spec_Id)))
then
return False;
===================================================================
@@ -1186,6 +1186,9 @@
end loop;
end;
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
+
Analyze_Declarations (Declarations (N));
Check_Completion;
Analyze (Handled_Statement_Sequence (N));
@@ -2923,6 +2926,8 @@
Reference_Body_Formals (Spec_Id, Body_Id);
end if;
+ Set_Ekind (Body_Id, E_Subprogram_Body);
+
if Nkind (N) = N_Subprogram_Body_Stub then
Set_Corresponding_Spec_Of_Stub (N, Spec_Id);
@@ -2989,9 +2994,17 @@
-- Set SPARK_Mode from spec if spec had a SPARK_Mode pragma
- if Present (SPARK_Mode_Pragmas (Spec_Id)) then
- SPARK_Mode :=
- Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+ if Present (SPARK_Pragma (Spec_Id)) then
+ SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
+ SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
+ Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
+
+ -- Otherwise set from context
+
+ else
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
end if;
-- Make sure that the subprogram is immediately visible. For
@@ -3003,7 +3016,6 @@
Set_Corresponding_Body (Unit_Declaration_Node (Spec_Id), Body_Id);
Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
- Set_Ekind (Body_Id, E_Subprogram_Body);
Set_Scope (Body_Id, Scope (Spec_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
@@ -3550,8 +3562,9 @@
------------------------------------
procedure Analyze_Subprogram_Declaration (N : Node_Id) is
- Scop : constant Entity_Id := Current_Scope;
+ Scop : constant Entity_Id := Current_Scope;
Designator : Entity_Id;
+
Is_Completion : Boolean;
-- Indicates whether a null procedure declaration is a completion
@@ -3585,6 +3598,9 @@
Generate_Definition (Designator);
+ Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Designator, True);
+
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Write_Name (Chars (Designator));
===================================================================
@@ -346,13 +346,29 @@
Push_Scope (Spec_Id);
- -- Set SPARK_Mode from spec if package spec had SPARK_Mode pragma
+ -- Set SPARK_Mode from private part of spec if it has a SPARK pragma.
+ -- Note that in the default case, SPARK_Aux_Pragma will be a copy of
+ -- SPARK_Pragma in the spec, so this properly handles the case where
+ -- there is no explicit SPARK_Pragma mode in the private part.
- if Present (SPARK_Mode_Pragmas (Spec_Id)) then
- SPARK_Mode :=
- Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+ if Present (SPARK_Pragma (Spec_Id)) then
+ SPARK_Mode_Pragma := SPARK_Aux_Pragma (Spec_Id);
+ SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
+
+ -- Otherwise set from context
+
+ else
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
end if;
+ -- Set elaboration code SPARK mode the same for now
+
+ Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
+ Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+
Set_Categorization_From_Pragmas (N);
Install_Visible_Declarations (Spec_Id);
@@ -798,6 +814,13 @@
Set_Etype (Id, Standard_Void_Type);
Set_Contract (Id, Make_Contract (Sloc (Id)));
+ -- Inherit spark mode from context for now
+
+ Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Id, True);
+ Set_SPARK_Aux_Pragma_Inherited (Id, True);
+
-- Analyze aspect specifications immediately, since we need to recognize
-- things like Pure early enough to diagnose violations during analysis.
===================================================================
@@ -7400,6 +7400,7 @@
Check_Policy_List := SST.Save_Check_Policy_List;
Default_Pool := SST.Save_Default_Storage_Pool;
SPARK_Mode := SST.Save_SPARK_Mode;
+ SPARK_Mode_Pragma := SST.Save_SPARK_Mode_Pragma;
if Debug_Flag_W then
Write_Str ("<-- exiting scope: ");
@@ -7474,6 +7475,7 @@
SST.Save_Check_Policy_List := Check_Policy_List;
SST.Save_Default_Storage_Pool := Default_Pool;
SST.Save_SPARK_Mode := SPARK_Mode;
+ SST.Save_SPARK_Mode_Pragma := SPARK_Mode_Pragma;
if Scope_Stack.Last > Scope_Stack.First then
SST.Component_Alignment_Default := Scope_Stack.Table
===================================================================
@@ -18056,116 +18056,58 @@
-- 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.
+ Body_Id : Entity_Id;
+ Context : Node_Id;
+ Mode : Name_Id;
+ Mode_Id : SPARK_Mode_Type;
+ Spec_Id : Entity_Id;
+ Stmt : Node_Id;
- procedure Check_Spark_Mode_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 is the desired new mode.
+ procedure Check_Pragma_Conformance (Old_Pragma : Node_Id);
+ -- Verify the monotonicity of SPARK modes between the new pragma
+ -- N, and the old pragma, Old_Pragma, that was inherited. If
+ -- Old_Pragma is Empty, the call has no effect, otherwise we
+ -- verify that the new mode is less restrictive than the old mode.
+ -- For example, if the old mode is ON, then the new mode can be
+ -- anything. But if the old mode is OFF, then the only allowed
+ -- new mode is also OFF. If there is no error, this routine also
+ -- sets SPARK_Mode_Pragma to N, and SPARK_Mode to Mode_Id.
- 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_Type) return Name_Id;
-- Convert a value of type SPARK_Mode_Type to corresponding name
- ------------------
- -- Chain_Pragma --
- ------------------
-
- procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id) is
- Existing_Prag : constant Node_Id :=
- SPARK_Mode_Pragmas (Context);
-
- begin
- -- Chain existing pragmas to this one, checking consistency
-
- if Present (Existing_Prag) then
- Check_Pragma_Conformance
- (Governing_Mode => Existing_Prag,
- New_Mode => Prag);
-
- Set_Next_Pragma (Prag, Existing_Prag);
- end if;
-
- Set_SPARK_Mode_Pragmas (Context, Prag);
- end Chain_Pragma;
-
- ----------------------------------
- -- Check_Spark_Mode_Conformance --
- ----------------------------------
-
- procedure Check_Spark_Mode_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_Spark_Mode_Conformance;
-
------------------------------
-- Check_Pragma_Conformance --
------------------------------
- procedure Check_Pragma_Conformance
- (Governing_Mode : Node_Id;
- New_Mode : Node_Id)
- is
- Gov_M : constant SPARK_Mode_Type :=
- Get_SPARK_Mode_From_Pragma (Governing_Mode);
- New_M : constant SPARK_Mode_Type :=
- Get_SPARK_Mode_From_Pragma (New_Mode);
-
+ procedure Check_Pragma_Conformance (Old_Pragma : Node_Id) is
begin
- -- The new mode is less restrictive than the established mode
+ if Present (Old_Pragma) then
+ pragma Assert (Nkind (Old_Pragma) = N_Pragma);
- 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);
+ declare
+ Gov_M : constant SPARK_Mode_Type :=
+ Get_SPARK_Mode_From_Pragma (Old_Pragma);
- 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);
+ begin
+ -- New mode less restrictive than the established mode
+
+ if Gov_M < Mode_Id then
+ Error_Msg_Name_1 := Mode;
+ Error_Msg_N ("cannot define 'S'P'A'R'K mode %", Arg1);
+
+ Error_Msg_Name_1 := Get_SPARK_Mode_Name (SPARK_Mode);
+ Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
+ Error_Msg_N
+ ("\mode is less restrictive than mode "
+ & "% defined #", Arg1);
+ raise Pragma_Exit;
+ end if;
+ end;
end if;
+
+ SPARK_Mode_Pragma := N;
+ SPARK_Mode := Mode_Id;
end Check_Pragma_Conformance;
-------------------------
@@ -18190,15 +18132,6 @@
end if;
end Get_SPARK_Mode_Name;
- -- Local variables
-
- Body_Id : Entity_Id;
- Context : Node_Id;
- Mode : Name_Id;
- Mode_Id : SPARK_Mode_Type;
- Spec_Id : Entity_Id;
- Stmt : Node_Id;
-
-- Start of processing for SPARK_Mod
begin
@@ -18217,20 +18150,30 @@
Mode_Id := Get_SPARK_Mode_Type (Mode);
Context := Parent (N);
- SPARK_Mode := Mode_Id;
- -- The pragma appears in a configuration file
+ -- The pragma appears in a configuration pragmas file
if No (Context) then
Check_Valid_Configuration_Pragma;
+ if Present (SPARK_Mode_Pragma) then
+ Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
+ Error_Msg_N ("pragma% duplicates pragma declared#", N);
+ raise Pragma_Exit;
+ end if;
+
+ SPARK_Mode_Pragma := N;
+ 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;
- Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
+ SPARK_Mode_Pragma := N;
+ SPARK_Mode := Mode_Id;
+
-- The pragma applies to a [library unit] subprogram or package
else
@@ -18238,8 +18181,8 @@
if Mode_Id = Auto then
Error_Pragma_Arg
- ("mode `Auto` can only apply to the configuration variant "
- & "of pragma %", Arg1);
+ ("mode `Auto` is only allowed when pragma % appears as "
+ & "a configuration pragma", Arg1);
end if;
-- Verify the placement of the pragma with respect to package
@@ -18255,6 +18198,7 @@
Error_Msg_Name_1 := Pname;
Error_Msg_Sloc := Sloc (Stmt);
Error_Msg_N ("pragma% duplicates pragma declared#", N);
+ raise Pragma_Exit;
end if;
-- Skip internally generated code
@@ -18262,15 +18206,31 @@
elsif not Comes_From_Source (Stmt) then
null;
- -- The pragma applies to a package or subprogram declaration
+ -- The pragma applies to a package declaration
elsif Nkind_In (Stmt, N_Generic_Package_Declaration,
- N_Generic_Subprogram_Declaration,
- N_Package_Declaration,
+ N_Package_Declaration)
+ then
+ Spec_Id := Defining_Unit_Name (Specification (Stmt));
+ Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
+ Set_SPARK_Aux_Pragma (Spec_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+
+ return;
+
+ -- The pragma applies to a subprogram declaration
+
+ elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
N_Subprogram_Declaration)
then
Spec_Id := Defining_Unit_Name (Specification (Stmt));
- Chain_Pragma (Spec_Id, N);
+ Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
return;
-- The pragma does not apply to a legal construct, issue an
@@ -18304,48 +18264,79 @@
end if;
end if;
- -- The pragma is at the top level of a package spec or appears
- -- as an aspect on a subprogram.
+ -- The pragma is at the top level of a package spec
- -- function F ... with SPARK_Mode => ...;
-
-- package P is
-- pragma SPARK_Mode;
- if Nkind_In (Context, N_Function_Specification,
- N_Package_Specification,
- N_Procedure_Specification)
+ -- or
+
+ -- package P is
+ -- ...
+ -- private
+ -- pragma SPARK_Mode;
+
+ if Nkind (Context) = N_Package_Specification then
+ Spec_Id := Defining_Unit_Name (Context);
+
+ -- Pragma applies to private part
+
+ if List_Containing (N) = Private_Declarations (Context) then
+ Check_Pragma_Conformance (SPARK_Aux_Pragma (Spec_Id));
+ Set_SPARK_Aux_Pragma (Spec_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False);
+
+ -- Pragma applies to public part
+
+ else
+ Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
+ Set_SPARK_Aux_Pragma (Spec_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+ end if;
+
+ -- The pragma appears as an aspect on a subprogram.
+
+ -- function F ... with SPARK_Mode => ...;
+
+ elsif Nkind_In (Context, N_Function_Specification,
+ N_Procedure_Specification)
then
Spec_Id := Defining_Unit_Name (Context);
- Chain_Pragma (Spec_Id, N);
+ Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
- -- Pragma is immediately within a package or subprogram body
+ Set_SPARK_Pragma (Spec_Id, N);
+ Set_SPARK_Pragma_Inherited (Spec_Id, False);
- -- function F ... is
- -- pragma SPARK_Mode;
+ -- Pragma is immediately within a package body
-- package body P is
-- pragma SPARK_Mode;
- elsif Nkind_In (Context, N_Package_Body,
- N_Subprogram_Body)
- then
+ elsif Nkind (Context) = N_Package_Body then
Spec_Id := Corresponding_Spec (Context);
+ Body_Id := Defining_Entity (Context);
+ Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
- if Nkind (Context) = N_Subprogram_Body then
- Context := Specification (Context);
- end if;
+ Set_SPARK_Pragma (Body_Id, N);
+ Set_SPARK_Pragma_Inherited (Body_Id, False);
+ Set_SPARK_Aux_Pragma (Body_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
- Body_Id := Defining_Entity (Context);
+ -- Pragma is immediately within a subprogram body
- Chain_Pragma (Body_Id, N);
+ -- function F ... is
+ -- pragma SPARK_Mode;
- -- Verify that the SPARK modes are consistent between
- -- body and spec, if any.
+ elsif Nkind (Context) = N_Subprogram_Body then
+ Spec_Id := Corresponding_Spec (Context);
+ Context := Specification (Context);
+ Body_Id := Defining_Entity (Context);
+ Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
- if Present (Spec_Id) then
- Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
- end if;
+ Set_SPARK_Pragma (Body_Id, N);
+ Set_SPARK_Pragma_Inherited (Body_Id, False);
-- The pragma applies to the statements of a package body
@@ -18359,9 +18350,10 @@
Context := Parent (Context);
Spec_Id := Corresponding_Spec (Context);
Body_Id := Defining_Unit_Name (Context);
+ Check_Pragma_Conformance (SPARK_Aux_Pragma (Body_Id));
- Chain_Pragma (Body_Id, N);
- Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
+ Set_SPARK_Aux_Pragma (Body_Id, N);
+ Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
-- The pragma does not apply to a legal construct, issue error
This patch redoes the data structures for pragma SPARK_Mode so that the tree captures full information on the SPARK_Mode setting in all cases, so that it can easily be accessed by gnat2why. It also fully implements the error checking on "monotonicity" of SPARK_Mode settings, and also properly checks for duplicate pragmas in a configuration pragma file. The following program: 1. package body PSMode is 2. pragma SPARK_Mode (On); 3. procedure q is begin null; end; 4. begin 5. pragma SPARK_Mode (Off); 6. Z := 2; 7. end PSMode; 1. package PSMode is 2. pragma SPARK_Mode (On); 3. X : Integer := 12; 4. Y : Integer := 2 ** X; 5. procedure q; 6. private 7. pragma SPARK_Mode (Off); 8. Z : Integer; 9. end PSMode; compiled with a gnat.adc file that looks like: 1. pragma SPARK_Mode (On); 2. pragma SPARK_Mode (On); gets the following errors compiled with -gnatj60 psmode.adb:2:23: cannot define SPARK mode "on", mode is less restrictive than mode "off" defined at psmode.ads:7 gnat.adc:2:01: pragma "Spark_Mode" duplicates pragma declared at line 1 Tested on x86_64-pc-linux-gnu, committed on trunk 2014-01-21 Robert Dewar <dewar@adacore.com> * atree.ads, atree.adb: Add Node33 and Set_Node33. * einfo.ads, einfo.adb (SPARK_Pragma): New field (SPARK_Aux_Pragma): New field (SPARK_Pragma_Inherited): New flag (SPARK_Aux_Pragma_Inherited): New flag (SPARK_Mode_Pragmas): Removed. * lib.ads, lib.adb: Remove SPARK_Mode_Pragma, no longer used. * opt.ads (SPARK_Mode_Pragma): New global variable. * sem.ads: Add Save_SPARK_Mode_Pragma field to Scope_Stack_Entry. * sem_ch3.adb: Use new SPARK_Mode data structures. * sem_ch6.adb: Set SPARK_Mode fields in subprogram specs and bodies. * sem_ch7.adb: Set SPARK_Mode fields in package spec and body entities. * sem_ch8.adb (Push_Scope): Save SPARK_Mode_Pragma. (Pop_Scope): Restore SPARK_Mode_Pragma. * sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Rewrite for new data structures.