+2014-01-21 Robert Dewar <dewar@adacore.com>
+
+ * exp_aggr.adb: Minor reformatting.
+
+2014-01-21 Johannes Kanig <kanig@adacore.com>
+
+ * gnat1drv.adb (Gnat1drv) remove obsolete reference to -gnatd.H.
+
+2014-01-21 Bob Duff <duff@adacore.com>
+
+ * gnat_ugn.texi: Document the "checks" attribute in gnat2xml.
+
+2014-01-21 Steve Baird <baird@adacore.com>
+
+ * gnat_rm.texi: Improve description of SPARK_Mode pragma.
+
+2014-01-21 Vincent Celier <celier@adacore.com>
+
+ * prj-part.adb (Parse_Single_Project): Accept to extend a project
+ if it has only be imported by an project being extended. When a
+ project that has only been imported by a project being extended
+ is imported by another project that is not being extended,
+ reset the previous indication, so that it will be an error if
+ this project is extended later.
+ * prj-tree.adb (Create_Project): Include component From_Extended
+ in table Projects_HT
+ * prj-tree.ads (Project_Name_And_Node): New Boolean component
+ From_Extended
+
+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.
+
+2014-01-21 Arnaud Charlet <charlet@adacore.com>
+
+ * back_end.adb: Undo previous change, not needed. Minor reformatting.
+
2014-01-21 Thomas Quinot <quinot@adacore.com>
* exp_ch5.adb: Fix comment.
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);
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);
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);
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);
-----------------------------
procedure Scan_Compiler_Arguments is
-
Next_Arg : Positive;
-- Next argument to be scanned
elsif Switch_Chars (First .. Last) = "fdump-scos" then
Opt.Generate_SCO := True;
Opt.Generate_SCO_Instance_Table := True;
-
end if;
end if;
end Scan_Back_End_Switches;
-- Local variables
Arg_Count : constant Natural := Natural (save_argc - 1);
- Args : Argument_List (1 .. Arg_Count);
+ Args : Argument_List (1 .. Arg_Count);
-- Start of processing for Scan_Compiler_Arguments
Argv_Ptr : constant Big_String_Ptr := save_argv (Arg);
Argv_Len : constant Nat := Len_Arg (Arg);
Argv : constant String :=
- Argv_Ptr (1 .. Natural (Argv_Len));
+ Argv_Ptr (1 .. Natural (Argv_Len));
begin
Args (Positive (Arg)) := new String'(Argv);
end;
-- flag (that is we have seen a -gnatO), then the next argument
-- is the name of the output object file.
- if Output_File_Name_Present
- and then not Output_File_Name_Seen
- then
+ if Output_File_Name_Present and then not Output_File_Name_Seen then
if Is_Switch (Argv) then
Fail ("Object file name missing after -gnatO");
-
- -- In GNATprove_Mode, such an object file is never written, and
- -- the call to Set_Output_Object_File_Name may fail (e.g. when
- -- the object file name does not have the expected suffix). So
- -- we skip that call when GNATprove_Mode is set.
-
- elsif GNATprove_Mode then
- Output_File_Name_Seen := True;
-
else
Set_Output_Object_File_Name (Argv);
Output_File_Name_Seen := True;
Search_Directory_Present := False;
end if;
- elsif not Is_Switch (Argv) then -- must be a file name
+ -- If not a switch, must be a file name
+
+ elsif not Is_Switch (Argv) then
Add_File (Argv);
-- We must recognize -nostdinc to suppress visibility on the
-- Thunk_Entity Node31
- -- SPARK_Mode_Pragmas Node32
+ -- SPARK_Pragma Node32
- -- (unused) Node33
+ -- SPARK_Aux_Pragma Node33
-- (unused) Node34
-- 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
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_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
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_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
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));
E_Package_Body |
E_Procedure |
E_Subprogram_Body =>
- Write_Str ("SPARK_Mode_Pragmas");
+ Write_Str ("SPARK_Pragma");
when others =>
Write_Str ("Field32??");
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;
-- 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
-- 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)
-- 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)
-- 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)
-- 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)
-- 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
-- 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)
-- 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)
-- 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
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;
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);
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);
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);
elsif Is_Access_Type (Ctype) then
Append_To (L,
Make_Assignment_Statement (Loc,
- Name => Indexed_Comp,
- Expression => Make_Null (Loc)));
+ Name => Indexed_Comp,
+ Expression => Make_Null (Loc)));
end if;
if Needs_Finalization (Ctype) then
-- assignment in a block.
if Present (Comp_Type)
- and then Needs_Finalization (Comp_Type)
- and then Is_Array_Type (Comp_Type)
- and then Present (Expr)
+ and then Needs_Finalization (Comp_Type)
+ and then Is_Array_Type (Comp_Type)
+ and then Present (Expr)
then
- A := Make_Block_Statement (Loc,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (A)));
+ A :=
+ Make_Block_Statement (Loc,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (A)));
end if;
Append_To (L, A);
begin
A :=
Make_OK_Assignment_Statement (Loc,
- Name =>
+ Name =>
Make_Selected_Component (Loc,
- Prefix => New_Copy_Tree (Indexed_Comp),
+ Prefix => New_Copy_Tree (Indexed_Comp),
Selector_Name =>
New_Reference_To
(First_Tag_Component (Full_Typ), Loc)),
Original_Operating_Mode := Operating_Mode;
Frontend;
- -- Exit with errors if the main source could not be parsed. Also, when
- -- -gnatd.H is present, the source file is not set.
+ -- Exit with errors if the main source could not be parsed.
if Sinput.Main_Source_File = No_Source_File then
-
- -- Handle -gnatd.H debug mode
-
- if Debug_Flag_Dot_HH then
-
- -- For -gnatd.H, lock all the tables to keep the convention that
- -- the backend needs to unlock the tables it wants to touch.
-
- Atree.Lock;
- Elists.Lock;
- Fname.UF.Lock;
- Inline.Lock;
- Lib.Lock;
- Nlists.Lock;
- Sem.Lock;
- Sinput.Lock;
- Namet.Lock;
- Stringt.Lock;
-
- -- And all we need to do is to call the back end
-
- Back_End.Call_Back_End (Back_End.Generate_Object);
- end if;
-
Errout.Finalize (Last_Call => True);
Errout.Output_Messages;
Exit_Program (E_Errors);
A SPARK_Mode pragma may be used as a configuration pragma and then has the
semantics described below. A SPARK_Mode pragma which is not used as a
-configuration pragma shall not have an argument of Auto.
+configuration pragma (or an equivalent SPARK_Mode aspect_specification)
+shall not have an argument of Auto.
A SPARK_Mode pragma can be used as a local pragma only
in the following contexts:
mode indicates that the parameter is of mode 'in', 'in out', or 'out'.
@end itemize
+@noindent
+All elements other than Not_An_Element have this attribute:
+
+@itemize @bullet
+@item
+checks is a comma-separated list of run-time checks that are needed
+for that element. The possible checks are: do_accessibility_check,
+do_discriminant_check,do_division_check,do_length_check,
+do_overflow_check,do_range_check,do_storage_check,do_tag_check.
+@end itemize
+
@noindent
The "kind" part of the "def" and "ref" attributes is taken from the ASIS
enumeration type Flat_Declaration_Kinds, declared in
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;
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;
-- 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.
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_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
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);
------------------------------------------------------------------------------
--- SPARK --
+-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- O P T --
-- 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
-- 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
Polling_Required : Boolean;
Short_Descriptors : Boolean;
SPARK_Mode : SPARK_Mode_Type;
+ SPARK_Mode_Pragma : Node_Id;
Use_VADS_Size : Boolean;
end record;
"cannot extend the same project file several times",
Token_Ptr);
end if;
- else
+ elsif not A_Project_Name_And_Node.From_Extended then
Error_Msg
(Env.Flags,
"cannot extend an already imported project file",
Token_Ptr);
+
+ else
+ -- Register this project as being extended
+
+ A_Project_Name_And_Node.Extended := True;
+ Tree_Private_Part.Projects_Htable.Set
+ (In_Tree.Projects_HT,
+ A_Project_Name_And_Node.Name,
+ A_Project_Name_And_Node);
end if;
elsif A_Project_Name_And_Node.Extended then
"cannot import an already extended project file",
Token_Ptr);
end if;
+
+ elsif A_Project_Name_And_Node.From_Extended then
+ -- This project is now imported from a non extending project.
+ -- Indicate this in has table Projects.HT.
+
+ A_Project_Name_And_Node.From_Extended := False;
+ Tree_Private_Part.Projects_Htable.Set
+ (In_Tree.Projects_HT,
+ A_Project_Name_And_Node.Name,
+ A_Project_Name_And_Node);
end if;
Project := A_Project_Name_And_Node.Node;
Node => Project,
Canonical_Path => Canonical_Path_Name,
Extended => Extended,
+ From_Extended => From_Extended /= None,
Proj_Qualifier => Project_Qualifier_Of (Project, In_Tree)));
end if;
begin
pragma Assert
(Present (Node)
- and then
- In_Tree.Project_Nodes.Table (Node).Kind = N_Term);
+ and then In_Tree.Project_Nodes.Table (Node).Kind = N_Term);
return In_Tree.Project_Nodes.Table (Node).Field2;
end Next_Term;
function Next_Variable
(Node : Project_Node_Id;
- In_Tree : Project_Node_Tree_Ref)
- return Project_Node_Id
+ In_Tree : Project_Node_Tree_Ref) return Project_Node_Id
is
begin
pragma Assert
(Present (Node)
and then
- (In_Tree.Project_Nodes.Table (Node).Kind =
- N_Typed_Variable_Declaration
+ (In_Tree.Project_Nodes.Table (Node).Kind =
+ N_Typed_Variable_Declaration
or else
- In_Tree.Project_Nodes.Table (Node).Kind =
- N_Variable_Declaration));
+ In_Tree.Project_Nodes.Table (Node).Kind =
+ N_Variable_Declaration));
return In_Tree.Project_Nodes.Table (Node).Field3;
end Next_Variable;
Canonical_Path => No_Path,
Node => Project,
Extended => False,
+ From_Extended => False,
Proj_Qualifier => Qualifier));
end if;
Extended : Boolean;
-- True when the project is being extended by another project
+ From_Extended : Boolean;
+ -- True when the project is only imported by projects that are
+ -- extended.
+
Proj_Qualifier : Project_Qualifier;
-- The project qualifier of the project, if any
end record;
Node => Empty_Node,
Canonical_Path => No_Path,
Extended => True,
+ From_Extended => False,
Proj_Qualifier => Unspecified);
package Projects_Htable is new GNAT.Dynamic_HTables.Simple_HTable
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)
-- 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;
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));
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);
-- 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
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));
------------------------------------
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
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));
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);
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.
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: ");
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
-- 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_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
- (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.
+ Body_Id : Entity_Id;
+ Context : Node_Id;
+ Mode : Name_Id;
+ Mode_Id : SPARK_Mode_Type;
+ Spec_Id : Entity_Id;
+ Stmt : Node_Id;
+
+ 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.
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;
-------------------------
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
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
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
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
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
end if;
end if;
- -- The pragma is at the top level of a package spec or appears
- -- as an aspect on a subprogram.
-
- -- function F ... with SPARK_Mode => ...;
+ -- The pragma is at the top level of a package spec
-- 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
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
projects / gcc.git / commitdiff