+2017-01-19 Steve Baird <baird@adacore.com>
+
+ * sem_util.ads: Add new Use_Full_View Boolean parameter to
+ Get_Index_Bounds.
+ * sem_util.adb (Get_Index_Bounds): replace calls to Scalar_Range with
+ calls to a newly-defined Scalar_Range_Of_Right_View function.
+
+2017-01-19 Arnaud Charlet <charlet@adacore.com>
+
+ * gnat1drv.adb: minor fix of unbalanced parens in comment
+ * lib-xref.ads (Traverse_Compilation_Unit): declaration moved
+ to visible part of the package to allow re-use in GNATprove.
+ * lib-xref-spark_specific.adb (Traverse_Stub): routine refactored
+ from repeated code of Traverse_Compilation_Unit.
+ (Traverse_Declaration_Or_Statement): fixed detection of
+ generic subprograms and packages; also, iteration over case
+ statement alternatives rewritten to avoid testing if the first
+ alternative is present (since it must be present due to Ada
+ syntax restrictions).
+
2017-01-19 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch6.adb (Expand_N_Subprogram_Body): Mark the spec as
function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
-- Hash function for hash table
- generic
- with procedure Process (N : Node_Id) is <>;
- procedure Traverse_Compilation_Unit (CU : Node_Id; Inside_Stubs : Boolean);
- -- 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 --
--------------------
---------------------------------------
procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
+ function Traverse_Stub (N : Node_Id) return Boolean;
+ -- Returns True iff stub N should be traversed
+
+ function Traverse_Stub (N : Node_Id) return Boolean is
+ begin
+ pragma Assert (Nkind_In (N, N_Package_Body_Stub,
+ N_Protected_Body_Stub,
+ N_Subprogram_Body_Stub,
+ N_Task_Body_Stub));
+
+ return Inside_Stubs and then Present (Library_Unit (N));
+ end Traverse_Stub;
+
+ -- Start of processing for Traverse_Declaration_Or_Statement
+
begin
case Nkind (N) is
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;
+ Traverse_Package_Body (N);
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;
+ if Traverse_Stub (N) then
+ Traverse_Package_Body (Get_Body_From_Stub (N));
end if;
when N_Subprogram_Body =>
- if not Is_Generic_Subprogram (Defining_Entity (N)) then
- Traverse_Subprogram_Body (N);
- end if;
+ Traverse_Subprogram_Body (N);
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;
+ if Traverse_Stub (N) then
+ Traverse_Subprogram_Body (Get_Body_From_Stub (N));
end if;
when N_Protected_Body =>
Traverse_Protected_Body (N);
when N_Protected_Body_Stub =>
- if Present (Library_Unit (N)) and then Inside_Stubs then
+ if Traverse_Stub (N) then
Traverse_Protected_Body (Get_Body_From_Stub (N));
end if;
- when N_Protected_Type_Declaration
- | N_Single_Protected_Declaration
- =>
+ when N_Protected_Type_Declaration =>
Traverse_Visible_And_Private_Parts (Protected_Definition (N));
when N_Task_Definition =>
Traverse_Task_Body (N);
when N_Task_Body_Stub =>
- if Present (Library_Unit (N)) and then Inside_Stubs then
+ if Traverse_Stub (N) then
Traverse_Task_Body (Get_Body_From_Stub (N));
end if;
-- Process case branches
declare
- Alt : Node_Id;
+ Alt : Node_Id := First (Alternatives (N));
begin
- Alt := First (Alternatives (N));
- while Present (Alt) loop
+ loop
Traverse_Declarations_Or_Statements (Statements (Alt));
Next (Alt);
+ exit when No (Alt);
end loop;
end;
-- Traverse_Package_Body --
---------------------------
- procedure Traverse_Package_Body (N : Node_Id) renames
- Traverse_Declarations_And_HSS;
+ procedure Traverse_Package_Body (N : Node_Id) is
+ Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
+ begin
+ case Ekind (Spec_E) is
+ when E_Package =>
+ Traverse_Declarations_And_HSS (N);
+ when E_Generic_Package =>
+ null;
+ when others =>
+ raise Program_Error;
+ end case;
+ end Traverse_Package_Body;
-----------------------------
-- Traverse_Protected_Body --
-- Traverse_Subprogram_Body --
------------------------------
- procedure Traverse_Subprogram_Body (N : Node_Id) renames
- Traverse_Declarations_And_HSS;
+ procedure Traverse_Subprogram_Body (N : Node_Id) is
+ Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
+ begin
+ case Ekind (Spec_E) is
+ when E_Function | E_Procedure | Entry_Kind =>
+ Traverse_Declarations_And_HSS (N);
+ when Generic_Subprogram_Kind =>
+ null;
+ when others =>
+ raise Program_Error;
+ end case;
+ end Traverse_Subprogram_Body;
------------------------
-- Traverse_Task_Body --
-- Get_Index_Bounds --
----------------------
- procedure Get_Index_Bounds (N : Node_Id; L, H : out Node_Id) is
+ procedure Get_Index_Bounds
+ (N : Node_Id;
+ L, H : out Node_Id;
+ Use_Full_View : Boolean := False)
+ is
Kind : constant Node_Kind := Nkind (N);
R : Node_Id;
+ function Scalar_Range_Of_Right_View return Node_Id;
+ -- Call Scalar_Range with argument determined by Use_Full_View
+ -- parameter.
+
+ --------------------------------
+ -- Scalar_Range_Of_Right_View --
+ --------------------------------
+
+ function Scalar_Range_Of_Right_View return Node_Id is
+ E : Entity_Id := Entity (N);
+ begin
+ if Use_Full_View and then Present (Full_View (E)) then
+ E := Full_View (E);
+ end if;
+ return Scalar_Range (E);
+ end Scalar_Range_Of_Right_View;
+
begin
if Kind = N_Range then
L := Low_Bound (N);
end if;
elsif Is_Entity_Name (N) and then Is_Type (Entity (N)) then
- if Error_Posted (Scalar_Range (Entity (N))) then
+ if Error_Posted (Scalar_Range_Of_Right_View) then
L := Error;
H := Error;
- elsif Nkind (Scalar_Range (Entity (N))) = N_Subtype_Indication then
- Get_Index_Bounds (Scalar_Range (Entity (N)), L, H);
+ elsif Nkind (Scalar_Range_Of_Right_View) = N_Subtype_Indication then
+ Get_Index_Bounds (Scalar_Range_Of_Right_View, L, H);
else
- L := Low_Bound (Scalar_Range (Entity (N)));
- H := High_Bound (Scalar_Range (Entity (N)));
+ L := Low_Bound (Scalar_Range_Of_Right_View);
+ H := High_Bound (Scalar_Range_Of_Right_View);
end if;
else
-- ancestor declared in a parent unit, even if there is an intermediate
-- derivation that does not see the full view of that ancestor.
- procedure Get_Index_Bounds (N : Node_Id; L, H : out Node_Id);
+ procedure Get_Index_Bounds
+ (N : Node_Id;
+ L, H : out Node_Id;
+ Use_Full_View : Boolean := False);
-- This procedure assigns to L and H respectively the values of the low and
-- high bounds of node N, which must be a range, subtype indication, or the
-- name of a scalar subtype. The result in L, H may be set to Error if
-- there was an earlier error in the range.
+ -- Use_Full_View is intended for use by clients other than the compiler
+ -- (specifically, gnat2scil) to indicate that we want the full view if
+ -- the index type turns out to be a partial view; this case should
+ -- not arise during normal compilation of semantically correct programs.
function Get_Enum_Lit_From_Pos
(T : Entity_Id;