[multiple changes]
2016-06-22 Hristian Kirtchev <kirtchev@adacore.com> * lib-xref-spark_specific.adb, checks.adb, sem_ch13.adb: Minor reformatting. * exp_ch7.adb: Minor typo fix. * lib.ads (Get_Top_Level_Code_Unit): Add comment. 2016-06-22 Bob Duff <duff@adacore.com> * s-tassta.adb (Task_Wrapper): Fix handling of Fall_Back_Handler wrt independent tasks. 2016-06-22 Ed Schonberg <schonberg@adacore.com> * sem_dim.adb (Analyze_Dimension): Propagate dimension for explicit_dereference nodes when they do not come from source, to handle correctly dimensional analysis on iterators over containers whose elements have declared dimensions. From-SVN: r237691
This commit is contained in:
parent
7ffbef9966
commit
80007176a5
|
@ -1,3 +1,22 @@
|
|||
2016-06-22 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* lib-xref-spark_specific.adb, checks.adb, sem_ch13.adb: Minor
|
||||
reformatting.
|
||||
* exp_ch7.adb: Minor typo fix.
|
||||
* lib.ads (Get_Top_Level_Code_Unit): Add comment.
|
||||
|
||||
2016-06-22 Bob Duff <duff@adacore.com>
|
||||
|
||||
* s-tassta.adb (Task_Wrapper): Fix handling of Fall_Back_Handler
|
||||
wrt independent tasks.
|
||||
|
||||
2016-06-22 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_dim.adb (Analyze_Dimension): Propagate dimension for
|
||||
explicit_dereference nodes when they do not come from source,
|
||||
to handle correctly dimensional analysis on iterators over
|
||||
containers whose elements have declared dimensions.
|
||||
|
||||
2016-06-22 Arnaud Charlet <charlet@adacore.com>
|
||||
|
||||
* spark_xrefs.ads (Scope_Num): type refined to positive integers.
|
||||
|
|
|
@ -635,17 +635,15 @@ package body Checks is
|
|||
procedure Apply_Address_Clause_Check (E : Entity_Id; N : Node_Id) is
|
||||
pragma Assert (Nkind (N) = N_Freeze_Entity);
|
||||
|
||||
AC : constant Node_Id := Address_Clause (E);
|
||||
Loc : constant Source_Ptr := Sloc (AC);
|
||||
Typ : constant Entity_Id := Etype (E);
|
||||
AC : constant Node_Id := Address_Clause (E);
|
||||
Loc : constant Source_Ptr := Sloc (AC);
|
||||
Typ : constant Entity_Id := Etype (E);
|
||||
|
||||
Expr : Node_Id;
|
||||
-- Address expression (not necessarily the same as Aexp, for example
|
||||
-- when Aexp is a reference to a constant, in which case Expr gets
|
||||
-- reset to reference the value expression of the constant).
|
||||
|
||||
-- Start of processing for Apply_Address_Clause_Check
|
||||
|
||||
begin
|
||||
-- See if alignment check needed. Note that we never need a check if the
|
||||
-- maximum alignment is one, since the check will always succeed.
|
||||
|
@ -679,8 +677,8 @@ package body Checks is
|
|||
AL : Uint := Alignment (Typ);
|
||||
|
||||
begin
|
||||
-- The object alignment might be more restrictive than the
|
||||
-- type alignment.
|
||||
-- The object alignment might be more restrictive than the type
|
||||
-- alignment.
|
||||
|
||||
if Known_Alignment (E) then
|
||||
AL := Alignment (E);
|
||||
|
@ -718,9 +716,9 @@ package body Checks is
|
|||
-- Generate a check to raise PE if alignment may be inappropriate
|
||||
|
||||
else
|
||||
-- If the original expression is a non-static constant, use the
|
||||
-- name of the constant itself rather than duplicating its
|
||||
-- defining expression, which was extracted above.
|
||||
-- If the original expression is a non-static constant, use the name
|
||||
-- of the constant itself rather than duplicating its initialization
|
||||
-- expression, which was extracted above.
|
||||
|
||||
-- Note: Expr is empty if the address-clause is applied to in-mode
|
||||
-- actuals (allowed by 13.1(22)).
|
||||
|
@ -729,8 +727,8 @@ package body Checks is
|
|||
or else
|
||||
(Is_Entity_Name (Expression (AC))
|
||||
and then Ekind (Entity (Expression (AC))) = E_Constant
|
||||
and then Nkind (Parent (Entity (Expression (AC))))
|
||||
= N_Object_Declaration)
|
||||
and then Nkind (Parent (Entity (Expression (AC)))) =
|
||||
N_Object_Declaration)
|
||||
then
|
||||
Expr := New_Copy_Tree (Expression (AC));
|
||||
else
|
||||
|
@ -745,9 +743,9 @@ package body Checks is
|
|||
Make_Raise_Program_Error (Loc,
|
||||
Condition =>
|
||||
Make_Op_Ne (Loc,
|
||||
Left_Opnd =>
|
||||
Left_Opnd =>
|
||||
Make_Op_Mod (Loc,
|
||||
Left_Opnd =>
|
||||
Left_Opnd =>
|
||||
Unchecked_Convert_To
|
||||
(RTE (RE_Integer_Address), Expr),
|
||||
Right_Opnd =>
|
||||
|
@ -755,7 +753,7 @@ package body Checks is
|
|||
Prefix => New_Occurrence_Of (E, Loc),
|
||||
Attribute_Name => Name_Alignment)),
|
||||
Right_Opnd => Make_Integer_Literal (Loc, Uint_0)),
|
||||
Reason => PE_Misaligned_Address_Value));
|
||||
Reason => PE_Misaligned_Address_Value));
|
||||
|
||||
Warning_Msg := No_Error_Msg;
|
||||
Analyze (First (Actions (N)), Suppress => All_Checks);
|
||||
|
@ -765,6 +763,7 @@ package body Checks is
|
|||
-- No_Exception_Propagation).
|
||||
|
||||
if Warning_Msg /= No_Error_Msg then
|
||||
|
||||
-- If the expression has a known at compile time value, then
|
||||
-- once we know the alignment of the type, we can check if the
|
||||
-- exception will be raised or not, and if not, we don't need
|
||||
|
@ -773,12 +772,13 @@ package body Checks is
|
|||
if Compile_Time_Known_Value (Expr) then
|
||||
Alignment_Warnings.Append
|
||||
((E => E, A => Expr_Value (Expr), W => Warning_Msg));
|
||||
else
|
||||
-- Add explanation of the warning generated by the check
|
||||
|
||||
-- Add explanation of the warning generated by the check
|
||||
|
||||
else
|
||||
Error_Msg_N
|
||||
("\address value may be incompatible with alignment "
|
||||
& "of object?X?", AC);
|
||||
("\address value may be incompatible with alignment of "
|
||||
& "object?X?", AC);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
@ -786,6 +786,7 @@ package body Checks is
|
|||
end if;
|
||||
|
||||
exception
|
||||
|
||||
-- If we have some missing run time component in configurable run time
|
||||
-- mode then just skip the check (it is not required in any case).
|
||||
|
||||
|
|
|
@ -4616,7 +4616,7 @@ package body Exp_Ch7 is
|
|||
Set_Ghost_Mode_From_Entity (Work_Typ);
|
||||
|
||||
-- Emulate the environment of the invariant procedure by installing
|
||||
-- its scope and formal parameters. Note that this is not need, but
|
||||
-- its scope and formal parameters. Note that this is not needed, but
|
||||
-- having the scope of the invariant procedure installed helps with
|
||||
-- the detection of invariant-related errors.
|
||||
|
||||
|
|
|
@ -54,9 +54,9 @@ package body SPARK_Specific is
|
|||
-- True for each reference type used in SPARK
|
||||
|
||||
SPARK_References : constant array (Character) of Boolean :=
|
||||
('m' => True,
|
||||
'r' => True,
|
||||
's' => True,
|
||||
('m' => True,
|
||||
'r' => True,
|
||||
's' => True,
|
||||
others => False);
|
||||
|
||||
type Entity_Hashed_Range is range 0 .. 255;
|
||||
|
@ -102,9 +102,9 @@ package body SPARK_Specific is
|
|||
generic
|
||||
with procedure Process (N : Node_Id) is <>;
|
||||
procedure Traverse_Compilation_Unit (CU : Node_Id; Inside_Stubs : Boolean);
|
||||
-- Call Process on all declarations in compilation unit CU. If
|
||||
-- Inside_Stubs is True, then the body of stubs is also traversed.
|
||||
-- Generic declarations are ignored.
|
||||
-- Call Process on all declarations within compilation unit CU. If flag
|
||||
-- Inside_Stubs is True, then the body of stubs is also traversed. Generic
|
||||
-- declarations are ignored.
|
||||
|
||||
--------------------
|
||||
-- Add_SPARK_File --
|
||||
|
@ -114,9 +114,6 @@ package body SPARK_Specific is
|
|||
File : constant Source_File_Index := Source_Index (Uspec);
|
||||
From : constant Scope_Index := SPARK_Scope_Table.Last + 1;
|
||||
|
||||
File_Name : String_Ptr;
|
||||
Unit_File_Name : String_Ptr;
|
||||
|
||||
Scope_Id : Pos := 1;
|
||||
|
||||
procedure Add_SPARK_Scope (N : Node_Id);
|
||||
|
@ -147,49 +144,46 @@ package body SPARK_Specific is
|
|||
end if;
|
||||
|
||||
case Ekind (E) is
|
||||
when E_Entry
|
||||
| E_Entry_Family
|
||||
| E_Generic_Function
|
||||
| E_Generic_Package
|
||||
| E_Generic_Procedure
|
||||
| E_Package
|
||||
| E_Protected_Type
|
||||
| E_Task_Type
|
||||
=>
|
||||
Typ := Xref_Entity_Letters (Ekind (E));
|
||||
|
||||
when E_Function
|
||||
| E_Procedure
|
||||
=>
|
||||
-- In SPARK we need to distinguish protected functions and
|
||||
-- procedures from ordinary subprograms, but there are no special
|
||||
-- Xref letters for them. Since this distiction is only needed to
|
||||
-- detect protected calls, we pretend that such calls are entry
|
||||
-- calls.
|
||||
|
||||
if Ekind (Scope (E)) = E_Protected_Type then
|
||||
Typ := Xref_Entity_Letters (E_Entry);
|
||||
else
|
||||
when E_Entry |
|
||||
E_Entry_Family |
|
||||
E_Generic_Function |
|
||||
E_Generic_Package |
|
||||
E_Generic_Procedure |
|
||||
E_Package |
|
||||
E_Protected_Type |
|
||||
E_Task_Type =>
|
||||
Typ := Xref_Entity_Letters (Ekind (E));
|
||||
end if;
|
||||
|
||||
when E_Package_Body
|
||||
| E_Protected_Body
|
||||
| E_Subprogram_Body
|
||||
| E_Task_Body
|
||||
=>
|
||||
Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));
|
||||
when E_Function | E_Procedure =>
|
||||
|
||||
when E_Void =>
|
||||
-- In SPARK we need to distinguish protected functions and
|
||||
-- procedures from ordinary subprograms, but there are no
|
||||
-- special Xref letters for them. Since this distiction is
|
||||
-- only needed to detect protected calls, we pretend that
|
||||
-- such calls are entry calls.
|
||||
|
||||
-- Compilation of prj-attr.adb with -gnatn creates a node with
|
||||
-- entity E_Void for the package defined at a-charac.ads16:13.
|
||||
-- ??? TBD
|
||||
if Ekind (Scope (E)) = E_Protected_Type then
|
||||
Typ := Xref_Entity_Letters (E_Entry);
|
||||
else
|
||||
Typ := Xref_Entity_Letters (Ekind (E));
|
||||
end if;
|
||||
|
||||
return;
|
||||
when E_Package_Body |
|
||||
E_Protected_Body |
|
||||
E_Subprogram_Body |
|
||||
E_Task_Body =>
|
||||
Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));
|
||||
|
||||
when others =>
|
||||
raise Program_Error;
|
||||
when E_Void =>
|
||||
|
||||
-- Compilation of prj-attr.adb with -gnatn creates a node with
|
||||
-- entity E_Void for the package defined at a-charac.ads16:13.
|
||||
-- ??? TBD
|
||||
|
||||
return;
|
||||
|
||||
when others =>
|
||||
raise Program_Error;
|
||||
end case;
|
||||
|
||||
-- File_Num and Scope_Num are filled later. From_Xref and To_Xref
|
||||
|
@ -218,24 +212,32 @@ package body SPARK_Specific is
|
|||
|
||||
procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
|
||||
begin
|
||||
if Nkind_In (N, N_Entry_Body, -- entries
|
||||
N_Entry_Declaration)
|
||||
or else
|
||||
Nkind_In (N, N_Package_Body, -- packages
|
||||
N_Package_Body_Stub,
|
||||
N_Package_Declaration)
|
||||
or else
|
||||
Nkind_In (N, N_Protected_Body, -- protected objects
|
||||
N_Protected_Body_Stub,
|
||||
N_Protected_Type_Declaration)
|
||||
or else
|
||||
Nkind_In (N, N_Subprogram_Body, -- subprograms
|
||||
N_Subprogram_Body_Stub,
|
||||
N_Subprogram_Declaration)
|
||||
or else
|
||||
Nkind_In (N, N_Task_Body, -- tasks
|
||||
N_Task_Body_Stub,
|
||||
N_Task_Type_Declaration)
|
||||
-- Entries
|
||||
|
||||
if Nkind_In (N, N_Entry_Body, N_Entry_Declaration)
|
||||
|
||||
-- Packages
|
||||
|
||||
or else Nkind_In (N, N_Package_Body,
|
||||
N_Package_Body_Stub,
|
||||
N_Package_Declaration)
|
||||
-- Protected units
|
||||
|
||||
or else Nkind_In (N, N_Protected_Body,
|
||||
N_Protected_Body_Stub,
|
||||
N_Protected_Type_Declaration)
|
||||
|
||||
-- Subprograms
|
||||
|
||||
or else Nkind_In (N, N_Subprogram_Body,
|
||||
N_Subprogram_Body_Stub,
|
||||
N_Subprogram_Declaration)
|
||||
|
||||
-- Task units
|
||||
|
||||
or else Nkind_In (N, N_Task_Body,
|
||||
N_Task_Body_Stub,
|
||||
N_Task_Type_Declaration)
|
||||
then
|
||||
Add_SPARK_Scope (N);
|
||||
end if;
|
||||
|
@ -244,6 +246,11 @@ package body SPARK_Specific is
|
|||
procedure Traverse_Scopes is new
|
||||
Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
|
||||
|
||||
-- Local variables
|
||||
|
||||
File_Name : String_Ptr;
|
||||
Unit_File_Name : String_Ptr;
|
||||
|
||||
-- Start of processing for Add_SPARK_File
|
||||
|
||||
begin
|
||||
|
@ -307,6 +314,9 @@ package body SPARK_Specific is
|
|||
function Get_Entity_Type (E : Entity_Id) return Character;
|
||||
-- Return a character representing the type of entity
|
||||
|
||||
function Get_Scope_Num (N : Entity_Id) return Nat;
|
||||
-- Return the scope number associated to entity N
|
||||
|
||||
function Is_Constant_Object_Without_Variable_Input
|
||||
(E : Entity_Id) return Boolean;
|
||||
-- Return True if E is known to have no variable input, as defined in
|
||||
|
@ -333,6 +343,9 @@ package body SPARK_Specific is
|
|||
procedure Move (From : Natural; To : Natural);
|
||||
-- Move procedure for Sort call
|
||||
|
||||
procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
|
||||
-- Associate entity N to scope number Num
|
||||
|
||||
procedure Update_Scope_Range
|
||||
(S : Scope_Index;
|
||||
From : Xref_Index;
|
||||
|
@ -341,12 +354,6 @@ package body SPARK_Specific is
|
|||
|
||||
package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
|
||||
|
||||
function Get_Scope_Num (N : Entity_Id) return Nat;
|
||||
-- Return the scope number associated to entity N
|
||||
|
||||
procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
|
||||
-- Associate entity N to scope number Num
|
||||
|
||||
No_Scope : constant Nat := 0;
|
||||
-- Initial scope counter
|
||||
|
||||
|
@ -551,7 +558,7 @@ package body SPARK_Specific is
|
|||
-- Lt --
|
||||
--------
|
||||
|
||||
function Lt (Op1, Op2 : Natural) return Boolean is
|
||||
function Lt (Op1 : Natural; Op2 : Natural) return Boolean is
|
||||
T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
|
||||
T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
|
||||
|
||||
|
@ -767,9 +774,7 @@ package body SPARK_Specific is
|
|||
Nrefs := 1;
|
||||
|
||||
for Index in 2 .. Ref_Count loop
|
||||
if Xrefs.Table (Rnums (Index)) /=
|
||||
Xrefs.Table (Rnums (Nrefs))
|
||||
then
|
||||
if Xrefs.Table (Rnums (Index)) /= Xrefs.Table (Rnums (Nrefs)) then
|
||||
Nrefs := Nrefs + 1;
|
||||
Rnums (Nrefs) := Rnums (Index);
|
||||
end if;
|
||||
|
@ -900,7 +905,8 @@ package body SPARK_Specific is
|
|||
(Sdep_Table : Unit_Ref_Table;
|
||||
Num_Sdep : Nat)
|
||||
is
|
||||
Sdep, Sdep_Next : Pos;
|
||||
Sdep : Pos;
|
||||
Sdep_Next : Pos;
|
||||
-- Index of the current and next source dependency
|
||||
|
||||
Sdep_File : Pos;
|
||||
|
@ -908,7 +914,8 @@ package body SPARK_Specific is
|
|||
-- library-level instances of generic units this points to the unit
|
||||
-- of the body, because this is where references are assigned to.
|
||||
|
||||
Uspec, Ubody : Unit_Number_Type;
|
||||
Ubody : Unit_Number_Type;
|
||||
Uspec : Unit_Number_Type;
|
||||
-- Unit numbers for the dependency spec and possibly its body (only in
|
||||
-- the case of library-level instance of a generic package).
|
||||
|
||||
|
@ -936,20 +943,22 @@ package body SPARK_Specific is
|
|||
declare
|
||||
Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep));
|
||||
Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1));
|
||||
|
||||
begin
|
||||
-- Both Cunit point to compilation unit nodes
|
||||
pragma Assert (Nkind (Cunit1) = N_Compilation_Unit
|
||||
and then
|
||||
Nkind (Cunit2) = N_Compilation_Unit);
|
||||
|
||||
pragma Assert
|
||||
(Nkind (Cunit1) = N_Compilation_Unit
|
||||
and then Nkind (Cunit2) = N_Compilation_Unit);
|
||||
|
||||
-- Do not depend on the sorting order, which is based on
|
||||
-- Unit_Name and for library-level instances of nested
|
||||
-- generic-packages they are equal.
|
||||
|
||||
-- If declaration comes before the body
|
||||
|
||||
if Nkind (Unit (Cunit1)) = N_Package_Declaration
|
||||
and then
|
||||
Nkind (Unit (Cunit2)) = N_Package_Body
|
||||
and then Nkind (Unit (Cunit2)) = N_Package_Body
|
||||
then
|
||||
Uspec := Sdep_Table (Sdep);
|
||||
Ubody := Sdep_Table (Sdep + 1);
|
||||
|
@ -959,8 +968,7 @@ package body SPARK_Specific is
|
|||
-- If body comes before declaration
|
||||
|
||||
elsif Nkind (Unit (Cunit1)) = N_Package_Body
|
||||
and then
|
||||
Nkind (Unit (Cunit2)) = N_Package_Declaration
|
||||
and then Nkind (Unit (Cunit2)) = N_Package_Declaration
|
||||
then
|
||||
Uspec := Sdep_Table (Sdep + 1);
|
||||
Ubody := Sdep_Table (Sdep);
|
||||
|
@ -970,18 +978,19 @@ package body SPARK_Specific is
|
|||
-- Otherwise it is an error
|
||||
|
||||
else
|
||||
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
Sdep_Next := Sdep + 2;
|
||||
end;
|
||||
|
||||
-- ??? otherwise?
|
||||
|
||||
else
|
||||
Uspec := Sdep_Table (Sdep);
|
||||
Ubody := No_Unit;
|
||||
|
||||
Sdep_File := Sdep;
|
||||
|
||||
Sdep_Next := Sdep + 1;
|
||||
end if;
|
||||
|
||||
|
@ -1191,7 +1200,6 @@ package body SPARK_Specific is
|
|||
-- Start of processing for Generate_Dereference
|
||||
|
||||
begin
|
||||
|
||||
if Loc > No_Location then
|
||||
Drefs.Increment_Last;
|
||||
|
||||
|
@ -1234,11 +1242,9 @@ package body SPARK_Specific is
|
|||
(CU : Node_Id;
|
||||
Inside_Stubs : Boolean)
|
||||
is
|
||||
Lu : Node_Id;
|
||||
|
||||
procedure Traverse_Block (N : Node_Id);
|
||||
procedure Traverse_Declarations_And_HSS (N : Node_Id);
|
||||
procedure Traverse_Declaration_Or_Statement (N : Node_Id);
|
||||
procedure Traverse_Declarations_And_HSS (N : Node_Id);
|
||||
procedure Traverse_Declarations_Or_Statements (L : List_Id);
|
||||
procedure Traverse_Handled_Statement_Sequence (N : Node_Id);
|
||||
procedure Traverse_Package_Body (N : Node_Id);
|
||||
|
@ -1260,133 +1266,129 @@ package body SPARK_Specific is
|
|||
-- Traverse_Declaration_Or_Statement --
|
||||
---------------------------------------
|
||||
|
||||
procedure Traverse_Declaration_Or_Statement (N : Node_Id)
|
||||
is
|
||||
procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
|
||||
begin
|
||||
case Nkind (N) is
|
||||
when N_Package_Declaration =>
|
||||
Traverse_Visible_And_Private_Parts (Specification (N));
|
||||
when N_Package_Declaration =>
|
||||
Traverse_Visible_And_Private_Parts (Specification (N));
|
||||
|
||||
when N_Package_Body =>
|
||||
if Ekind (Defining_Entity (N)) /= E_Generic_Package then
|
||||
Traverse_Package_Body (N);
|
||||
end if;
|
||||
when N_Package_Body =>
|
||||
if Ekind (Defining_Entity (N)) /= E_Generic_Package then
|
||||
Traverse_Package_Body (N);
|
||||
end if;
|
||||
|
||||
when N_Package_Body_Stub =>
|
||||
if Present (Library_Unit (N)) then
|
||||
declare
|
||||
Body_N : constant Node_Id := Get_Body_From_Stub (N);
|
||||
begin
|
||||
if Inside_Stubs
|
||||
and then
|
||||
Ekind (Defining_Entity (Body_N)) /= E_Generic_Package
|
||||
then
|
||||
Traverse_Package_Body (Body_N);
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
when N_Package_Body_Stub =>
|
||||
if Present (Library_Unit (N)) then
|
||||
declare
|
||||
Body_N : constant Node_Id := Get_Body_From_Stub (N);
|
||||
begin
|
||||
if Inside_Stubs
|
||||
and then Ekind (Defining_Entity (Body_N)) /=
|
||||
E_Generic_Package
|
||||
then
|
||||
Traverse_Package_Body (Body_N);
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
|
||||
when N_Subprogram_Body =>
|
||||
if not Is_Generic_Subprogram (Defining_Entity (N)) then
|
||||
when N_Subprogram_Body =>
|
||||
if not Is_Generic_Subprogram (Defining_Entity (N)) then
|
||||
Traverse_Subprogram_Body (N);
|
||||
end if;
|
||||
|
||||
when N_Entry_Body =>
|
||||
Traverse_Subprogram_Body (N);
|
||||
end if;
|
||||
|
||||
when N_Entry_Body =>
|
||||
Traverse_Subprogram_Body (N);
|
||||
when N_Subprogram_Body_Stub =>
|
||||
if Present (Library_Unit (N)) then
|
||||
declare
|
||||
Body_N : constant Node_Id := Get_Body_From_Stub (N);
|
||||
begin
|
||||
if Inside_Stubs
|
||||
and then
|
||||
not Is_Generic_Subprogram (Defining_Entity (Body_N))
|
||||
then
|
||||
Traverse_Subprogram_Body (Body_N);
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
|
||||
when N_Subprogram_Body_Stub =>
|
||||
if Present (Library_Unit (N)) then
|
||||
declare
|
||||
Body_N : constant Node_Id := Get_Body_From_Stub (N);
|
||||
begin
|
||||
if Inside_Stubs
|
||||
and then
|
||||
not Is_Generic_Subprogram (Defining_Entity (Body_N))
|
||||
then
|
||||
Traverse_Subprogram_Body (Body_N);
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
when N_Protected_Body =>
|
||||
Traverse_Protected_Body (N);
|
||||
|
||||
when N_Protected_Body =>
|
||||
Traverse_Protected_Body (N);
|
||||
|
||||
when N_Protected_Body_Stub =>
|
||||
if Present (Library_Unit (N)) then
|
||||
if Inside_Stubs then
|
||||
when N_Protected_Body_Stub =>
|
||||
if Present (Library_Unit (N)) and then Inside_Stubs then
|
||||
Traverse_Protected_Body (Get_Body_From_Stub (N));
|
||||
end if;
|
||||
end if;
|
||||
|
||||
when N_Protected_Type_Declaration | N_Single_Protected_Declaration =>
|
||||
Traverse_Visible_And_Private_Parts (Protected_Definition (N));
|
||||
when N_Protected_Type_Declaration |
|
||||
N_Single_Protected_Declaration =>
|
||||
Traverse_Visible_And_Private_Parts (Protected_Definition (N));
|
||||
|
||||
when N_Task_Definition =>
|
||||
Traverse_Visible_And_Private_Parts (N);
|
||||
when N_Task_Definition =>
|
||||
Traverse_Visible_And_Private_Parts (N);
|
||||
|
||||
when N_Task_Body =>
|
||||
Traverse_Task_Body (N);
|
||||
when N_Task_Body =>
|
||||
Traverse_Task_Body (N);
|
||||
|
||||
when N_Task_Body_Stub =>
|
||||
if Present (Library_Unit (N)) then
|
||||
if Inside_Stubs then
|
||||
when N_Task_Body_Stub =>
|
||||
if Present (Library_Unit (N)) and then Inside_Stubs then
|
||||
Traverse_Task_Body (Get_Body_From_Stub (N));
|
||||
end if;
|
||||
end if;
|
||||
|
||||
when N_Block_Statement =>
|
||||
Traverse_Block (N);
|
||||
when N_Block_Statement =>
|
||||
Traverse_Block (N);
|
||||
|
||||
when N_If_Statement =>
|
||||
when N_If_Statement =>
|
||||
|
||||
-- Traverse the statements in the THEN part
|
||||
-- Traverse the statements in the THEN part
|
||||
|
||||
Traverse_Declarations_Or_Statements (Then_Statements (N));
|
||||
Traverse_Declarations_Or_Statements (Then_Statements (N));
|
||||
|
||||
-- Loop through ELSIF parts if present
|
||||
-- Loop through ELSIF parts if present
|
||||
|
||||
if Present (Elsif_Parts (N)) then
|
||||
declare
|
||||
Elif : Node_Id := First (Elsif_Parts (N));
|
||||
|
||||
begin
|
||||
while Present (Elif) loop
|
||||
Traverse_Declarations_Or_Statements
|
||||
(Then_Statements (Elif));
|
||||
Next (Elif);
|
||||
end loop;
|
||||
end;
|
||||
end if;
|
||||
|
||||
-- Finally traverse the ELSE statements if present
|
||||
|
||||
Traverse_Declarations_Or_Statements (Else_Statements (N));
|
||||
|
||||
when N_Case_Statement =>
|
||||
|
||||
-- Process case branches
|
||||
|
||||
if Present (Elsif_Parts (N)) then
|
||||
declare
|
||||
Elif : Node_Id := First (Elsif_Parts (N));
|
||||
|
||||
Alt : Node_Id;
|
||||
begin
|
||||
while Present (Elif) loop
|
||||
Traverse_Declarations_Or_Statements
|
||||
(Then_Statements (Elif));
|
||||
Next (Elif);
|
||||
Alt := First (Alternatives (N));
|
||||
while Present (Alt) loop
|
||||
Traverse_Declarations_Or_Statements (Statements (Alt));
|
||||
Next (Alt);
|
||||
end loop;
|
||||
end;
|
||||
end if;
|
||||
|
||||
-- Finally traverse the ELSE statements if present
|
||||
when N_Extended_Return_Statement =>
|
||||
Traverse_Handled_Statement_Sequence
|
||||
(Handled_Statement_Sequence (N));
|
||||
|
||||
Traverse_Declarations_Or_Statements (Else_Statements (N));
|
||||
when N_Loop_Statement =>
|
||||
Traverse_Declarations_Or_Statements (Statements (N));
|
||||
|
||||
when N_Case_Statement =>
|
||||
-- Generic declarations are ignored
|
||||
|
||||
-- Process case branches
|
||||
|
||||
declare
|
||||
Alt : Node_Id;
|
||||
begin
|
||||
Alt := First (Alternatives (N));
|
||||
while Present (Alt) loop
|
||||
Traverse_Declarations_Or_Statements (Statements (Alt));
|
||||
Next (Alt);
|
||||
end loop;
|
||||
end;
|
||||
|
||||
when N_Extended_Return_Statement =>
|
||||
Traverse_Handled_Statement_Sequence
|
||||
(Handled_Statement_Sequence (N));
|
||||
|
||||
when N_Loop_Statement =>
|
||||
Traverse_Declarations_Or_Statements (Statements (N));
|
||||
|
||||
-- Generic declarations are ignored
|
||||
|
||||
when others =>
|
||||
null;
|
||||
when others =>
|
||||
null;
|
||||
end case;
|
||||
end Traverse_Declaration_Or_Statement;
|
||||
|
||||
|
@ -1394,8 +1396,7 @@ package body SPARK_Specific is
|
|||
-- Traverse_Declarations_And_HSS --
|
||||
-----------------------------------
|
||||
|
||||
procedure Traverse_Declarations_And_HSS (N : Node_Id)
|
||||
is
|
||||
procedure Traverse_Declarations_And_HSS (N : Node_Id) is
|
||||
begin
|
||||
Traverse_Declarations_Or_Statements (Declarations (N));
|
||||
Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N));
|
||||
|
@ -1405,8 +1406,7 @@ package body SPARK_Specific is
|
|||
-- Traverse_Declarations_Or_Statements --
|
||||
-----------------------------------------
|
||||
|
||||
procedure Traverse_Declarations_Or_Statements (L : List_Id)
|
||||
is
|
||||
procedure Traverse_Declarations_Or_Statements (L : List_Id) is
|
||||
N : Node_Id;
|
||||
|
||||
begin
|
||||
|
@ -1414,13 +1414,12 @@ package body SPARK_Specific is
|
|||
|
||||
N := First (L);
|
||||
while Present (N) loop
|
||||
|
||||
-- Call Process on all declarations
|
||||
|
||||
if Nkind (N) in N_Declaration
|
||||
or else
|
||||
Nkind (N) in N_Later_Decl_Item
|
||||
or else
|
||||
Nkind (N) = N_Entry_Body
|
||||
or else Nkind (N) in N_Later_Decl_Item
|
||||
or else Nkind (N) = N_Entry_Body
|
||||
then
|
||||
Process (N);
|
||||
end if;
|
||||
|
@ -1435,8 +1434,7 @@ package body SPARK_Specific is
|
|||
-- Traverse_Handled_Statement_Sequence --
|
||||
-----------------------------------------
|
||||
|
||||
procedure Traverse_Handled_Statement_Sequence (N : Node_Id)
|
||||
is
|
||||
procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is
|
||||
Handler : Node_Id;
|
||||
|
||||
begin
|
||||
|
@ -1483,12 +1481,20 @@ package body SPARK_Specific is
|
|||
procedure Traverse_Task_Body (N : Node_Id) renames
|
||||
Traverse_Declarations_And_HSS;
|
||||
|
||||
----------------------------------------
|
||||
-- Traverse_Visible_And_Private_Parts --
|
||||
----------------------------------------
|
||||
|
||||
procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is
|
||||
begin
|
||||
Traverse_Declarations_Or_Statements (Visible_Declarations (N));
|
||||
Traverse_Declarations_Or_Statements (Private_Declarations (N));
|
||||
end Traverse_Visible_And_Private_Parts;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Lu : Node_Id;
|
||||
|
||||
-- Start of processing for Traverse_Compilation_Unit
|
||||
|
||||
begin
|
||||
|
|
|
@ -548,6 +548,12 @@ package Lib is
|
|||
-- This is like Get_Code_Unit, except that in the case of subunits, it
|
||||
-- returns the top-level unit to which the subunit belongs instead of
|
||||
-- the subunit.
|
||||
--
|
||||
-- Note: for nodes and slocs in declarations of library-level instances of
|
||||
-- generics these routines wrongly return the unit number corresponding to
|
||||
-- the body of the instance. In effect, locations of SPARK references in
|
||||
-- ALI files are bogus. However, fixing this is not worth the effort, since
|
||||
-- these references are only used for debugging.
|
||||
|
||||
function In_Extended_Main_Code_Unit
|
||||
(N : Node_Or_Entity_Id) return Boolean;
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- B o d y --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
|
||||
-- --
|
||||
-- GNARL is free software; you can redistribute it and/or modify it under --
|
||||
-- terms of the GNU General Public License as published by the Free Soft- --
|
||||
|
@ -1339,7 +1339,13 @@ package body System.Tasking.Stages is
|
|||
|
||||
if Self_ID.Common.Specific_Handler /= null then
|
||||
TH := Self_ID.Common.Specific_Handler;
|
||||
else
|
||||
|
||||
-- Independent tasks should not call the Fall_Back_Handler (of the
|
||||
-- environment task), because they are implementation artifacts that
|
||||
-- should be invisible to Ada programs.
|
||||
|
||||
elsif Self_ID.Master_of_Task /= Independent_Task_Level then
|
||||
|
||||
-- Look for a fall-back handler following the master relationship
|
||||
-- for the task. As specified in ARM C.7.3 par. 9/2, "the fall-back
|
||||
-- handler applies only to the dependent tasks of the task". Hence,
|
||||
|
|
|
@ -13204,11 +13204,11 @@ package body Sem_Ch13 is
|
|||
-- Get alignments, sizes and offset, if any
|
||||
|
||||
X_Alignment := Alignment (ACCR.X);
|
||||
X_Size := Esize (ACCR.X);
|
||||
X_Size := Esize (ACCR.X);
|
||||
|
||||
if Present (ACCR.Y) then
|
||||
Y_Alignment := Alignment (ACCR.Y);
|
||||
Y_Size := Esize (ACCR.Y);
|
||||
Y_Size := Esize (ACCR.Y);
|
||||
end if;
|
||||
|
||||
if ACCR.Off
|
||||
|
|
|
@ -1121,13 +1121,15 @@ package body Sem_Dim is
|
|||
begin
|
||||
-- Aspect is an Ada 2012 feature. Note that there is no need to check
|
||||
-- dimensions for nodes that don't come from source, except for subtype
|
||||
-- declarations where the dimensions are inherited from the base type.
|
||||
-- declarations where the dimensions are inherited from the base type,
|
||||
-- and for explicit dereferences generated when expanding iterators.
|
||||
|
||||
if Ada_Version < Ada_2012 then
|
||||
return;
|
||||
|
||||
elsif not Comes_From_Source (N)
|
||||
and then Nkind (N) /= N_Subtype_Declaration
|
||||
and then Nkind (N) /= N_Explicit_Dereference
|
||||
then
|
||||
return;
|
||||
end if;
|
||||
|
@ -2015,7 +2017,8 @@ package body Sem_Dim is
|
|||
end if;
|
||||
end if;
|
||||
|
||||
-- Removal of dimensions in expression
|
||||
-- Remove dimensions from inner expressions, to prevent dimensions
|
||||
-- table from growing uselessly.
|
||||
|
||||
case Nkind (N) is
|
||||
when N_Attribute_Reference |
|
||||
|
|
Loading…
Reference in New Issue