+2011-08-02 Yannick Moy <moy@adacore.com>
+
+ * cstand.adb (Create_Standard): sets Is_In_ALFA component of standard
+ types.
+ * einfo.adb, einfo.ads (Is_In_ALFA): add flag for all entities
+ (Is_In_ALFA, Set_Is_In_ALFA): new subprograms to access flag Is_In_ALFA
+ * sem_ch3.adb
+ (Analyze_Object_Declaration): set Is_In_ALFA flag for objects
+ (Constrain_Enumeration): set Is_In_ALFA flag for enumeration subtypes
+ (Constrain_Integer): set Is_In_ALFA flag for integer subtypes
+ (Enumeration_Type_Declaration): set Is_In_ALFA flag for enumeration
+ types.
+ (Set_Scalar_Range_For_Subtype): unset Is_In_ALFA flag for subtypes with
+ non-static range.
+ * sem_ch6.adb (Analyze_Return_Type): unset Is_In_ALFA flag for
+ functions whose return type is not in ALFA.
+ (Analyze_Subprogram_Specification): set Is_In_ALFA flag for subprogram
+ specifications.
+ (Process_Formals): unset Is_In_ALFA flag for subprograms if a
+ parameter's type is not in ALFA.
+ * stand.ads (Standard_Type_Is_In_ALFA): array defines which standard
+ types are in ALFA.
+
2011-08-02 Ed Schonberg <schonberg@adacore.com>
* sem_ch6 (Analyze_Expression_Function): treat the function as
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT 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- --
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));
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT 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- --
-- Is_Compilation_Unit Flag149
-- Has_Pragma_Elaborate_Body Flag150
+ -- Is_In_ALFA Flag151
-- Entry_Accepted Flag152
-- Is_Obsolescent Flag153
-- Has_Per_Object_Constraint Flag154
-- Is_Safe_To_Reevaluate Flag249
-- Has_Predicates Flag250
- -- (unused) Flag151
-- (unused) Flag251
-- (unused) Flag252
-- (unused) Flag253
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);
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);
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));
-- 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.
+
-- Is_Inlined (Flag11)
-- Present in all entities. Set for functions and procedures which are
-- to be inlined. For subprograms created during expansion, this flag
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;
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);
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);
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);
Act_T := T;
+ -- The object is in ALFA if-and-only-if its type is in ALFA
+
+ if Is_In_ALFA (T) then
+ 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.
if Skip
or else (Present (Etype (Id))
- and then (Is_Private_Type (Etype (Id))
- or else Is_Task_Type (Etype (Id))
- or else Is_Rewrite_Substitution (N)))
+ and then (Is_Private_Type (Etype (Id))
+ or else Is_Task_Type (Etype (Id))
+ or else Is_Rewrite_Substitution (N)))
then
null;
if Has_Predicates (T)
or else (Present (Ancestor_Subtype (T))
- and then Has_Predicates (Ancestor_Subtype (T)))
+ and then Has_Predicates (Ancestor_Subtype (T)))
then
Set_Has_Predicates (Id);
Set_Has_Delayed_Freeze (Id);
begin
-- Set common attributes
- Set_Scope (Derived_Type, Current_Scope);
+ Set_Scope (Derived_Type, Current_Scope);
- Set_Ekind (Derived_Type, Ekind (Parent_Base));
- Set_Etype (Derived_Type, Parent_Base);
- Set_Has_Task (Derived_Type, Has_Task (Parent_Base));
+ Set_Ekind (Derived_Type, Ekind (Parent_Base));
+ Set_Etype (Derived_Type, Parent_Base);
+ Set_Has_Task (Derived_Type, Has_Task (Parent_Base));
Set_Size_Info (Derived_Type, Parent_Type);
Set_RM_Size (Derived_Type, RM_Size (Parent_Type));
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 Nkind (Original_Node (Parent (Def_Id))) = N_Subtype_Declaration
+ and then 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)));
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 Nkind (Original_Node (Parent (Def_Id))) = N_Subtype_Declaration
+ and then 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
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
if Nkind (R) = N_Range then
- -- In SPARK/ALFA, all ranges should be static, with the exception of
- -- the discrete type definition of a loop parameter specification.
+ -- In SPARK, all ranges should be static, with the exception of the
+ -- discrete type definition of a loop parameter specification.
if not In_Iter_Schm
and then not Is_Static_Range (R)
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;
--------------------------------------------------------
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;
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 or ALFA
if Is_Array_Type (Typ)
-- 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 or ALFA, except as
-- a renaming.
begin
return Is_Class_Wide_Type (Designated_Type (Etype (D)))
or else (Nkind (D) = N_Attribute_Reference
- and then Attribute_Name (D) = Name_Access
- and then Is_Class_Wide_Type (Etype (Prefix (D))));
+ and then Attribute_Name (D) = Name_Access
+ and then Is_Class_Wide_Type (Etype (Prefix (D))));
end Is_Class_Wide_Default;
-- Start of processing for Process_Formals
end if;
Set_Etype (Formal, Formal_Type);
+
+ -- If the type of a subprogram's formal parameter is not in ALFA,
+ -- then the subprogram is not in ALFA.
+
+ if Nkind (Parent (First (T))) in N_Subprogram_Specification
+ and then not Is_In_ALFA (Formal_Type)
+ then
+ Set_Is_In_ALFA (Defining_Entity (Parent (First (T))), False);
+ end if;
+
Default := Expression (Param_Spec);
if Present (Default) then
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT 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- --
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 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 --
-------------------------------------
OSDN Git Service
