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 <de...@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.
Index: atree.adb =================================================================== --- atree.adb (revision 206872) +++ atree.adb (working copy) @@ -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); Index: atree.ads =================================================================== --- atree.ads (revision 206872) +++ atree.ads (working copy) @@ -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); Index: einfo.adb =================================================================== --- einfo.adb (revision 206832) +++ einfo.adb (working copy) @@ -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; Index: einfo.ads =================================================================== --- einfo.ads (revision 206832) +++ einfo.ads (working copy) @@ -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_Mode_Pragmas (Node32) +-- 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 a list of SPARK_Mode pragmas that --- apply to the related construct. Add note of what this is used for ??? +-- 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); Index: lib.adb =================================================================== --- lib.adb (revision 206804) +++ lib.adb (working copy) @@ -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; Index: lib.ads =================================================================== --- lib.ads (revision 206804) +++ lib.ads (working copy) @@ -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); Index: opt.ads =================================================================== --- opt.ads (revision 206871) +++ opt.ads (working copy) @@ -1,5 +1,5 @@ ------------------------------------------------------------------------------ --- SPARK -- +-- -- -- 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; Index: sem.ads =================================================================== --- sem.ads (revision 206844) +++ sem.ads (working copy) @@ -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) Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 206844) +++ sem_ch3.adb (working copy) @@ -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; Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 206844) +++ sem_ch6.adb (working copy) @@ -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)); Index: sem_ch7.adb =================================================================== --- sem_ch7.adb (revision 206844) +++ sem_ch7.adb (working copy) @@ -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. Index: sem_ch8.adb =================================================================== --- sem_ch8.adb (revision 206870) +++ sem_ch8.adb (working copy) @@ -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 Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 206878) +++ sem_prag.adb (working copy) @@ -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