[multiple changes]
2011-08-04 Yannick Moy <moy@adacore.com> * alfa.adb, alfa.ads (Get_Entity_For_Decl): remove function, partial duplicate of Defining_Entity (Get_Unique_Entity_For_Decl): rename function into Unique_Defining_Entity * einfo.adb, einfo.ads (Is_In_ALFA, Body_Is_In_ALFA): remove flags (Formal_Proof_On): remove synthesized flag * cstand.adb, sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch9.adb, sem_res.adb, sem_util.adb, sem_util.ads, stand.ads: Remove treatment associated to entities in ALFA * sem_prag.adb (Analyze_Pragma): remove special treatment for pragma Annotate (Formal_Proof) 2011-08-04 Emmanuel Briot <briot@adacore.com> * prj-env.adb (Create_Config_Pragmas_File): fix handling of multi-unit source files with non-standard naming schemes, in imported projects From-SVN: r177353
This commit is contained in:
parent
756ef2a03d
commit
ad05f2e9b8
|
@ -1,3 +1,22 @@
|
|||
2011-08-04 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* alfa.adb, alfa.ads (Get_Entity_For_Decl): remove function, partial
|
||||
duplicate of Defining_Entity
|
||||
(Get_Unique_Entity_For_Decl): rename function into
|
||||
Unique_Defining_Entity
|
||||
* einfo.adb, einfo.ads (Is_In_ALFA, Body_Is_In_ALFA): remove flags
|
||||
(Formal_Proof_On): remove synthesized flag
|
||||
* cstand.adb, sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb,
|
||||
sem_ch5.adb, sem_ch6.adb, sem_ch9.adb, sem_res.adb, sem_util.adb,
|
||||
sem_util.ads, stand.ads: Remove treatment associated to entities in ALFA
|
||||
* sem_prag.adb (Analyze_Pragma): remove special treatment for pragma
|
||||
Annotate (Formal_Proof)
|
||||
|
||||
2011-08-04 Emmanuel Briot <briot@adacore.com>
|
||||
|
||||
* prj-env.adb (Create_Config_Pragmas_File): fix handling of multi-unit
|
||||
source files with non-standard naming schemes, in imported projects
|
||||
|
||||
2011-08-04 Emmanuel Briot <briot@adacore.com>
|
||||
|
||||
* makeutl.adb (Complete_Mains): when a multi-unit source file is
|
||||
|
|
|
@ -26,6 +26,7 @@
|
|||
with Atree; use Atree;
|
||||
with Output; use Output;
|
||||
with Put_ALFA;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sinfo; use Sinfo;
|
||||
|
||||
package body ALFA is
|
||||
|
@ -144,74 +145,6 @@ package body ALFA is
|
|||
end loop;
|
||||
end dalfa;
|
||||
|
||||
-------------------------
|
||||
-- Get_Entity_For_Decl --
|
||||
-------------------------
|
||||
|
||||
function Get_Entity_For_Decl (N : Node_Id) return Entity_Id is
|
||||
E : Entity_Id := Empty;
|
||||
|
||||
begin
|
||||
case Nkind (N) is
|
||||
when N_Subprogram_Declaration |
|
||||
N_Subprogram_Body |
|
||||
N_Package_Declaration =>
|
||||
E := Defining_Unit_Name (Specification (N));
|
||||
|
||||
when N_Package_Body =>
|
||||
E := Defining_Unit_Name (N);
|
||||
|
||||
when N_Object_Declaration =>
|
||||
E := Defining_Identifier (N);
|
||||
|
||||
when others =>
|
||||
null;
|
||||
end case;
|
||||
|
||||
if Nkind (E) = N_Defining_Program_Unit_Name then
|
||||
E := Defining_Identifier (E);
|
||||
end if;
|
||||
|
||||
return E;
|
||||
end Get_Entity_For_Decl;
|
||||
|
||||
--------------------------------
|
||||
-- Get_Unique_Entity_For_Decl --
|
||||
--------------------------------
|
||||
|
||||
function Get_Unique_Entity_For_Decl (N : Node_Id) return Entity_Id is
|
||||
E : Entity_Id := Empty;
|
||||
|
||||
begin
|
||||
case Nkind (N) is
|
||||
when N_Subprogram_Declaration |
|
||||
N_Package_Declaration =>
|
||||
E := Defining_Unit_Name (Specification (N));
|
||||
|
||||
when N_Package_Body =>
|
||||
E := Corresponding_Spec (N);
|
||||
|
||||
when N_Subprogram_Body =>
|
||||
if Acts_As_Spec (N) then
|
||||
E := Defining_Unit_Name (Specification (N));
|
||||
else
|
||||
E := Corresponding_Spec (N);
|
||||
end if;
|
||||
|
||||
when N_Object_Declaration =>
|
||||
E := Defining_Identifier (N);
|
||||
|
||||
when others =>
|
||||
null;
|
||||
end case;
|
||||
|
||||
if Nkind (E) = N_Defining_Program_Unit_Name then
|
||||
E := Defining_Identifier (E);
|
||||
end if;
|
||||
|
||||
return E;
|
||||
end Get_Unique_Entity_For_Decl;
|
||||
|
||||
----------------
|
||||
-- Initialize --
|
||||
----------------
|
||||
|
@ -270,4 +203,26 @@ package body ALFA is
|
|||
Debug_Put_ALFA;
|
||||
end palfa;
|
||||
|
||||
----------------------------
|
||||
-- Unique_Defining_Entity --
|
||||
----------------------------
|
||||
|
||||
function Unique_Defining_Entity (N : Node_Id) return Entity_Id is
|
||||
begin
|
||||
case Nkind (N) is
|
||||
when N_Package_Body =>
|
||||
return Corresponding_Spec (N);
|
||||
|
||||
when N_Subprogram_Body =>
|
||||
if Acts_As_Spec (N) then
|
||||
return Defining_Entity (N);
|
||||
else
|
||||
return Corresponding_Spec (N);
|
||||
end if;
|
||||
|
||||
when others =>
|
||||
return Defining_Entity (N);
|
||||
end case;
|
||||
end Unique_Defining_Entity;
|
||||
|
||||
end ALFA;
|
||||
|
|
|
@ -319,10 +319,7 @@ package ALFA is
|
|||
procedure Initialize_ALFA_Tables;
|
||||
-- Reset tables for a new compilation
|
||||
|
||||
function Get_Entity_For_Decl (N : Node_Id) return Entity_Id;
|
||||
-- Return the entity for declaration N
|
||||
|
||||
function Get_Unique_Entity_For_Decl (N : Node_Id) return Entity_Id;
|
||||
function Unique_Defining_Entity (N : Node_Id) return Entity_Id;
|
||||
-- Return the entity which represents declaration N, so that matching
|
||||
-- declaration and body have the same entity.
|
||||
|
||||
|
|
|
@ -570,10 +570,6 @@ package body CStand is
|
|||
Decl := New_Node (N_Full_Type_Declaration, Stloc);
|
||||
end if;
|
||||
|
||||
if Standard_Type_Is_In_ALFA (S) then
|
||||
Set_Is_In_ALFA (Standard_Entity (S));
|
||||
end if;
|
||||
|
||||
Set_Is_Frozen (Standard_Entity (S));
|
||||
Set_Is_Public (Standard_Entity (S));
|
||||
Set_Defining_Identifier (Decl, Standard_Entity (S));
|
||||
|
@ -1334,7 +1330,6 @@ package body CStand is
|
|||
Set_Scope (Universal_Integer, Standard_Standard);
|
||||
Build_Signed_Integer_Type
|
||||
(Universal_Integer, Standard_Long_Long_Integer_Size);
|
||||
Set_Is_In_ALFA (Universal_Integer);
|
||||
|
||||
Universal_Real := New_Standard_Entity;
|
||||
Decl := New_Node (N_Full_Type_Declaration, Stloc);
|
||||
|
|
|
@ -409,7 +409,7 @@ package body Einfo is
|
|||
-- Is_Compilation_Unit Flag149
|
||||
-- Has_Pragma_Elaborate_Body Flag150
|
||||
|
||||
-- Is_In_ALFA Flag151
|
||||
-- (unused) Flag151
|
||||
-- Entry_Accepted Flag152
|
||||
-- Is_Obsolescent Flag153
|
||||
-- Has_Per_Object_Constraint Flag154
|
||||
|
@ -519,7 +519,7 @@ package body Einfo is
|
|||
-- Is_Safe_To_Reevaluate Flag249
|
||||
-- Has_Predicates Flag250
|
||||
|
||||
-- Body_Is_In_ALFA Flag251
|
||||
-- (unused) Flag251
|
||||
-- Is_Processed_Transient Flag252
|
||||
-- Is_Postcondition_Proc Flag253
|
||||
-- (unused) Flag254
|
||||
|
@ -652,12 +652,6 @@ package body Einfo is
|
|||
return Node19 (Id);
|
||||
end Body_Entity;
|
||||
|
||||
function Body_Is_In_ALFA (Id : E) return B is
|
||||
begin
|
||||
pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
|
||||
return Flag251 (Id);
|
||||
end Body_Is_In_ALFA;
|
||||
|
||||
function Body_Needed_For_SAL (Id : E) return B is
|
||||
begin
|
||||
pragma Assert
|
||||
|
@ -1854,11 +1848,6 @@ package body Einfo is
|
|||
return Flag24 (Id);
|
||||
end Is_Imported;
|
||||
|
||||
function Is_In_ALFA (Id : E) return B is
|
||||
begin
|
||||
return Flag151 (Id);
|
||||
end Is_In_ALFA;
|
||||
|
||||
function Is_Inlined (Id : E) return B is
|
||||
begin
|
||||
return Flag11 (Id);
|
||||
|
@ -3126,12 +3115,6 @@ package body Einfo is
|
|||
Set_Node19 (Id, V);
|
||||
end Set_Body_Entity;
|
||||
|
||||
procedure Set_Body_Is_In_ALFA (Id : E; V : B := True) is
|
||||
begin
|
||||
pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
|
||||
Set_Flag251 (Id, V);
|
||||
end Set_Body_Is_In_ALFA;
|
||||
|
||||
procedure Set_Body_Needed_For_SAL (Id : E; V : B := True) is
|
||||
begin
|
||||
pragma Assert
|
||||
|
@ -4374,11 +4357,6 @@ package body Einfo is
|
|||
Set_Flag24 (Id, V);
|
||||
end Set_Is_Imported;
|
||||
|
||||
procedure Set_Is_In_ALFA (Id : E; V : B := True) is
|
||||
begin
|
||||
Set_Flag151 (Id, V);
|
||||
end Set_Is_In_ALFA;
|
||||
|
||||
procedure Set_Is_Inlined (Id : E; V : B := True) is
|
||||
begin
|
||||
Set_Flag11 (Id, V);
|
||||
|
@ -5899,41 +5877,6 @@ package body Einfo is
|
|||
end if;
|
||||
end First_Formal_With_Extras;
|
||||
|
||||
---------------------
|
||||
-- Formal_Proof_On --
|
||||
---------------------
|
||||
|
||||
function Formal_Proof_On (Id : E) return B is
|
||||
N : Node_Id;
|
||||
Arg1 : Node_Id;
|
||||
Arg2 : Node_Id;
|
||||
|
||||
begin
|
||||
pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
|
||||
|
||||
N := First_Rep_Item (Id);
|
||||
while Present (N) loop
|
||||
if Nkind (N) = N_Pragma
|
||||
and then Get_Pragma_Id (Pragma_Name (N)) = Pragma_Annotate
|
||||
and then Present (Pragma_Argument_Associations (N))
|
||||
and then List_Length (Pragma_Argument_Associations (N)) = 2
|
||||
then
|
||||
Arg1 := First (Pragma_Argument_Associations (N));
|
||||
Arg2 := Next (Arg1);
|
||||
|
||||
if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof
|
||||
and then Chars (Get_Pragma_Arg (Arg2)) = Name_On
|
||||
then
|
||||
return True;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next_Rep_Item (N);
|
||||
end loop;
|
||||
|
||||
return False;
|
||||
end Formal_Proof_On;
|
||||
|
||||
-------------------------------------
|
||||
-- Get_Attribute_Definition_Clause --
|
||||
-------------------------------------
|
||||
|
@ -7449,7 +7392,6 @@ package body Einfo is
|
|||
end if;
|
||||
|
||||
W ("Address_Taken", Flag104 (Id));
|
||||
W ("Body_Is_In_ALFA", Flag251 (Id));
|
||||
W ("Body_Needed_For_SAL", Flag40 (Id));
|
||||
W ("C_Pass_By_Copy", Flag125 (Id));
|
||||
W ("Can_Never_Be_Null", Flag38 (Id));
|
||||
|
@ -7587,7 +7529,6 @@ package body Einfo is
|
|||
W ("Is_Hidden_Open_Scope", Flag171 (Id));
|
||||
W ("Is_Immediately_Visible", Flag7 (Id));
|
||||
W ("Is_Imported", Flag24 (Id));
|
||||
W ("Is_In_ALFA", Flag151 (Id));
|
||||
W ("Is_Inlined", Flag11 (Id));
|
||||
W ("Is_Instantiated", Flag126 (Id));
|
||||
W ("Is_Interface", Flag186 (Id));
|
||||
|
|
|
@ -486,11 +486,6 @@ package Einfo is
|
|||
-- Present in package and generic package entities, points to the
|
||||
-- corresponding package body entity if one is present.
|
||||
|
||||
-- Body_Is_In_ALFA (Flag251)
|
||||
-- Present in subprogram entities. Set for subprograms whose body belongs
|
||||
-- to the ALFA subset, which are eligible for formal verification through
|
||||
-- SPARK or Why tool-sets.
|
||||
|
||||
-- Body_Needed_For_SAL (Flag40)
|
||||
-- Present in package and subprogram entities that are compilation
|
||||
-- units. Indicates that the source for the body must be included
|
||||
|
@ -1272,11 +1267,6 @@ package Einfo is
|
|||
-- Float_Rep_Kind. Together with the Digits_Value uniquely defines
|
||||
-- the floating-point representation to be used.
|
||||
|
||||
-- Formal_Proof_On (synthesized)
|
||||
-- Applies to subprogram and generic subprogram entities. Returns True if
|
||||
-- the Rep_Item chain for the subprogram has a pragma Annotate which
|
||||
-- forces formal proof on the subprogram's body.
|
||||
|
||||
-- Freeze_Node (Node7)
|
||||
-- Present in all entities. If there is an associated freeze node for
|
||||
-- the entity, this field references this freeze node. If no freeze
|
||||
|
@ -2279,13 +2269,6 @@ package Einfo is
|
|||
-- Is_Incomplete_Type (synthesized)
|
||||
-- Applies to all entities, true for incomplete types and subtypes
|
||||
|
||||
-- Is_In_ALFA (Flag151)
|
||||
-- Present in all entities. Set for entities that belong to the ALFA
|
||||
-- subset, which are eligible for formal verification through SPARK or
|
||||
-- Why tool-sets. For a subprogram, this only means that a call to the
|
||||
-- subprogram can be formally analyzed. Another flag, Body_Is_In_ALFA,
|
||||
-- defines which subprograms can be formally analyzed.
|
||||
|
||||
-- Is_Inlined (Flag11)
|
||||
-- Present in all entities. Set for functions and procedures which are
|
||||
-- to be inlined. For subprograms created during expansion, this flag
|
||||
|
@ -5997,7 +5980,6 @@ package Einfo is
|
|||
function Barrier_Function (Id : E) return N;
|
||||
function Block_Node (Id : E) return N;
|
||||
function Body_Entity (Id : E) return E;
|
||||
function Body_Is_In_ALFA (Id : E) return B;
|
||||
function Body_Needed_For_SAL (Id : E) return B;
|
||||
function CR_Discriminant (Id : E) return E;
|
||||
function C_Pass_By_Copy (Id : E) return B;
|
||||
|
@ -6205,7 +6187,6 @@ package Einfo is
|
|||
function Is_Hidden_Open_Scope (Id : E) return B;
|
||||
function Is_Immediately_Visible (Id : E) return B;
|
||||
function Is_Imported (Id : E) return B;
|
||||
function Is_In_ALFA (Id : E) return B;
|
||||
function Is_Inlined (Id : E) return B;
|
||||
function Is_Interface (Id : E) return B;
|
||||
function Is_Instantiated (Id : E) return B;
|
||||
|
@ -6452,7 +6433,6 @@ package Einfo is
|
|||
function First_Component_Or_Discriminant (Id : E) return E;
|
||||
function First_Formal (Id : E) return E;
|
||||
function First_Formal_With_Extras (Id : E) return E;
|
||||
function Formal_Proof_On (Id : E) return B;
|
||||
function Has_Attach_Handler (Id : E) return B;
|
||||
function Has_Entries (Id : E) return B;
|
||||
function Has_Foreign_Convention (Id : E) return B;
|
||||
|
@ -6589,7 +6569,6 @@ package Einfo is
|
|||
procedure Set_Barrier_Function (Id : E; V : N);
|
||||
procedure Set_Block_Node (Id : E; V : N);
|
||||
procedure Set_Body_Entity (Id : E; V : E);
|
||||
procedure Set_Body_Is_In_ALFA (Id : E; V : B := True);
|
||||
procedure Set_Body_Needed_For_SAL (Id : E; V : B := True);
|
||||
procedure Set_CR_Discriminant (Id : E; V : E);
|
||||
procedure Set_C_Pass_By_Copy (Id : E; V : B := True);
|
||||
|
@ -6800,7 +6779,6 @@ package Einfo is
|
|||
procedure Set_Is_Hidden_Open_Scope (Id : E; V : B := True);
|
||||
procedure Set_Is_Immediately_Visible (Id : E; V : B := True);
|
||||
procedure Set_Is_Imported (Id : E; V : B := True);
|
||||
procedure Set_Is_In_ALFA (Id : E; V : B := True);
|
||||
procedure Set_Is_Inlined (Id : E; V : B := True);
|
||||
procedure Set_Is_Interface (Id : E; V : B := True);
|
||||
procedure Set_Is_Instantiated (Id : E; V : B := True);
|
||||
|
@ -7286,7 +7264,6 @@ package Einfo is
|
|||
pragma Inline (Barrier_Function);
|
||||
pragma Inline (Block_Node);
|
||||
pragma Inline (Body_Entity);
|
||||
pragma Inline (Body_Is_In_ALFA);
|
||||
pragma Inline (Body_Needed_For_SAL);
|
||||
pragma Inline (CR_Discriminant);
|
||||
pragma Inline (C_Pass_By_Copy);
|
||||
|
@ -7522,7 +7499,6 @@ package Einfo is
|
|||
pragma Inline (Is_Imported);
|
||||
pragma Inline (Is_Incomplete_Or_Private_Type);
|
||||
pragma Inline (Is_Incomplete_Type);
|
||||
pragma Inline (Is_In_ALFA);
|
||||
pragma Inline (Is_Inlined);
|
||||
pragma Inline (Is_Interface);
|
||||
pragma Inline (Is_Instantiated);
|
||||
|
@ -7731,7 +7707,6 @@ package Einfo is
|
|||
pragma Inline (Set_Barrier_Function);
|
||||
pragma Inline (Set_Block_Node);
|
||||
pragma Inline (Set_Body_Entity);
|
||||
pragma Inline (Set_Body_Is_In_ALFA);
|
||||
pragma Inline (Set_Body_Needed_For_SAL);
|
||||
pragma Inline (Set_CR_Discriminant);
|
||||
pragma Inline (Set_C_Pass_By_Copy);
|
||||
|
@ -7941,7 +7916,6 @@ package Einfo is
|
|||
pragma Inline (Set_Is_Hidden_Open_Scope);
|
||||
pragma Inline (Set_Is_Immediately_Visible);
|
||||
pragma Inline (Set_Is_Imported);
|
||||
pragma Inline (Set_Is_In_ALFA);
|
||||
pragma Inline (Set_Is_Inlined);
|
||||
pragma Inline (Set_Is_Interface);
|
||||
pragma Inline (Set_Is_Instantiated);
|
||||
|
|
|
@ -477,8 +477,6 @@ package body Prj.Env is
|
|||
File : File_Descriptor := Invalid_FD;
|
||||
|
||||
Current_Naming : Naming_Id;
|
||||
Iter : Source_Iterator;
|
||||
Source : Source_Id;
|
||||
|
||||
procedure Check
|
||||
(Project : Project_Id;
|
||||
|
@ -509,11 +507,13 @@ package body Prj.Env is
|
|||
In_Tree : Project_Tree_Ref;
|
||||
State : in out Integer)
|
||||
is
|
||||
pragma Unreferenced (State, In_Tree);
|
||||
pragma Unreferenced (State);
|
||||
|
||||
Lang : constant Language_Ptr :=
|
||||
Get_Language_From_Name (Project, "ada");
|
||||
Naming : Lang_Naming_Data;
|
||||
Iter : Source_Iterator;
|
||||
Source : Source_Id;
|
||||
|
||||
begin
|
||||
if Current_Verbosity = High then
|
||||
|
@ -528,6 +528,25 @@ package body Prj.Env is
|
|||
return;
|
||||
end if;
|
||||
|
||||
-- Visit all the files and process those that need an SFN pragma
|
||||
|
||||
Iter := For_Each_Source (In_Tree, Project);
|
||||
while Element (Iter) /= No_Source loop
|
||||
Source := Element (Iter);
|
||||
|
||||
Debug_Output ("MANU Source index=" & Source.Index'Img,
|
||||
Name_Id (Source.File));
|
||||
|
||||
if Source.Index >= 1
|
||||
and then not Source.Locally_Removed
|
||||
and then Source.Unit /= null
|
||||
then
|
||||
Put (Source);
|
||||
end if;
|
||||
|
||||
Next (Iter);
|
||||
end loop;
|
||||
|
||||
Naming := Lang.Config.Naming_Data;
|
||||
|
||||
-- Is the naming scheme of this project one that we know?
|
||||
|
@ -684,6 +703,7 @@ package body Prj.Env is
|
|||
-- Start of processing for Create_Config_Pragmas_File
|
||||
|
||||
begin
|
||||
Debug_Output ("MANU Create_Config_Pragmas_File", For_Project.Name);
|
||||
if not For_Project.Config_Checked then
|
||||
Naming_Table.Init (Namings);
|
||||
|
||||
|
@ -692,22 +712,6 @@ package body Prj.Env is
|
|||
Check_Imported_Projects
|
||||
(For_Project, In_Tree, Dummy, Imported_First => False);
|
||||
|
||||
-- Visit all the files and process those that need an SFN pragma
|
||||
|
||||
Iter := For_Each_Source (In_Tree, For_Project);
|
||||
while Element (Iter) /= No_Source loop
|
||||
Source := Element (Iter);
|
||||
|
||||
if Source.Index >= 1
|
||||
and then not Source.Locally_Removed
|
||||
and then Source.Unit /= null
|
||||
then
|
||||
Put (Source);
|
||||
end if;
|
||||
|
||||
Next (Iter);
|
||||
end loop;
|
||||
|
||||
-- If there are no non standard naming scheme, issue the GNAT
|
||||
-- standard naming scheme. This will tell the compiler that
|
||||
-- a project file is used and will forbid any pragma SFN.
|
||||
|
|
|
@ -434,7 +434,6 @@ package body Sem_Ch11 is
|
|||
P : Node_Id;
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("raise statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("raise statement is not allowed", N);
|
||||
Check_Unreachable_Code (N);
|
||||
|
||||
|
|
|
@ -24,14 +24,12 @@
|
|||
------------------------------------------------------------------------------
|
||||
|
||||
with Atree; use Atree;
|
||||
with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Namet; use Namet;
|
||||
with Opt; use Opt;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sinfo; use Sinfo;
|
||||
with Stand; use Stand;
|
||||
with Uintp; use Uintp;
|
||||
|
@ -76,13 +74,6 @@ package body Sem_Ch2 is
|
|||
return;
|
||||
else
|
||||
Find_Direct_Name (N);
|
||||
|
||||
if Present (Entity (N))
|
||||
and then Is_Object (Entity (N))
|
||||
and then not Is_In_ALFA (Entity (N))
|
||||
then
|
||||
Mark_Non_ALFA_Subprogram ("object is not in ALFA", N);
|
||||
end if;
|
||||
end if;
|
||||
end Analyze_Identifier;
|
||||
|
||||
|
|
|
@ -3057,17 +3057,6 @@ package body Sem_Ch3 is
|
|||
|
||||
Act_T := T;
|
||||
|
||||
-- The object is in ALFA if-and-only-if its type is in ALFA and it is
|
||||
-- not aliased.
|
||||
|
||||
if not Is_In_ALFA (T) then
|
||||
Mark_Non_ALFA_Subprogram ("object type is not in ALFA", N);
|
||||
elsif Aliased_Present (N) then
|
||||
Mark_Non_ALFA_Subprogram ("ALIASED is not in ALFA", N);
|
||||
else
|
||||
Set_Is_In_ALFA (Id);
|
||||
end if;
|
||||
|
||||
-- These checks should be performed before the initialization expression
|
||||
-- is considered, so that the Object_Definition node is still the same
|
||||
-- as in source code.
|
||||
|
@ -4661,7 +4650,6 @@ package body Sem_Ch3 is
|
|||
Nb_Index : Nat;
|
||||
P : constant Node_Id := Parent (Def);
|
||||
Priv : Entity_Id;
|
||||
T_In_ALFA : Boolean := True;
|
||||
|
||||
begin
|
||||
if Nkind (Def) = N_Constrained_Array_Definition then
|
||||
|
@ -4742,12 +4730,6 @@ package body Sem_Ch3 is
|
|||
|
||||
Make_Index (Index, P, Related_Id, Nb_Index);
|
||||
|
||||
if Present (Etype (Index))
|
||||
and then not Is_In_ALFA (Etype (Index))
|
||||
then
|
||||
T_In_ALFA := False;
|
||||
end if;
|
||||
|
||||
-- Check error of subtype with predicate for index type
|
||||
|
||||
Bad_Predicated_Subtype_Use
|
||||
|
@ -4769,18 +4751,10 @@ package body Sem_Ch3 is
|
|||
Check_SPARK_Restriction ("subtype mark required", Component_Typ);
|
||||
end if;
|
||||
|
||||
if Present (Element_Type)
|
||||
and then not Is_In_ALFA (Element_Type)
|
||||
then
|
||||
T_In_ALFA := False;
|
||||
end if;
|
||||
|
||||
-- Ada 2005 (AI-230): Access Definition case
|
||||
|
||||
else pragma Assert (Present (Access_Definition (Component_Def)));
|
||||
|
||||
T_In_ALFA := False;
|
||||
|
||||
-- Indicate that the anonymous access type is created by the
|
||||
-- array type declaration.
|
||||
|
||||
|
@ -4857,12 +4831,6 @@ package body Sem_Ch3 is
|
|||
(Implicit_Base, Finalize_Storage_Only
|
||||
(Element_Type));
|
||||
|
||||
-- Final check for static bounds on array
|
||||
|
||||
if not Has_Static_Array_Bounds (T) then
|
||||
T_In_ALFA := False;
|
||||
end if;
|
||||
|
||||
-- Unconstrained array case
|
||||
|
||||
else
|
||||
|
@ -4887,8 +4855,6 @@ package body Sem_Ch3 is
|
|||
|
||||
Set_Component_Type (Base_Type (T), Element_Type);
|
||||
Set_Packed_Array_Type (T, Empty);
|
||||
Set_Is_In_ALFA (T, T_In_ALFA);
|
||||
Set_Is_In_ALFA (Base_Type (T), T_In_ALFA);
|
||||
|
||||
if Aliased_Present (Component_Definition (Def)) then
|
||||
Check_SPARK_Restriction
|
||||
|
@ -11599,14 +11565,6 @@ package body Sem_Ch3 is
|
|||
C : constant Node_Id := Constraint (S);
|
||||
|
||||
begin
|
||||
-- By default, consider that the enumeration subtype is in ALFA if the
|
||||
-- entity of its subtype mark is in ALFA. This is reversed later if the
|
||||
-- range of the subtype is not static.
|
||||
|
||||
if Is_In_ALFA (T) then
|
||||
Set_Is_In_ALFA (Def_Id);
|
||||
end if;
|
||||
|
||||
Set_Ekind (Def_Id, E_Enumeration_Subtype);
|
||||
|
||||
Set_First_Literal (Def_Id, First_Literal (Base_Type (T)));
|
||||
|
@ -11829,14 +11787,6 @@ package body Sem_Ch3 is
|
|||
C : constant Node_Id := Constraint (S);
|
||||
|
||||
begin
|
||||
-- By default, consider that the integer subtype is in ALFA if the
|
||||
-- entity of its subtype mark is in ALFA. This is reversed later if the
|
||||
-- range of the subtype is not static.
|
||||
|
||||
if Is_In_ALFA (T) then
|
||||
Set_Is_In_ALFA (Def_Id);
|
||||
end if;
|
||||
|
||||
Set_Scalar_Range_For_Subtype (Def_Id, Range_Expression (C), T);
|
||||
|
||||
if Is_Modular_Integer_Type (T) then
|
||||
|
@ -14586,12 +14536,6 @@ package body Sem_Ch3 is
|
|||
Set_Enum_Esize (T);
|
||||
Set_Enum_Pos_To_Rep (T, Empty);
|
||||
|
||||
-- Enumeration type is in ALFA only if it is not a character type
|
||||
|
||||
if not Is_Character_Type (T) then
|
||||
Set_Is_In_ALFA (T);
|
||||
end if;
|
||||
|
||||
-- Set Discard_Names if configuration pragma set, or if there is
|
||||
-- a parameterless pragma in the current declarative region
|
||||
|
||||
|
@ -16550,19 +16494,6 @@ package body Sem_Ch3 is
|
|||
then
|
||||
Set_Is_Non_Static_Subtype (Def_Id);
|
||||
end if;
|
||||
|
||||
-- By default, consider that the subtype is in ALFA if its base type
|
||||
-- is in ALFA.
|
||||
|
||||
Set_Is_In_ALFA (Def_Id, Is_In_ALFA (Base_Type (Def_Id)));
|
||||
|
||||
-- In ALFA, all subtypes should have a static range
|
||||
|
||||
if Nkind (R) = N_Range
|
||||
and then not Is_Static_Range (R)
|
||||
then
|
||||
Set_Is_In_ALFA (Def_Id, False);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Final step is to label the index with this constructed type
|
||||
|
@ -19539,14 +19470,6 @@ package body Sem_Ch3 is
|
|||
Set_Ekind (Def_Id, E_Void);
|
||||
Process_Range_Expr_In_Decl (R, Subt);
|
||||
Set_Ekind (Def_Id, Kind);
|
||||
|
||||
-- In ALFA, all subtypes should have a static range
|
||||
|
||||
if Nkind (R) = N_Range
|
||||
and then not Is_Static_Range (R)
|
||||
then
|
||||
Set_Is_In_ALFA (Def_Id, False);
|
||||
end if;
|
||||
end Set_Scalar_Range_For_Subtype;
|
||||
|
||||
--------------------------------------------------------
|
||||
|
@ -19718,7 +19641,6 @@ package body Sem_Ch3 is
|
|||
Set_Scalar_Range (T, Def);
|
||||
Set_RM_Size (T, UI_From_Int (Minimum_Size (T)));
|
||||
Set_Is_Constrained (T);
|
||||
Set_Is_In_ALFA (T);
|
||||
end Signed_Integer_Type_Declaration;
|
||||
|
||||
end Sem_Ch3;
|
||||
|
|
|
@ -350,8 +350,6 @@ package body Sem_Ch4 is
|
|||
|
||||
procedure Analyze_Aggregate (N : Node_Id) is
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("aggregate is not in ALFA", N);
|
||||
|
||||
if No (Etype (N)) then
|
||||
Set_Etype (N, Any_Composite);
|
||||
end if;
|
||||
|
@ -371,7 +369,6 @@ package body Sem_Ch4 is
|
|||
C : Node_Id;
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("allocator is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("allocator is not allowed", N);
|
||||
|
||||
-- Deal with allocator restrictions
|
||||
|
@ -978,15 +975,6 @@ package body Sem_Ch4 is
|
|||
return;
|
||||
end if;
|
||||
|
||||
-- If this is an indirect call, or the subprogram called is not in
|
||||
-- ALFA, then the call is not in ALFA.
|
||||
|
||||
if not Is_Subprogram (Nam_Ent) then
|
||||
Mark_Non_ALFA_Subprogram ("indirect call is not in ALFA", N);
|
||||
elsif not Is_In_ALFA (Nam_Ent) then
|
||||
Mark_Non_ALFA_Subprogram ("call to subprogram not in ALFA", N);
|
||||
end if;
|
||||
|
||||
Analyze_One_Call (N, Nam_Ent, True, Success);
|
||||
|
||||
-- If this is an indirect call, the return type of the access_to
|
||||
|
@ -1363,8 +1351,6 @@ package body Sem_Ch4 is
|
|||
L : Node_Id;
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("concatenation is not in ALFA", N);
|
||||
|
||||
Candidate_Type := Empty;
|
||||
|
||||
-- The following code is equivalent to:
|
||||
|
@ -1517,26 +1503,6 @@ package body Sem_Ch4 is
|
|||
|
||||
Else_Expr := Next (Then_Expr);
|
||||
|
||||
-- In ALFA, boolean conditional expressions are allowed:
|
||||
-- * if they have no ELSE part, in which case the expression is
|
||||
-- equivalent to
|
||||
|
||||
-- NOT Condition OR ELSE Then_Expr
|
||||
|
||||
-- * in pre- and postconditions, where the Condition cannot have side-
|
||||
-- effects (in ALFA) and thus the expression is equivalent to
|
||||
|
||||
-- (Condition AND THEN Then_Expr)
|
||||
-- and (NOT Condition AND THEN Then_Expr)
|
||||
|
||||
-- Non-boolean conditional expressions are marked as not in ALFA during
|
||||
-- resolution.
|
||||
|
||||
if Present (Else_Expr) and then not In_Pre_Post_Expression then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("this form of conditional expression is not in ALFA", N);
|
||||
end if;
|
||||
|
||||
if Comes_From_Source (N) then
|
||||
Check_Compiler_Unit (N);
|
||||
end if;
|
||||
|
@ -1733,7 +1699,6 @@ package body Sem_Ch4 is
|
|||
-- Start of processing for Analyze_Explicit_Dereference
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("explicit dereference is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("explicit dereference is not allowed", N);
|
||||
|
||||
Analyze (P);
|
||||
|
@ -2616,7 +2581,6 @@ package body Sem_Ch4 is
|
|||
|
||||
procedure Analyze_Null (N : Node_Id) is
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("null is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("null is not allowed", N);
|
||||
|
||||
Set_Etype (N, Any_Access);
|
||||
|
@ -3248,8 +3212,6 @@ package body Sem_Ch4 is
|
|||
T : Entity_Id;
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("qualified expression is not in ALFA", N);
|
||||
|
||||
Analyze_Expression (Expr);
|
||||
|
||||
Set_Etype (N, Any_Type);
|
||||
|
@ -3308,7 +3270,6 @@ package body Sem_Ch4 is
|
|||
Iterator : Node_Id;
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("quantified expression is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("quantified expression is not allowed", N);
|
||||
|
||||
Set_Etype (Ent, Standard_Void_Type);
|
||||
|
@ -3474,8 +3435,6 @@ package body Sem_Ch4 is
|
|||
Acc_Type : Entity_Id;
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("reference is not in ALFA", N);
|
||||
|
||||
Analyze (P);
|
||||
|
||||
-- An interesting error check, if we take the 'Reference of an object
|
||||
|
@ -4340,7 +4299,6 @@ package body Sem_Ch4 is
|
|||
-- Start of processing for Analyze_Slice
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("slice is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("slice is not allowed", N);
|
||||
|
||||
Analyze (P);
|
||||
|
@ -4406,14 +4364,6 @@ package body Sem_Ch4 is
|
|||
Analyze_Expression (Expr);
|
||||
Validate_Remote_Type_Type_Conversion (N);
|
||||
|
||||
-- Type conversion between scalar types are allowed in ALFA. All other
|
||||
-- type conversions are not allowed.
|
||||
|
||||
if not (Is_Scalar_Type (Etype (Expr)) and then Is_Scalar_Type (T)) then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("only type conversion between scalar types is in ALFA", N);
|
||||
end if;
|
||||
|
||||
-- Only remaining step is validity checks on the argument. These
|
||||
-- are skipped if the conversion does not come from the source.
|
||||
|
||||
|
@ -4523,8 +4473,6 @@ package body Sem_Ch4 is
|
|||
|
||||
procedure Analyze_Unchecked_Type_Conversion (N : Node_Id) is
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("unchecked type conversion is not in ALFA", N);
|
||||
Find_Type (Subtype_Mark (N));
|
||||
Analyze_Expression (Expression (N));
|
||||
Set_Etype (N, Entity (Subtype_Mark (N)));
|
||||
|
|
|
@ -1113,8 +1113,6 @@ package body Sem_Ch5 is
|
|||
if Others_Present
|
||||
and then List_Length (Alternatives (N)) = 1
|
||||
then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("OTHERS as unique case alternative is not in ALFA", N);
|
||||
Check_SPARK_Restriction
|
||||
("OTHERS as unique case alternative is not allowed", N);
|
||||
end if;
|
||||
|
@ -1164,7 +1162,7 @@ package body Sem_Ch5 is
|
|||
-- loop. Otherwise there must be an innermost open loop on the stack, to
|
||||
-- which the statement implicitly refers.
|
||||
|
||||
-- Additionally, in formal mode:
|
||||
-- Additionally, in SPARK mode:
|
||||
|
||||
-- The exit can only name the closest enclosing loop;
|
||||
|
||||
|
@ -1196,9 +1194,6 @@ package body Sem_Ch5 is
|
|||
|
||||
else
|
||||
if Has_Loop_In_Inner_Open_Scopes (U_Name) then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("exit label must name the closest enclosing loop"
|
||||
& " in ALFA", N);
|
||||
Check_SPARK_Restriction
|
||||
("exit label must name the closest enclosing loop", N);
|
||||
end if;
|
||||
|
@ -1245,9 +1240,6 @@ package body Sem_Ch5 is
|
|||
|
||||
if Present (Cond) then
|
||||
if Nkind (Parent (N)) /= N_Loop_Statement then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("exit with when clause must be directly in loop"
|
||||
& " in ALFA", N);
|
||||
Check_SPARK_Restriction
|
||||
("exit with when clause must be directly in loop", N);
|
||||
end if;
|
||||
|
@ -1255,36 +1247,26 @@ package body Sem_Ch5 is
|
|||
else
|
||||
if Nkind (Parent (N)) /= N_If_Statement then
|
||||
if Nkind (Parent (N)) = N_Elsif_Part then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("exit must be in IF without ELSIF in ALFA", N);
|
||||
Check_SPARK_Restriction
|
||||
("exit must be in IF without ELSIF", N);
|
||||
else
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("exit must be directly in IF in ALFA", N);
|
||||
Check_SPARK_Restriction ("exit must be directly in IF", N);
|
||||
end if;
|
||||
|
||||
elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("exit must be in IF directly in loop in ALFA", N);
|
||||
Check_SPARK_Restriction
|
||||
("exit must be in IF directly in loop", N);
|
||||
|
||||
-- First test the presence of ELSE, so that an exit in an ELSE
|
||||
-- leads to an error mentioning the ELSE.
|
||||
-- First test the presence of ELSE, so that an exit in an ELSE leads
|
||||
-- to an error mentioning the ELSE.
|
||||
|
||||
elsif Present (Else_Statements (Parent (N))) then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("exit must be in IF without ELSE in ALFA", N);
|
||||
Check_SPARK_Restriction ("exit must be in IF without ELSE", N);
|
||||
|
||||
-- An exit in an ELSIF does not reach here, as it would have been
|
||||
-- detected in the case (Nkind (Parent (N)) /= N_If_Statement).
|
||||
-- An exit in an ELSIF does not reach here, as it would have been
|
||||
-- detected in the case (Nkind (Parent (N)) /= N_If_Statement).
|
||||
|
||||
elsif Present (Elsif_Parts (Parent (N))) then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("exit must be in IF without ELSIF in ALFA", N);
|
||||
Check_SPARK_Restriction ("exit must be in IF without ELSIF", N);
|
||||
end if;
|
||||
end if;
|
||||
|
@ -1313,7 +1295,6 @@ package body Sem_Ch5 is
|
|||
Label_Ent : Entity_Id;
|
||||
|
||||
begin
|
||||
Mark_Non_ALFA_Subprogram ("goto statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("goto statement is not allowed", N);
|
||||
|
||||
-- Actual semantic checks
|
||||
|
@ -2093,18 +2074,6 @@ package body Sem_Ch5 is
|
|||
Set_Etype (Id, Etype (DS));
|
||||
end if;
|
||||
|
||||
-- The entity for iterating over a loop is always in ALFA if
|
||||
-- its type is in ALFA, and it is not an iteration over
|
||||
-- elements of a container using the OF syntax.
|
||||
|
||||
if Is_In_ALFA (Etype (Id))
|
||||
and then
|
||||
(No (Iterator_Specification (N))
|
||||
or else not Of_Present (Iterator_Specification (N)))
|
||||
then
|
||||
Set_Is_In_ALFA (Id);
|
||||
end if;
|
||||
|
||||
-- Treat a range as an implicit reference to the type, to
|
||||
-- inhibit spurious warnings.
|
||||
|
||||
|
|
|
@ -664,21 +664,18 @@ package body Sem_Ch6 is
|
|||
Check_Limited_Return (Expr);
|
||||
end if;
|
||||
|
||||
-- RETURN only allowed in SPARK is as the last statement function
|
||||
-- RETURN only allowed in SPARK as the last statement in function
|
||||
|
||||
if Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements
|
||||
and then
|
||||
(Nkind (Parent (Parent (N))) /= N_Subprogram_Body
|
||||
or else Present (Next (N)))
|
||||
then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("RETURN should be the last statement in ALFA", N);
|
||||
Check_SPARK_Restriction
|
||||
("RETURN should be the last statement in function", N);
|
||||
end if;
|
||||
|
||||
else
|
||||
Mark_Non_ALFA_Subprogram ("extended RETURN is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("extended RETURN is not allowed", N);
|
||||
|
||||
-- Analyze parts specific to extended_return_statement:
|
||||
|
@ -1491,13 +1488,6 @@ package body Sem_Ch6 is
|
|||
Typ := Entity (Result_Definition (N));
|
||||
Set_Etype (Designator, Typ);
|
||||
|
||||
-- If the result type of a subprogram is not in ALFA, then the
|
||||
-- subprogram is not in ALFA.
|
||||
|
||||
if not Is_In_ALFA (Typ) then
|
||||
Set_Is_In_ALFA (Designator, False);
|
||||
end if;
|
||||
|
||||
-- Unconstrained array as result is not allowed in SPARK
|
||||
|
||||
if Is_Array_Type (Typ)
|
||||
|
@ -1932,11 +1922,11 @@ package body Sem_Ch6 is
|
|||
Check_Returns (HSS, 'P', Missing_Ret, Spec_Id);
|
||||
end if;
|
||||
|
||||
-- Special checks in formal mode
|
||||
-- Special checks in SPARK mode
|
||||
|
||||
if Nkind (Body_Spec) = N_Function_Specification then
|
||||
|
||||
-- In formal mode, last statement of a function should be a return
|
||||
-- In SPARK mode, last statement of a function should be a return
|
||||
|
||||
declare
|
||||
Stat : constant Node_Id := Last_Source_Statement (HSS);
|
||||
|
@ -1945,13 +1935,12 @@ package body Sem_Ch6 is
|
|||
and then not Nkind_In (Stat, N_Simple_Return_Statement,
|
||||
N_Extended_Return_Statement)
|
||||
then
|
||||
Set_Body_Is_In_ALFA (Id, False);
|
||||
Check_SPARK_Restriction
|
||||
("last statement in function should be RETURN", Stat);
|
||||
end if;
|
||||
end;
|
||||
|
||||
-- In formal mode, verify that a procedure has no return
|
||||
-- In SPARK mode, verify that a procedure has no return
|
||||
|
||||
elsif Nkind (Body_Spec) = N_Procedure_Specification then
|
||||
if Present (Spec_Id) then
|
||||
|
@ -1964,7 +1953,6 @@ package body Sem_Ch6 is
|
|||
-- borrow the Check_Returns procedure here ???
|
||||
|
||||
if Return_Present (Id) then
|
||||
Set_Body_Is_In_ALFA (Id, False);
|
||||
Check_SPARK_Restriction
|
||||
("procedure should not have RETURN", N);
|
||||
end if;
|
||||
|
@ -2282,24 +2270,6 @@ package body Sem_Ch6 is
|
|||
end if;
|
||||
end if;
|
||||
|
||||
-- By default, consider that the subprogram body is in ALFA if the spec
|
||||
-- is in ALFA. This is reversed later if some expression or statement is
|
||||
-- not in ALFA.
|
||||
|
||||
declare
|
||||
Id : Entity_Id;
|
||||
begin
|
||||
if Present (Spec_Id) then
|
||||
Id := Spec_Id;
|
||||
else
|
||||
Id := Body_Id;
|
||||
end if;
|
||||
|
||||
if Is_In_ALFA (Id) then
|
||||
Set_Body_Is_In_ALFA (Id);
|
||||
end if;
|
||||
end;
|
||||
|
||||
-- Do not inline any subprogram that contains nested subprograms, since
|
||||
-- the backend inlining circuit seems to generate uninitialized
|
||||
-- references in this case. We know this happens in the case of front
|
||||
|
@ -2531,7 +2501,6 @@ package body Sem_Ch6 is
|
|||
Set_Ekind (Body_Id, E_Subprogram_Body);
|
||||
Set_Scope (Body_Id, Scope (Spec_Id));
|
||||
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
|
||||
Set_Is_In_ALFA (Body_Id, False);
|
||||
|
||||
-- Case of subprogram body with no previous spec
|
||||
|
||||
|
@ -3177,11 +3146,6 @@ package body Sem_Ch6 is
|
|||
-- Start of processing for Analyze_Subprogram_Specification
|
||||
|
||||
begin
|
||||
-- By default, consider that the subprogram spec is in ALFA. This is
|
||||
-- reversed later if some parameter or result is not in ALFA.
|
||||
|
||||
Set_Is_In_ALFA (Designator);
|
||||
|
||||
-- User-defined operator is not allowed in SPARK, except as a renaming
|
||||
|
||||
if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
|
||||
|
@ -8905,14 +8869,6 @@ package body Sem_Ch6 is
|
|||
|
||||
Set_Etype (Formal, Formal_Type);
|
||||
|
||||
-- The parameter is in ALFA if-and-only-if its type is in ALFA
|
||||
|
||||
if Is_In_ALFA (Formal_Type) then
|
||||
Set_Is_In_ALFA (Formal);
|
||||
else
|
||||
Mark_Non_ALFA_Subprogram ("formal is not in ALFA", Formal);
|
||||
end if;
|
||||
|
||||
Default := Expression (Param_Spec);
|
||||
|
||||
if Present (Default) then
|
||||
|
|
|
@ -101,7 +101,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("abort statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("abort statement is not allowed", N);
|
||||
|
||||
T_Name := First (Names (N));
|
||||
|
@ -140,7 +139,6 @@ package body Sem_Ch9 is
|
|||
procedure Analyze_Accept_Alternative (N : Node_Id) is
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("accept is not in ALFA", N);
|
||||
|
||||
if Present (Pragmas_Before (N)) then
|
||||
Analyze_List (Pragmas_Before (N));
|
||||
|
@ -174,7 +172,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("accept statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("accept statement is not allowed", N);
|
||||
|
||||
-- Entry name is initialized to Any_Id. It should get reset to the
|
||||
|
@ -406,7 +403,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("select statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("select statement is not allowed", N);
|
||||
Check_Restriction (Max_Asynchronous_Select_Nesting, N);
|
||||
Check_Restriction (No_Select_Statements, N);
|
||||
|
@ -453,7 +449,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("select statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("select statement is not allowed", N);
|
||||
Check_Restriction (No_Select_Statements, N);
|
||||
|
||||
|
@ -500,7 +495,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("delay is not in ALFA", N);
|
||||
Check_Restriction (No_Delay, N);
|
||||
|
||||
if Present (Pragmas_Before (N)) then
|
||||
|
@ -552,7 +546,6 @@ package body Sem_Ch9 is
|
|||
E : constant Node_Id := Expression (N);
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("delay statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("delay statement is not allowed", N);
|
||||
Check_Restriction (No_Relative_Delay, N);
|
||||
Check_Restriction (No_Delay, N);
|
||||
|
@ -571,7 +564,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("delay statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("delay statement is not allowed", N);
|
||||
Check_Restriction (No_Delay, N);
|
||||
Check_Potentially_Blocking_Operation (N);
|
||||
|
@ -600,7 +592,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N);
|
||||
|
||||
-- Entry_Name is initialized to Any_Id. It should get reset to the
|
||||
-- matching entry entity. An error is signalled if it is not reset
|
||||
|
@ -833,7 +824,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N);
|
||||
|
||||
if Present (Index) then
|
||||
Analyze (Index);
|
||||
|
@ -861,7 +851,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("entry call is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("entry call is not allowed", N);
|
||||
|
||||
if Present (Pragmas_Before (N)) then
|
||||
|
@ -897,7 +886,6 @@ package body Sem_Ch9 is
|
|||
begin
|
||||
Generate_Definition (Def_Id);
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N);
|
||||
|
||||
-- Case of no discrete subtype definition
|
||||
|
||||
|
@ -967,7 +955,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("entry is not in ALFA", N);
|
||||
Analyze (Def);
|
||||
|
||||
-- There is no elaboration of the entry index specification. Therefore,
|
||||
|
@ -1009,7 +996,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("protected body is not in ALFA", N);
|
||||
Set_Ekind (Body_Id, E_Protected_Body);
|
||||
Spec_Id := Find_Concurrent_Spec (Body_Id);
|
||||
|
||||
|
@ -1128,7 +1114,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("protected definition is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("protected definition is not allowed", N);
|
||||
Analyze_Declarations (Visible_Declarations (N));
|
||||
|
||||
|
@ -1182,7 +1167,6 @@ package body Sem_Ch9 is
|
|||
end if;
|
||||
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("protected type is not in ALFA", N);
|
||||
Check_Restriction (No_Protected_Types, N);
|
||||
|
||||
T := Find_Type_Name (N);
|
||||
|
@ -1324,7 +1308,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("requeue statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("requeue statement is not allowed", N);
|
||||
Check_Restriction (No_Requeue_Statements, N);
|
||||
Check_Unreachable_Code (N);
|
||||
|
@ -1599,7 +1582,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("select statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("select statement is not allowed", N);
|
||||
Check_Restriction (No_Select_Statements, N);
|
||||
|
||||
|
@ -1720,7 +1702,6 @@ package body Sem_Ch9 is
|
|||
begin
|
||||
Generate_Definition (Id);
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("protected object is not in ALFA", N);
|
||||
|
||||
-- The node is rewritten as a protected type declaration, in exact
|
||||
-- analogy with what is done with single tasks.
|
||||
|
@ -1782,7 +1763,6 @@ package body Sem_Ch9 is
|
|||
begin
|
||||
Generate_Definition (Id);
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("task is not in ALFA", N);
|
||||
|
||||
-- The node is rewritten as a task type declaration, followed by an
|
||||
-- object declaration of that anonymous task type.
|
||||
|
@ -1860,7 +1840,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("task body is not in ALFA", N);
|
||||
Set_Ekind (Body_Id, E_Task_Body);
|
||||
Set_Scope (Body_Id, Current_Scope);
|
||||
Spec_Id := Find_Concurrent_Spec (Body_Id);
|
||||
|
@ -1981,7 +1960,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("task definition is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("task definition is not allowed", N);
|
||||
|
||||
if Present (Visible_Declarations (N)) then
|
||||
|
@ -2016,7 +1994,6 @@ package body Sem_Ch9 is
|
|||
begin
|
||||
Check_Restriction (No_Tasking, N);
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("task type is not in ALFA", N);
|
||||
T := Find_Type_Name (N);
|
||||
Generate_Definition (T);
|
||||
|
||||
|
@ -2122,7 +2099,6 @@ package body Sem_Ch9 is
|
|||
procedure Analyze_Terminate_Alternative (N : Node_Id) is
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("terminate is not in ALFA", N);
|
||||
|
||||
if Present (Pragmas_Before (N)) then
|
||||
Analyze_List (Pragmas_Before (N));
|
||||
|
@ -2144,7 +2120,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("select statement is not in ALFA", N);
|
||||
Check_SPARK_Restriction ("select statement is not allowed", N);
|
||||
Check_Restriction (No_Select_Statements, N);
|
||||
|
||||
|
@ -2181,7 +2156,6 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Mark_Non_ALFA_Subprogram ("triggering statement is not in ALFA", N);
|
||||
|
||||
if Present (Pragmas_Before (N)) then
|
||||
Analyze_List (Pragmas_Before (N));
|
||||
|
|
|
@ -6090,18 +6090,6 @@ package body Sem_Prag is
|
|||
-- external tool and a tool-specific function. These arguments are
|
||||
-- not analyzed.
|
||||
|
||||
-- The following is a special form used in conjunction with the
|
||||
-- ALFA subset of Ada:
|
||||
|
||||
-- pragma Annotate (Formal_Proof, MODE);
|
||||
-- MODE ::= On | Off
|
||||
|
||||
-- This pragma either forces (mode On) or disables (mode Off)
|
||||
-- formal verification of the subprogram in which it is added. When
|
||||
-- formal verification is forced, all violations of the the ALFA
|
||||
-- subset of Ada present in the subprogram are reported as errors
|
||||
-- to the user.
|
||||
|
||||
when Pragma_Annotate => Annotate : declare
|
||||
Arg : Node_Id;
|
||||
Exp : Node_Id;
|
||||
|
@ -6113,52 +6101,9 @@ package body Sem_Prag is
|
|||
Check_No_Identifiers;
|
||||
Store_Note (N);
|
||||
|
||||
-- Special processing for Formal_Proof case
|
||||
|
||||
if Chars (Get_Pragma_Arg (Arg1)) = Name_Formal_Proof then
|
||||
if No (Arg2) then
|
||||
Error_Pragma_Arg
|
||||
("missing second argument for pragma%", Arg1);
|
||||
end if;
|
||||
|
||||
Check_Arg_Count (2);
|
||||
Check_Arg_Is_One_Of (Arg2, Name_On, Name_Off);
|
||||
|
||||
declare
|
||||
Cur_Subp : constant Entity_Id := Current_Subprogram;
|
||||
|
||||
begin
|
||||
if Present (Cur_Subp)
|
||||
and then (Is_Subprogram (Cur_Subp)
|
||||
or else Is_Generic_Subprogram (Cur_Subp))
|
||||
then
|
||||
-- Notify user if some ALFA violation occurred before
|
||||
-- this point in Cur_Subp. These violations are not
|
||||
-- precisly located, but this is better than ignoring
|
||||
-- these violations.
|
||||
|
||||
if Chars (Get_Pragma_Arg (Arg2)) = Name_On
|
||||
and then (not Is_In_ALFA (Cur_Subp)
|
||||
or else not Body_Is_In_ALFA (Cur_Subp))
|
||||
then
|
||||
Error_Pragma
|
||||
("pragma% is placed after violation"
|
||||
& " of ALFA");
|
||||
end if;
|
||||
|
||||
-- We treat this as a Rep_Item to record it on the rep
|
||||
-- item chain for easy location later on.
|
||||
|
||||
Record_Rep_Item (Cur_Subp, N);
|
||||
|
||||
else
|
||||
Error_Pragma ("wrong placement for pragma%");
|
||||
end if;
|
||||
end;
|
||||
|
||||
-- Second parameter is optional, it is never analyzed
|
||||
|
||||
elsif No (Arg2) then
|
||||
if No (Arg2) then
|
||||
null;
|
||||
|
||||
-- Here if we have a second parameter
|
||||
|
|
|
@ -5817,23 +5817,14 @@ package body Sem_Res is
|
|||
-- types or array types except String.
|
||||
|
||||
if Is_Boolean_Type (T) then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("ordering operator on boolean type is not in ALFA", N);
|
||||
Check_SPARK_Restriction
|
||||
("comparison is not defined on Boolean type", N);
|
||||
|
||||
elsif Is_Array_Type (T) then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("ordering operator on array type is not in ALFA", N);
|
||||
|
||||
if Base_Type (T) /= Standard_String then
|
||||
Check_SPARK_Restriction
|
||||
("comparison is not defined on array types other than String",
|
||||
N);
|
||||
end if;
|
||||
|
||||
else
|
||||
null;
|
||||
elsif Is_Array_Type (T)
|
||||
and then Base_Type (T) /= Standard_String
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
("comparison is not defined on array types other than String", N);
|
||||
end if;
|
||||
|
||||
-- Check comparison on unordered enumeration
|
||||
|
@ -5883,11 +5874,6 @@ package body Sem_Res is
|
|||
Append_To (Expressions (N), Error);
|
||||
end if;
|
||||
|
||||
if Root_Type (Typ) /= Standard_Boolean then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("non-boolean conditional expression is not in ALFA", N);
|
||||
end if;
|
||||
|
||||
Set_Etype (N, Typ);
|
||||
Eval_Conditional_Expression (N);
|
||||
end Resolve_Conditional_Expression;
|
||||
|
@ -6688,9 +6674,6 @@ package body Sem_Res is
|
|||
-- operands have equal static bounds.
|
||||
|
||||
if Is_Array_Type (T) then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("equality operator on array is not in ALFA", N);
|
||||
|
||||
-- Protect call to Matching_Static_Array_Bounds to avoid costly
|
||||
-- operation if not needed.
|
||||
|
||||
|
@ -7262,9 +7245,6 @@ package body Sem_Res is
|
|||
if Is_Array_Type (B_Typ)
|
||||
and then Nkind (N) in N_Binary_Op
|
||||
then
|
||||
Mark_Non_ALFA_Subprogram
|
||||
("binary operator on array is not in ALFA", N);
|
||||
|
||||
declare
|
||||
Left_Typ : constant Node_Id := Etype (Left_Opnd (N));
|
||||
Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
|
||||
|
|
|
@ -141,14 +141,6 @@ package body Sem_Util is
|
|||
-- T is a derived tagged type. Check whether the type extension is null.
|
||||
-- If the parent type is fully initialized, T can be treated as such.
|
||||
|
||||
procedure Mark_Non_ALFA_Subprogram_Unconditional
|
||||
(Msg : String;
|
||||
N : Node_Id);
|
||||
-- Perform the action for Mark_Non_ALFA_Subprogram_Body, which allows the
|
||||
-- latter to be small and inlined. If the subprogram being marked as not in
|
||||
-- ALFA is annotated with Formal_Proof being On, then an error is issued
|
||||
-- with message Msg on node N.
|
||||
|
||||
------------------------------
|
||||
-- Abstract_Interface_List --
|
||||
------------------------------
|
||||
|
@ -2323,60 +2315,6 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Current_Subprogram;
|
||||
|
||||
------------------------------
|
||||
-- Mark_Non_ALFA_Subprogram --
|
||||
------------------------------
|
||||
|
||||
procedure Mark_Non_ALFA_Subprogram (Msg : String; N : Node_Id) is
|
||||
begin
|
||||
-- Isolate marking of the current subprogram body so that the body of
|
||||
-- Mark_Non_ALFA_Subprogram is small and inlined.
|
||||
|
||||
if ALFA_Mode then
|
||||
Mark_Non_ALFA_Subprogram_Unconditional (Msg, N);
|
||||
end if;
|
||||
end Mark_Non_ALFA_Subprogram;
|
||||
|
||||
--------------------------------------------
|
||||
-- Mark_Non_ALFA_Subprogram_Unconditional --
|
||||
--------------------------------------------
|
||||
|
||||
procedure Mark_Non_ALFA_Subprogram_Unconditional
|
||||
(Msg : String;
|
||||
N : Node_Id)
|
||||
is
|
||||
Cur_Subp : constant Entity_Id := Current_Subprogram;
|
||||
|
||||
begin
|
||||
if Present (Cur_Subp)
|
||||
and then (Is_Subprogram (Cur_Subp)
|
||||
or else Is_Generic_Subprogram (Cur_Subp))
|
||||
then
|
||||
-- If the subprogram has been annotated with Formal_Proof being On,
|
||||
-- then an error must be issued to notify the user that this
|
||||
-- subprogram unexpectedly falls outside the ALFA subset.
|
||||
|
||||
if Formal_Proof_On (Cur_Subp) then
|
||||
Error_Msg_F (Msg, N);
|
||||
end if;
|
||||
|
||||
-- If the non-ALFA construct is in a precondition or postcondition,
|
||||
-- then mark the subprogram as not in ALFA, because neither the
|
||||
-- subprogram nor its callers can be proved formally.
|
||||
|
||||
-- If the non-ALFA construct is in a regular piece of code inside the
|
||||
-- body of the subprogram, then mark the subprogram body as not in
|
||||
-- ALFA, because the subprogram cannot be proved formally, but its
|
||||
-- callers could.
|
||||
|
||||
if In_Pre_Post_Expression then
|
||||
Set_Is_In_ALFA (Cur_Subp, False);
|
||||
else
|
||||
Set_Body_Is_In_ALFA (Cur_Subp, False);
|
||||
end if;
|
||||
end if;
|
||||
end Mark_Non_ALFA_Subprogram_Unconditional;
|
||||
|
||||
---------------------
|
||||
-- Defining_Entity --
|
||||
---------------------
|
||||
|
|
|
@ -277,22 +277,6 @@ package Sem_Util is
|
|||
-- Current_Scope is returned. The returned value is Empty if this is called
|
||||
-- from a library package which is not within any subprogram.
|
||||
|
||||
procedure Mark_Non_ALFA_Subprogram (Msg : String; N : Node_Id);
|
||||
-- If Current_Subprogram is not Empty, mark either its specification or its
|
||||
-- body as not being in ALFA.
|
||||
|
||||
-- This procedure may be called during the analysis of a precondition or
|
||||
-- postcondition, as indicated by the flag In_Pre_Post_Expression, or
|
||||
-- during the analysis of a subprogram's body. In the first case, the
|
||||
-- specification of Current_Subprogram must be marked as not being in ALFA,
|
||||
-- as the contract is considered to be part of the specification, so that
|
||||
-- calls to this subprogram are not in ALFA. In the second case, mark the
|
||||
-- body as not being in ALFA, which does not prevent the subprogram's
|
||||
-- specification, and calls to the subprogram, from being in ALFA.
|
||||
|
||||
-- If the subprogram being marked as not in ALFA is annotated with
|
||||
-- Formal_Proof On, then an error is issued with message Msg on node N.
|
||||
|
||||
function Defining_Entity (N : Node_Id) return Entity_Id;
|
||||
-- Given a declaration N, returns the associated defining entity. If the
|
||||
-- declaration has a specification, the entity is obtained from the
|
||||
|
|
|
@ -313,35 +313,6 @@ package Stand is
|
|||
Boolean_Literals : array (Boolean) of Entity_Id;
|
||||
-- Entities for the two boolean literals, used by the expander
|
||||
|
||||
-- Standard types which are in ALFA are associated set to True
|
||||
|
||||
Standard_Type_Is_In_ALFA : array (S_Types) of Boolean :=
|
||||
(S_Boolean => True,
|
||||
|
||||
S_Short_Short_Integer => True,
|
||||
S_Short_Integer => True,
|
||||
S_Integer => True,
|
||||
S_Long_Integer => True,
|
||||
S_Long_Long_Integer => True,
|
||||
|
||||
S_Natural => True,
|
||||
S_Positive => True,
|
||||
|
||||
S_Short_Float => False,
|
||||
S_Float => False,
|
||||
S_Long_Float => False,
|
||||
S_Long_Long_Float => False,
|
||||
|
||||
S_Character => False,
|
||||
S_Wide_Character => False,
|
||||
S_Wide_Wide_Character => False,
|
||||
|
||||
S_String => False,
|
||||
S_Wide_String => False,
|
||||
S_Wide_Wide_String => False,
|
||||
|
||||
S_Duration => False);
|
||||
|
||||
-------------------------------------
|
||||
-- Semantic Phase Special Entities --
|
||||
-------------------------------------
|
||||
|
|
Loading…
Reference in New Issue