yggdrasil/gcc
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

[multiple changes]

Browse Source 
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.

From-SVN: r206879
This commit is contained in:
Arnaud Charlet 2014-01-21 13:02:54 +01:00
parent 376e7d14c0
commit 579847c272
22 changed files with 480 additions and 259 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
gcc/ada/ChangeLog
View File

@ -1,3 +1,54 @@
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.

12
gcc/ada/atree.adb
View File

@ -2595,6 +2595,12 @@ package body Atree is
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 @@ package body Atree is
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);

6
gcc/ada/atree.ads
View File

@ -1209,6 +1209,9 @@ package Atree is
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 @@ package Atree is
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);

23
gcc/ada/back_end.adb
View File

@ -183,7 +183,6 @@ package body Back_End is
-----------------------------
procedure Scan_Compiler_Arguments is
Next_Arg : Positive;
-- Next argument to be scanned
@ -247,7 +246,6 @@ package body Back_End is
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;
@ -255,7 +253,7 @@ package body Back_End is
-- 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
@ -271,7 +269,7 @@ package body Back_End is
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;
@ -289,20 +287,9 @@ package body Back_End is
-- 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;
@ -320,7 +307,9 @@ package body Back_End is
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

94
gcc/ada/einfo.adb
View File

@ -248,9 +248,9 @@ package body Einfo is
-- Thunk_Entity Node31
-- SPARK_Mode_Pragmas Node32
-- SPARK_Pragma Node32
-- (unused) Node33
-- SPARK_Aux_Pragma Node33
-- (unused) Node34
@ -554,9 +554,9 @@ package body Einfo is
-- 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,7 +2835,25 @@ package body Einfo is
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
@ -2848,7 +2866,22 @@ package body Einfo is
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
@ -5527,7 +5560,27 @@ package body Einfo is
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
@ -5541,7 +5594,23 @@ package body Einfo is
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
@ -8227,6 +8296,8 @@ package body Einfo is
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 @@ package body Einfo is
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 @@ package body Einfo is
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;

70
gcc/ada/einfo.ads
View File

@ -3801,10 +3801,35 @@ package Einfo is
-- 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
@ -5455,7 +5480,7 @@ package Einfo is
-- 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 @@ package Einfo is
-- 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 Einfo is
-- 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 @@ package Einfo is
-- 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 @@ package Einfo is
-- 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 @@ package Einfo is
-- 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 @@ package Einfo is
-- 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 @@ package Einfo is
-- 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 @@ package Einfo is
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 @@ package Einfo is
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 @@ package Einfo is
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 @@ package Einfo is
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);

23
gcc/ada/exp_aggr.adb
View File

@ -1164,8 +1164,8 @@ package body Exp_Aggr is
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
@ -1205,14 +1205,15 @@ package body Exp_Aggr is
-- 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);
@ -1231,9 +1232,9 @@ package body Exp_Aggr is
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)),

27
gcc/ada/gnat1drv.adb
View File

@ -858,34 +858,9 @@ begin
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);

3
gcc/ada/gnat_rm.texi
View File

@ -6287,7 +6287,8 @@ an implicit argument of On is assumed.
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:

11
gcc/ada/gnat_ugn.texi
View File

@ -15392,6 +15392,17 @@ attribute:
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

10
gcc/ada/lib.adb
View File

@ -166,11 +166,6 @@ package body Lib is
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 @@ package body Lib is
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;

8
gcc/ada/lib.ads
View File

@ -371,10 +371,6 @@ package Lib is
-- 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 @@ package Lib is
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 @@ package Lib is
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 @@ private
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);

13
gcc/ada/opt.ads
View File

@ -1,5 +1,5 @@
------------------------------------------------------------------------------
-- SPARK --
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- O P T --
@ -1272,6 +1272,11 @@ package Opt is
-- 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 @@ package Opt is
-- 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 @@ private
Polling_Required : Boolean;
Short_Descriptors : Boolean;
SPARK_Mode : SPARK_Mode_Type;
SPARK_Mode_Pragma : Node_Id;
Use_VADS_Size : Boolean;
end record;

22
gcc/ada/prj-part.adb
View File

@ -1325,11 +1325,20 @@ package body Prj.Part is
"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
@ -1372,6 +1381,16 @@ package body Prj.Part is
"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;
@ -1933,6 +1952,7 @@ package body Prj.Part is
Node => Project,
Canonical_Path => Canonical_Path_Name,
Extended => Extended,
From_Extended => From_Extended /= None,
Proj_Qualifier => Project_Qualifier_Of (Project, In_Tree)));
end if;

15
gcc/ada/prj-tree.adb
View File

@ -1321,8 +1321,7 @@ package body Prj.Tree is
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;
@ -1332,18 +1331,17 @@ package body Prj.Tree is
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;
@ -2925,6 +2923,7 @@ package body Prj.Tree is
Canonical_Path => No_Path,
Node => Project,
Extended => False,
From_Extended => False,
Proj_Qualifier => Qualifier));
end if;

5
gcc/ada/prj-tree.ads
View File

@ -1476,6 +1476,10 @@ package Prj.Tree is
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;
@ -1486,6 +1490,7 @@ package Prj.Tree is
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

3
gcc/ada/sem.ads
View File

@ -478,6 +478,9 @@ package Sem is
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)

8
gcc/ada/sem_ch3.adb
View File

@ -2162,15 +2162,15 @@ package body Sem_Ch3 is
-- 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;

26
gcc/ada/sem_ch6.adb
View File

@ -1186,6 +1186,9 @@ package body Sem_Ch6 is
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 @@ package body Sem_Ch6 is
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 @@ package body Sem_Ch6 is
-- 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 @@ package body Sem_Ch6 is
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 @@ package body Sem_Ch6 is
------------------------------------
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 @@ package body Sem_Ch6 is
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));

31
gcc/ada/sem_ch7.adb
View File

@ -346,13 +346,29 @@ package body Sem_Ch7 is
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 @@ package body Sem_Ch7 is
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.

2
gcc/ada/sem_ch8.adb
View File

@ -7400,6 +7400,7 @@ package body Sem_Ch8 is
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 @@ package body Sem_Ch8 is
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

276
gcc/ada/sem_prag.adb
View File

@ -18056,116 +18056,58 @@ package body Sem_Prag is
-- 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
(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.
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;
-------------------------
@ -18190,15 +18132,6 @@ package body Sem_Prag is
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,19 +18150,29 @@ package body Sem_Prag is
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
@ -18238,8 +18181,8 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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 @@ package body Sem_Prag is
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);
if Nkind (Context) = N_Subprogram_Body then
Context := Specification (Context);
end if;
Body_Id := Defining_Entity (Context);
Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
Chain_Pragma (Body_Id, N);
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);
-- Verify that the SPARK modes are consistent between
-- body and spec, if any.
-- Pragma is immediately within a subprogram body
if Present (Spec_Id) then
Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
end if;
-- function F ... is
-- pragma SPARK_Mode;
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));
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 @@ package body Sem_Prag is
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