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.
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);
-- 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)).
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
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 =>
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);
-- 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
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;
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).
-- 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;
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 --
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);
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 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
- when others =>
- raise Program_Error;
+ return;
+
+ when others =>
+ raise Program_Error;
end case;
-- File_Num and Scope_Num are filled later. From_Xref and To_Xref
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;
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
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
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;
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
-- 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)));
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;
(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;
-- 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).
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);
-- 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);
-- 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;
-- Start of processing for Generate_Dereference
begin
-
if Loc > No_Location then
Drefs.Increment_Last;
(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);
-- 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
- Traverse_Subprogram_Body (N);
- end if;
+ 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);
+ 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));
+ 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;
+ 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
+ -- Finally traverse the ELSE statements if present
- Traverse_Declarations_Or_Statements (Else_Statements (N));
+ Traverse_Declarations_Or_Statements (Else_Statements (N));
- when N_Case_Statement =>
+ when N_Case_Statement =>
- -- Process case branches
+ -- 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;
+ 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_Extended_Return_Statement =>
+ Traverse_Handled_Statement_Sequence
+ (Handled_Statement_Sequence (N));
- when N_Loop_Statement =>
- Traverse_Declarations_Or_Statements (Statements (N));
+ when N_Loop_Statement =>
+ Traverse_Declarations_Or_Statements (Statements (N));
- -- Generic declarations are ignored
+ -- Generic declarations are ignored
- when others =>
- null;
+ when others =>
+ null;
end case;
end Traverse_Declaration_Or_Statement;
-- 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));
-- 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
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;
-- 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
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
projects / gcc.git / commitdiff