+2010-10-19 Geert Bosch <bosch@adacore.com>
+
+ * ttypef.ads: Change VAXDF_Last to be -VAXDF_First, as type is
+ symmetric.
+
+2010-10-19 Robert Dewar <dewar@adacore.com>
+
+ * atree.h (Field29): Fix incorrect definition.
+ * einfo.adb (Invariant_Procedure): New attribute
+ (Has_Invariants): New flag
+ (Has_Inheritable_Invariants): New flag
+ (OK_To_Reference): New flag
+ Minor code reorganization (use Next_Rep_Item function)
+ * einfo.ads (Invariant_Procedure): New attribute
+ (Has_Invariants): New flag
+ (Has_Inheritable_Invariants): New flag
+ (OK_To_Reference): New flag
+ * exp_ch3.adb (Expand_N_Object_Declaration): Add check for invariant
+ * exp_ch4.adb (Expand_N_Type_Conversion): Check invariant on type
+ conversion. Minor reformatting.
+ * exp_util.ads, exp_util.adb (Make_Invariant_Call): New procedure.
+ * opt.ads (List_Inherited_Aspects): New name for List_Inherited_Pre_Post
+ * par-prag.adb: Add dummy entry for pragma Invariant.
+ * sem_ch13.adb (Build_Invariant_Procedure): New procedure
+ (Analyze_Aspect_Specification): Add support for Invariant aspect
+ * sem_ch13.ads (Build_Invariant_Procedure): New procedure
+ * sem_ch3.adb (Build_Derived_Type): Propagate invariant information
+ (Process_Full_View): Deal with invariants, building invariant procedure
+ Minor reformatting
+ * sem_ch6.adb (Process_PPCs): Add processing of invariants
+ * sem_ch7.adb (Analyze_Package_Specification): Build invariant
+ procedures.
+ * sem_prag.adb: Implement pragma Invariant.
+ * sem_res.adb (Resolve_Entity_Name): Allow type reference if
+ OK_To_Reference set.
+ * sem_warn.adb (List_Inherited_Aspects): New name for
+ List_Inherited_Pre_Post.
+ * snames.ads-tmpl: Add entries for pragma Invariant.
+ * treepr.adb (Print_Entity_Information): Add handling of Field29.
+ * usage.adb: Warning .l/.L applies to invariant as well as pre/post.
+
2010-10-19 Javier Miranda <miranda@adacore.com>
* par-ch4.adb: Update documentation of Ada 2012 syntax rules for
#define Field26(N) (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.field8)
#define Field27(N) (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.field9)
#define Field28(N) (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.field10)
-#define Field29(N) (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.field11)
+#define Field29(N) (Nodes_Ptr[(N) - First_Node_Id + 4].V.EX.X.field11)
#define Node1(N) Field1 (N)
#define Node2(N) Field2 (N)
-- Extra_Formals Node28
-- Underlying_Record_View Node28
- -- (unused) Node29
+ -- Invariant_Procedure Node29
---------------------------------------------
-- Usage of Flags in Defining Entity Nodes --
-- sense for them to be set true for certain subsets of entity kinds. See
-- the spec of Einfo for further details.
- -- Note: Flag1-Flag2 are absent from this list, for historical reasons
+ -- Note: Flag1-Flag3 are absent from this list, for historical reasons
-- Is_Frozen Flag4
-- Has_Discriminants Flag5
-- Has_Pragma_Inline_Always Flag230
-- Renamed_In_Spec Flag231
+ -- Has_Invariants Flag232
-- Has_Pragma_Unmodified Flag233
-- Is_Dispatch_Table_Entity Flag234
-- Is_Trivial_Subprogram Flag235
-- Is_Private_Primitive Flag245
-- Is_Underlying_Record_View Flag246
-- OK_To_Rename Flag247
+ -- Has_Inheritable_Invariants Flag248
+ -- OK_To_Reference Flag249
- -- (unused) Flag232
- -- (unused) Flag248
- -- (unused) Flag249
-- (unused) Flag250
-- (unused) Flag251
-- (unused) Flag252
then
return Ritem;
else
- Ritem := Next_Rep_Item (Ritem);
+ Next_Rep_Item (Ritem);
end if;
end loop;
return Flag56 (Id);
end Has_Homonym;
+ function Has_Inheritable_Invariants (Id : E) return B is
+ begin
+ pragma Assert (Is_Type (Id));
+ return Flag248 (Id);
+ end Has_Inheritable_Invariants;
+
function Has_Initial_Value (Id : E) return B is
begin
- pragma Assert
- (Ekind (Id) = E_Variable or else Is_Formal (Id));
+ pragma Assert (Ekind (Id) = E_Variable or else Is_Formal (Id));
return Flag219 (Id);
end Has_Initial_Value;
+ function Has_Invariants (Id : E) return B is
+ begin
+ pragma Assert (Is_Type (Id));
+ return Flag232 (Id);
+ end Has_Invariants;
+
function Has_Machine_Radix_Clause (Id : E) return B is
begin
pragma Assert (Is_Decimal_Fixed_Point_Type (Id));
return Elist25 (Id);
end Interfaces;
+ function Invariant_Procedure (Id : E) return N is
+ begin
+ pragma Assert (Is_Type (Id));
+ return Node29 (Id);
+ end Invariant_Procedure;
+
function In_Package_Body (Id : E) return B is
begin
return Flag48 (Id);
return Uint10 (Id);
end Normalized_Position_Max;
+ function OK_To_Reference (Id : E) return B is
+ begin
+ pragma Assert (Is_Type (Id));
+ return Flag249 (Id);
+ end OK_To_Reference;
+
function OK_To_Rename (Id : E) return B is
begin
pragma Assert (Ekind (Id) = E_Variable);
Set_Flag56 (Id, V);
end Set_Has_Homonym;
+ procedure Set_Has_Inheritable_Invariants (Id : E; V : B := True) is
+ begin
+ pragma Assert (Is_Type (Id));
+ Set_Flag248 (Id, V);
+ end Set_Has_Inheritable_Invariants;
+
procedure Set_Has_Initial_Value (Id : E; V : B := True) is
begin
pragma Assert (Ekind_In (Id, E_Variable, E_Out_Parameter));
Set_Flag219 (Id, V);
end Set_Has_Initial_Value;
+ procedure Set_Has_Invariants (Id : E; V : B := True) is
+ begin
+ pragma Assert (Is_Type (Id));
+ Set_Flag232 (Id, V);
+ end Set_Has_Invariants;
+
procedure Set_Has_Machine_Radix_Clause (Id : E; V : B := True) is
begin
pragma Assert (Is_Decimal_Fixed_Point_Type (Id));
Set_Elist25 (Id, V);
end Set_Interfaces;
+ procedure Set_Invariant_Procedure (Id : E; V : N) is
+ begin
+ pragma Assert (Is_Type (Id));
+ Set_Node29 (Id, V);
+ end Set_Invariant_Procedure;
+
procedure Set_In_Package_Body (Id : E; V : B := True) is
begin
Set_Flag48 (Id, V);
Set_Uint10 (Id, V);
end Set_Normalized_Position_Max;
+ procedure Set_OK_To_Reference (Id : E; V : B := True) is
+ begin
+ pragma Assert (Is_Type (Id));
+ Set_Flag249 (Id, V);
+ end Set_OK_To_Reference;
+
procedure Set_OK_To_Rename (Id : E; V : B := True) is
begin
pragma Assert (Ekind (Id) = E_Variable);
then
return True;
else
- Ritem := Next_Rep_Item (Ritem);
+ Next_Rep_Item (Ritem);
end if;
end loop;
then
return True;
else
- Ritem := Next_Rep_Item (Ritem);
+ Next_Rep_Item (Ritem);
end if;
end loop;
W ("Has_Fully_Qualified_Name", Flag173 (Id));
W ("Has_Gigi_Rep_Item", Flag82 (Id));
W ("Has_Homonym", Flag56 (Id));
+ W ("Has_Inheritable_Invariants", Flag248 (Id));
W ("Has_Initial_Value", Flag219 (Id));
+ W ("Has_Invariants", Flag232 (Id));
W ("Has_Machine_Radix_Clause", Flag83 (Id));
W ("Has_Master_Entity", Flag21 (Id));
W ("Has_Missing_Return", Flag142 (Id));
W ("No_Strict_Aliasing", Flag136 (Id));
W ("Non_Binary_Modulus", Flag58 (Id));
W ("Nonzero_Is_True", Flag162 (Id));
+ W ("OK_To_Reference", Flag249 (Id));
W ("OK_To_Rename", Flag247 (Id));
W ("OK_To_Reorder_Components", Flag239 (Id));
W ("Optimize_Alignment_Space", Flag241 (Id));
when E_Procedure |
E_Function =>
-
if Is_Dispatching_Operation (Id) then
Write_Str ("Overridden_Operation");
else
procedure Write_Field28_Name (Id : Entity_Id) is
begin
case Ekind (Id) is
+ when Private_Kind =>
+ Write_Str ("Invariant_Procedure");
+
when E_Procedure | E_Function | E_Entry =>
Write_Str ("Extra_Formals");
end case;
end Write_Field28_Name;
+ procedure Write_Field29_Name (Id : Entity_Id) is
+ begin
+ case Ekind (Id) is
+ when Type_Kind =>
+ Write_Str ("Invariant_Procedure");
+
+ when others =>
+ Write_Str ("Field29??");
+ end case;
+ end Write_Field29_Name;
+
-------------------------
-- Iterator Procedures --
-------------------------
-- which can never have a null value. This is set True for constant
-- access values initialized to a non-null value. This is also True for
-- all access parameters in Ada 83 and Ada 95 modes, and for access
--- parameters that explicily exlude null in Ada 2005.
+-- parameters that explicily exclude null in Ada 2005.
--
-- This is used to avoid unnecessary resetting of the Is_Known_Non_Null
-- flag for such entities. In Ada 2005 mode, this is also used when
-- definition contains at least one procedure to which a pragma
-- Interrupt_Handler applies.
+-- Has_Invariants (Flag232)
+-- Present in all type entities. Set True in private types if an
+-- Invariant or Invariant'Class aspect applies to the type, or if the
+-- type inherits one or more Invariant'Class aspects. Also set in the
+-- corresponding full type. Note: if this flag is set True, then usually
+-- the Invariant_Procedure field is set once the type is frozen, however
+-- this may not be true in some error situations. Note that it might be
+-- the full type which has inheritable invariants, and then the flag will
+-- also be set in the private type.
+
+-- Has_Inheritable_Invariants (Flag248)
+-- Present in all type entities. Set True in private types from which one
+-- or more Invariant'Class aspects will be inherited if a another type is
+-- derived from the type (i.e. those types which have an Invariant'Class
+-- aspect, or which inherit one or more Invariant'Class aspects). Also
+-- set in the corresponding full types. Note that it might be the full
+-- type which has inheritable invariants, and in this case the flag will
+-- also be set in the private type.
+
-- Has_Machine_Radix_Clause (Flag83)
-- Present in decimal types and subtypes, set if a Machine_Radix
-- representation clause is present. This flag is used to detect
-- representation clause, and thus is not inherited by a derived type.
-- This flag is always False for non-record types.
--- Has_Specified_Stream_Input (Flag190)
+-- Has_Specified_Stream_Input (Flag190)
-- Has_Specified_Stream_Output (Flag191)
--- Has_Specified_Stream_Read (Flag192)
--- Has_Specified_Stream_Write (Flag193)
+-- Has_Specified_Stream_Read (Flag192)
+-- Has_Specified_Stream_Write (Flag193)
-- Present in all type and subtype entities. Set for a given view if the
-- corresponding stream-oriented attribute has been defined by an
-- attribute definition clause. When such a clause occurs, a TSS is set
-- External_Name of the imported Java field (which is generally needed,
-- because Java names are case sensitive).
+-- Invariant_Procedure (Node29)
+-- Present in types and subtypes. Set for private types if one or more
+-- Invariant, or Invariant'Class, or inherited Invariant'Class aspects
+-- apply to the type. Points to the entity for a procedure which checks
+-- the invariant. This invariant procedure takes a single argument of the
+-- given type, and returns if the invariant holds, or raises exception
+-- Assertion_Error with an appropriate message if it does not hold. This
+-- field is present but always empty for private subtypes. This field is
+-- also set for the corresponding full type.
+
-- In_Use (Flag8)
-- Present in packages and types. Set when analyzing a use clause for
-- the corresponding entity. Reset at end of corresponding declarative
-- Applies to subprograms and subprogram types. Yields the number of
-- formals as a value of type Pos.
+-- OK_To_Reference (Flag249)
+-- Present in all entities for types and subtypes. If set it indicates
+-- that a naked reference to the type is permitted within an expression
+-- that is being analyzed or preanalyed (for example, a type name may
+-- be referenced within the Invariant aspect expression for the type).
+
-- OK_To_Rename (Flag247)
-- Present only in entities for variables. If this flag is set, it
-- means that if the entity is used as the initial value of an object
-- Alignment (Uint14)
-- Related_Expression (Node24)
-- Current_Use_Clause (Node27)
+ -- Invariant_Procedure (Node29)
-- Depends_On_Private (Flag14)
-- Discard_Names (Flag88)
-- Has_Complex_Representation (Flag140) (base type only)
-- Has_Constrained_Partial_View (Flag187)
-- Has_Discriminants (Flag5)
+ -- Has_Inheritable_Invariants (Flag248)
+ -- Has_Invariants (Flag232)
-- Has_Non_Standard_Rep (Flag75) (base type only)
-- Has_Object_Size_Clause (Flag172)
-- Has_Pragma_Preelab_Init (Flag221)
-- Known_To_Have_Preelab_Init (Flag207)
-- Must_Be_On_Byte_Boundary (Flag183)
-- Must_Have_Preelab_Init (Flag208)
+ -- OK_To_Reference (Flag249)
-- Optimize_Alignment_Space (Flag241)
-- Optimize_Alignment_Time (Flag242)
-- Size_Depends_On_Discriminant (Flag177)
function Has_Fully_Qualified_Name (Id : E) return B;
function Has_Gigi_Rep_Item (Id : E) return B;
function Has_Homonym (Id : E) return B;
+ function Has_Inheritable_Invariants (Id : E) return B;
function Has_Initial_Value (Id : E) return B;
+ function Has_Invariants (Id : E) return B;
function Has_Interrupt_Handler (Id : E) return B;
function Has_Machine_Radix_Clause (Id : E) return B;
function Has_Master_Entity (Id : E) return B;
function Interface_Alias (Id : E) return E;
function Interfaces (Id : E) return L;
function Interface_Name (Id : E) return N;
+ function Invariant_Procedure (Id : E) return N;
function Is_AST_Entry (Id : E) return B;
function Is_Abstract_Subprogram (Id : E) return B;
function Is_Abstract_Type (Id : E) return B;
function Normalized_First_Bit (Id : E) return U;
function Normalized_Position (Id : E) return U;
function Normalized_Position_Max (Id : E) return U;
+ function OK_To_Reference (Id : E) return B;
function OK_To_Rename (Id : E) return B;
function OK_To_Reorder_Components (Id : E) return B;
function Optimize_Alignment_Space (Id : E) return B;
procedure Set_Has_Fully_Qualified_Name (Id : E; V : B := True);
procedure Set_Has_Gigi_Rep_Item (Id : E; V : B := True);
procedure Set_Has_Homonym (Id : E; V : B := True);
+ procedure Set_Has_Inheritable_Invariants (Id : E; V : B := True);
procedure Set_Has_Initial_Value (Id : E; V : B := True);
+ procedure Set_Has_Invariants (Id : E; V : B := True);
procedure Set_Has_Machine_Radix_Clause (Id : E; V : B := True);
procedure Set_Has_Master_Entity (Id : E; V : B := True);
procedure Set_Has_Missing_Return (Id : E; V : B := True);
procedure Set_Inner_Instances (Id : E; V : L);
procedure Set_Interface_Alias (Id : E; V : E);
procedure Set_Interface_Name (Id : E; V : N);
+ procedure Set_Invariant_Procedure (Id : E; V : N);
procedure Set_Is_AST_Entry (Id : E; V : B := True);
procedure Set_Is_Abstract_Subprogram (Id : E; V : B := True);
procedure Set_Is_Abstract_Type (Id : E; V : B := True);
procedure Set_Normalized_First_Bit (Id : E; V : U);
procedure Set_Normalized_Position (Id : E; V : U);
procedure Set_Normalized_Position_Max (Id : E; V : U);
+ procedure Set_OK_To_Reference (Id : E; V : B := True);
procedure Set_OK_To_Rename (Id : E; V : B := True);
procedure Set_OK_To_Reorder_Components (Id : E; V : B := True);
procedure Set_Optimize_Alignment_Space (Id : E; V : B := True);
procedure Write_Field26_Name (Id : Entity_Id);
procedure Write_Field27_Name (Id : Entity_Id);
procedure Write_Field28_Name (Id : Entity_Id);
- -- These routines are used to output a nice symbolic name for the given
- -- field, depending on the Ekind. No blanks or end of lines are output,
- -- just the characters of the field name.
+ procedure Write_Field29_Name (Id : Entity_Id);
+ -- These routines are used in Treepr to output a nice symbolic name for
+ -- the given field, depending on the Ekind. No blanks or end of lines are
+ -- output, just the characters of the field name.
--------------------
-- Inline Pragmas --
pragma Inline (Has_Fully_Qualified_Name);
pragma Inline (Has_Gigi_Rep_Item);
pragma Inline (Has_Homonym);
+ pragma Inline (Has_Inheritable_Invariants);
pragma Inline (Has_Initial_Value);
+ pragma Inline (Has_Invariants);
pragma Inline (Has_Machine_Radix_Clause);
pragma Inline (Has_Master_Entity);
pragma Inline (Has_Missing_Return);
pragma Inline (Inner_Instances);
pragma Inline (Interface_Alias);
pragma Inline (Interface_Name);
+ pragma Inline (Invariant_Procedure);
pragma Inline (Is_AST_Entry);
pragma Inline (Is_Abstract_Subprogram);
pragma Inline (Is_Abstract_Type);
pragma Inline (Normalized_First_Bit);
pragma Inline (Normalized_Position);
pragma Inline (Normalized_Position_Max);
+ pragma Inline (OK_To_Reference);
pragma Inline (OK_To_Rename);
pragma Inline (OK_To_Reorder_Components);
pragma Inline (Optimize_Alignment_Space);
pragma Inline (Set_Has_Fully_Qualified_Name);
pragma Inline (Set_Has_Gigi_Rep_Item);
pragma Inline (Set_Has_Homonym);
+ pragma Inline (Set_Has_Inheritable_Invariants);
pragma Inline (Set_Has_Initial_Value);
+ pragma Inline (Set_Has_Invariants);
pragma Inline (Set_Has_Machine_Radix_Clause);
pragma Inline (Set_Has_Master_Entity);
pragma Inline (Set_Has_Missing_Return);
pragma Inline (Set_Inner_Instances);
pragma Inline (Set_Interface_Alias);
pragma Inline (Set_Interface_Name);
+ pragma Inline (Set_Invariant_Procedure);
pragma Inline (Set_Is_AST_Entry);
pragma Inline (Set_Is_Abstract_Subprogram);
pragma Inline (Set_Is_Abstract_Type);
pragma Inline (Set_Normalized_Position);
pragma Inline (Set_Normalized_Position_Max);
pragma Inline (Set_OK_To_Reorder_Components);
+ pragma Inline (Set_OK_To_Reference);
pragma Inline (Set_OK_To_Rename);
pragma Inline (Set_Optimize_Alignment_Space);
pragma Inline (Set_Optimize_Alignment_Time);
if No (Expr) then
+ -- For the default initialization case, if we have a private type
+ -- with invariants, and invariant checks are enabled, then insert an
+ -- invariant check after the object declaration. Note that it is OK
+ -- to clobber the object with an invalid value since if the exception
+ -- is raised, then the object will go out of scope.
+
+ if Is_Private_Type (Typ)
+ and then Present (Invariant_Procedure (Typ))
+ then
+ Insert_After (N,
+ Make_Invariant_Call (New_Occurrence_Of (Def_Id, Loc)));
+ end if;
+
-- Expand Initialize call for controlled objects. One may wonder why
-- the Initialize Call is not done in the regular Init procedure
-- attached to the record type. That's because the init procedure is
Set_Renamed_Object (Defining_Identifier (N), Expr_Q);
Set_Analyzed (N);
end if;
-
end if;
+ -- Exception on library entity not available
+
exception
when RE_Not_Available =>
return;
begin
if (Is_Entity_Name (Alt) and then Is_Type (Entity (Alt)))
- or else Nkind (Alt) = N_Range
+ or else Nkind (Alt) = N_Range
then
- Cond := Make_In (Sloc (Alt), Left_Opnd => L, Right_Opnd => R);
+ Cond :=
+ Make_In (Sloc (Alt),
+ Left_Opnd => L,
+ Right_Opnd => R);
else
Cond :=
- Make_Op_Eq (Sloc (Alt), Left_Opnd => L, Right_Opnd => R);
+ Make_Op_Eq (Sloc (Alt),
+ Left_Opnd => L,
+ Right_Opnd => R);
end if;
return Cond;
begin
-- If test is explicit x'First .. x'Last, replace by valid check
+ -- Could use some individual comments for this complex test ???
+
if Is_Scalar_Type (Ltyp)
and then Nkind (Lo_Orig) = N_Attribute_Reference
and then Attribute_Name (Lo_Orig) = Name_First
and then Nkind (Prefix (Lo_Orig)) in N_Has_Entity
and then Entity (Prefix (Lo_Orig)) = Ltyp
-
and then Nkind (Hi_Orig) = N_Attribute_Reference
and then Attribute_Name (Hi_Orig) = Name_Last
and then Nkind (Prefix (Hi_Orig)) in N_Has_Entity
and then Entity (Prefix (Hi_Orig)) = Ltyp
-
and then Comes_From_Source (N)
and then VM_Target = No_VM
then
end if;
Rewrite (N, Relocate_Node (Operand));
- return;
+ goto Done;
end if;
-- Nothing to do if this is the second argument of read. This is a
and then Attribute_Name (Parent (N)) = Name_Read
and then Next (First (Expressions (Parent (N)))) = N
then
- return;
+ goto Done;
+ end if;
+
+ -- Check for case of converting to a type that has an invariant
+ -- associated with it. This required an invariant check. We convert
+
+ -- typ (expr)
+
+ -- into
+
+ -- do invariant_check (typ (expr)) in typ (expr);
+
+ -- using Duplicate_Subexpr to avoid multiple side effects
+
+ -- Note: the Comes_From_Source check, and then the resetting of this
+ -- flag prevents what would otherwise be an infinite recursion.
+
+ if Present (Invariant_Procedure (Target_Type))
+ and then Comes_From_Source (N)
+ then
+ Set_Comes_From_Source (N, False);
+ Rewrite (N,
+ Make_Expression_With_Actions (Loc,
+ Actions => New_List (
+ Make_Invariant_Call (Duplicate_Subexpr (N))),
+ Expression => Duplicate_Subexpr_No_Checks (N)));
+ Analyze_And_Resolve (N, Target_Type);
+ goto Done;
end if;
-- Here if we may need to expand conversion
Expression => Opnd));
Analyze_And_Resolve (N, Target_Type);
- return;
+ goto Done;
end;
end if;
Type_Access_Level (Target_Type)
then
Raise_Accessibility_Error;
- return;
+ goto Done;
end if;
end if;
-- Sem_Ch8, and the expansion can interfere with this error check.
if Is_Access_Type (Target_Type) and then Is_Renamed_Object (N) then
- return;
+ goto Done;
end if;
-- Otherwise, proceed with processing tagged conversion
if Is_Interface (Actual_Op_Typ) then
Expand_Interface_Conversion (N, Is_Static => False);
- return;
+ goto Done;
end if;
if not Tag_Checks_Suppressed (Actual_Targ_Typ) then
and then (Vax_Float (Operand_Type) or else Vax_Float (Target_Type))
then
Expand_Vax_Conversion (N);
- return;
+ goto Done;
end if;
+
+ -- Here at end of processing
+
+ <<Done>>
+ null;
end Expand_N_Type_Conversion;
-----------------------------------
with Sem_Aux; use Sem_Aux;
with Sem_Ch8; use Sem_Ch8;
with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
return Equiv_Type;
end Make_CW_Equivalent_Type;
+ -------------------------
+ -- Make_Invariant_Call --
+ -------------------------
+
+ function Make_Invariant_Call (Expr : Node_Id) return Node_Id is
+ Loc : constant Source_Ptr := Sloc (Expr);
+ Typ : constant Entity_Id := Etype (Expr);
+
+ begin
+ if Check_Enabled (Name_Invariant)
+ or else
+ Check_Enabled (Name_Assertion)
+ then
+ return
+ Make_Procedure_Call_Statement (Loc,
+ Name =>
+ New_Occurrence_Of (Invariant_Procedure (Typ), Loc),
+ Parameter_Associations => New_List (Relocate_Node (Expr)));
+
+ else
+ return
+ Make_Null_Statement (Loc);
+ end if;
+ end Make_Invariant_Call;
+
------------------------
-- Make_Literal_Range --
------------------------
-- and returns True if so. Returns False otherwise. It is an error to call
-- this function if N is not of an access type.
+ function Make_Invariant_Call (Expr : Node_Id) return Node_Id;
+ -- Expr is an object of a type which Has_Invariants set (and which thus
+ -- also has an Invariant_Procedure set). If invariants are enabled, this
+ -- function returns a call to the Invariant procedure passing Expr as the
+ -- argument.
+
function Make_Subtype_From_Expr
(E : Node_Id;
Unc_Typ : Entity_Id) return Node_Id;
-- Set to True to skip compile and bind steps (except when Bind_Only is
-- set to True).
- List_Inherited_Pre_Post : Boolean := True;
+ List_Inherited_Aspects : Boolean := True;
-- GNAT
- -- List inherited preconditions and postconditions from Pre'Class and
- -- Post'Class aspects for ancestor subprograms.
+ -- List inherited invariants, preconditions, and postconditions from
+ -- Invariant'Class, Pre'Class, and Post'Class aspects.
List_Restrictions : Boolean := False;
-- GNATBIND
Pragma_Interrupt_Handler |
Pragma_Interrupt_State |
Pragma_Interrupt_Priority |
+ Pragma_Invariant |
Pragma_Java_Constructor |
Pragma_Java_Interface |
Pragma_Keep_Names |
with Snames; use Snames;
with Stand; use Stand;
with Sinfo; use Sinfo;
+with Stringt; use Stringt;
with Targparm; use Targparm;
with Ttypes; use Ttypes;
with Tbuild; use Tbuild;
when No_Aspect =>
raise Program_Error;
- -- Aspects taking an optional boolean argument. For all of
- -- these we just create a matching pragma and insert it,
- -- setting flag Cancel_Aspect if the expression is False.
+ -- Aspects taking an optional boolean argument. For all of
+ -- these we just create a matching pragma and insert it,
+ -- setting flag Cancel_Aspect if the expression is False.
when Aspect_Ada_2005 |
Aspect_Ada_2012 |
end if;
end if;
- -- Aspects corresponding to attribute definition clauses with
- -- the exception of Address which is treated specially.
+ -- Aspects corresponding to attribute definition clauses
when Aspect_Address |
Aspect_Alignment |
-- with a first argument that is the expression, and a second
-- argument that is an informative message if the test fails.
-- This is inserted right after the declaration, to get the
- -- required pragma placement.
+ -- required pragma placement. The processing for the pragmas
+ -- takes care of the required delay.
when Aspect_Pre | Aspect_Post => declare
Pname : Name_Id;
goto Continue;
end;
- -- Aspects currently unimplemented
+ -- Invariant aspect generates an Invariant pragma with a first
+ -- argument that is the entity, and the second argument is the
+ -- expression. This is inserted right after the declaration, to
+ -- get the required pragma placement. The processing for the
+ -- pragma takes care of the required delay.
- when Aspect_Invariant |
- Aspect_Predicate =>
+ when Aspect_Invariant =>
+ -- Construct the pragma
+
+ Aitem :=
+ Make_Pragma (Loc,
+ Pragma_Argument_Associations =>
+ New_List (Ent, Relocate_Node (Expr)),
+ Class_Present => Class_Present (Aspect),
+ Pragma_Identifier =>
+ Make_Identifier (Sloc (Id), Name_Invariant));
+
+ -- Add message unless exception messages are suppressed
+
+ if not Opt.Exception_Locations_Suppressed then
+ Append_To (Pragma_Argument_Associations (Aitem),
+ Make_Pragma_Argument_Association (Eloc,
+ Chars => Name_Message,
+ Expression =>
+ Make_String_Literal (Eloc,
+ Strval => "failed invariant from "
+ & Build_Location_String (Eloc))));
+ end if;
+
+ Set_From_Aspect_Specification (Aitem, True);
+
+ -- For Invariant case, insert immediately after the entity
+ -- declaration. We do not have to worry about delay issues
+ -- since the pragma processing takes care of this.
+
+ Insert_After (N, Aitem);
+ goto Continue;
+
+ -- Aspects currently unimplemented
+
+ when Aspect_Predicate =>
Error_Msg_N ("aspect& not implemented", Identifier (Aspect));
goto Continue;
end case;
end if;
end Analyze_Record_Representation_Clause;
+ -------------------------------
+ -- Build_Invariant_Procedure --
+ -------------------------------
+
+ -- The procedure that is constructed here has the form
+
+ -- procedure typInvariant (Ixxx : typ) is
+ -- begin
+ -- pragma Check (Invariant, exp, "failed invariant from xxx");
+ -- pragma Check (Invariant, exp, "failed invariant from xxx");
+ -- ...
+ -- pragma Check (Invariant, exp, "failed inherited invariant from xxx");
+ -- ...
+ -- end typInvariant;
+
+ procedure Build_Invariant_Procedure
+ (Typ : Entity_Id;
+ PDecl : out Node_Id;
+ PBody : out Node_Id)
+ is
+ Loc : constant Source_Ptr := Sloc (Typ);
+ Stmts : List_Id;
+ Spec : Node_Id;
+ SId : Entity_Id;
+
+ procedure Add_Invariants (T : Entity_Id; Inherit : Boolean);
+ -- Appends statements to Stmts for any invariants in the rep item chain
+ -- of the given type. If Inherit is False, then we only process entries
+ -- on the chain for the type Typ. If Inherit is True, then we ignore any
+ -- Invariant aspects, but we process all Invariant'Class aspects, adding
+ -- "inherited" to the exception message and generating an informational
+ -- message about the inheritance of an invariant.
+
+ Object_Name : constant Name_Id := New_Internal_Name ('I');
+ -- Name for argument of invariant procedure
+
+ --------------------
+ -- Add_Invariants --
+ --------------------
+
+ procedure Add_Invariants (T : Entity_Id; Inherit : Boolean) is
+ Ritem : Node_Id;
+ Arg1 : Node_Id;
+ Arg2 : Node_Id;
+ Arg3 : Node_Id;
+ Exp : Node_Id;
+ Loc : Source_Ptr;
+ Assoc : List_Id;
+ Str : String_Id;
+
+ function Replace_Node (N : Node_Id) return Traverse_Result;
+ -- Process single node for traversal to replace type references
+
+ procedure Replace_Type is new Traverse_Proc (Replace_Node);
+ -- Traverse an expression changing every occurrence of an entity
+ -- reference to type T with a reference to the object argument.
+
+ ------------------
+ -- Replace_Node --
+ ------------------
+
+ function Replace_Node (N : Node_Id) return Traverse_Result is
+ begin
+ -- Case of entity name referencing the type
+
+ if Is_Entity_Name (N)
+ and then Entity (N) = T
+ then
+ -- Invariant'Class, replace with T'Class (obj)
+
+ if Class_Present (Ritem) then
+ Rewrite (N,
+ Make_Type_Conversion (Loc,
+ Subtype_Mark =>
+ Make_Attribute_Reference (Loc,
+ Prefix =>
+ New_Occurrence_Of (T, Loc),
+ Attribute_Name => Name_Class),
+ Expression =>
+ Make_Identifier (Loc,
+ Chars => Object_Name)));
+
+ -- Invariant, replace with obj
+
+ else
+ Rewrite (N,
+ Make_Identifier (Loc,
+ Chars => Object_Name));
+ end if;
+
+ -- All done with this node
+
+ return Skip;
+
+ -- Not an instance of the type entity, keep going
+
+ else
+ return OK;
+ end if;
+ end Replace_Node;
+
+ -- Start of processing for Add_Invariants
+
+ begin
+ Ritem := First_Rep_Item (T);
+ while Present (Ritem) loop
+ if Nkind (Ritem) = N_Pragma
+ and then Pragma_Name (Ritem) = Name_Invariant
+ then
+ Arg1 := First (Pragma_Argument_Associations (Ritem));
+ Arg2 := Next (Arg1);
+ Arg3 := Next (Arg2);
+
+ Arg1 := Get_Pragma_Arg (Arg1);
+ Arg2 := Get_Pragma_Arg (Arg2);
+
+ -- For Inherit case, ignore Invariant, process only Class case
+
+ if Inherit then
+ if not Class_Present (Ritem) then
+ goto Continue;
+ end if;
+
+ -- For Inherit false, process only item for right type
+
+ else
+ if Entity (Arg1) /= Typ then
+ goto Continue;
+ end if;
+ end if;
+
+ if No (Stmts) then
+ Stmts := Empty_List;
+ end if;
+
+ Exp := New_Copy_Tree (Arg2);
+ Loc := Sloc (Exp);
+
+ -- We need to replace any occurrences of the name of the type
+ -- with references to the object, converted to type'Class in
+ -- the case of Invariant'Class aspects. We do this by first
+ -- doing a preanalysis, to identify all the entities, then
+ -- we traverse looking for the type entity, and doing the
+ -- necessary substitution. The preanalysis is done with the
+ -- special OK_To_Reference flag set on the type, so that if
+ -- we get an occurrence of this type, it will be reognized
+ -- as legitimate.
+
+ Set_OK_To_Reference (T, True);
+ Preanalyze_Spec_Expression (Exp, Standard_Boolean);
+ Set_OK_To_Reference (T, False);
+
+ -- Do the traversal
+
+ Replace_Type (Exp);
+
+ -- Build first two arguments for Check pragma
+
+ Assoc := New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression =>
+ Make_Identifier (Loc,
+ Chars => Name_Invariant)),
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Exp));
+
+ -- Add message if present in Invariant pragma
+
+ if Present (Arg3) then
+ Str := Strval (Get_Pragma_Arg (Arg3));
+
+ -- If inherited case, and message starts "failed invariant",
+ -- change it to be "failed inherited invariant".
+
+ if Inherit then
+ String_To_Name_Buffer (Str);
+
+ if Name_Buffer (1 .. 16) = "failed invariant" then
+ Insert_Str_In_Name_Buffer ("inherited ", 8);
+ Str := String_From_Name_Buffer;
+ end if;
+ end if;
+
+ Append_To (Assoc,
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_String_Literal (Loc, Str)));
+ end if;
+
+ -- Add Check pragma to list of statements
+
+ Append_To (Stmts,
+ Make_Pragma (Loc,
+ Pragma_Identifier =>
+ Make_Identifier (Loc,
+ Chars => Name_Check),
+ Pragma_Argument_Associations => Assoc));
+
+ -- If Inherited case and option enabled, output info msg. Note
+ -- that we know this is a case of Invariant'Class.
+
+ if Inherit and Opt.List_Inherited_Aspects then
+ Error_Msg_Sloc := Sloc (Ritem);
+ Error_Msg_N
+ ("?info: & inherits `Invariant''Class` aspect from #",
+ Typ);
+ end if;
+ end if;
+
+ <<Continue>>
+ Next_Rep_Item (Ritem);
+ end loop;
+ end Add_Invariants;
+
+ -- Start of processing for Build_Invariant_Procedure
+
+ begin
+ Stmts := No_List;
+ PDecl := Empty;
+ PBody := Empty;
+
+ -- Add invariants for the current type
+
+ Add_Invariants (Typ, Inherit => False);
+
+ -- Add invariants for parent types
+
+ declare
+ Current_Typ : Entity_Id;
+ Parent_Typ : Entity_Id;
+
+ begin
+ Current_Typ := Typ;
+ loop
+ Parent_Typ := Etype (Current_Typ);
+
+ if Is_Private_Type (Parent_Typ)
+ and then Present (Full_View (Base_Type (Parent_Typ)))
+ then
+ Parent_Typ := Full_View (Base_Type (Parent_Typ));
+ end if;
+
+ exit when Parent_Typ = Current_Typ;
+
+ Current_Typ := Parent_Typ;
+ Add_Invariants (Current_Typ, Inherit => True);
+ end loop;
+ end;
+
+ -- Add invariants for inherited interfaces
+ -- (commented out because it blows up on simpleinv in J701-022)
+
+-- declare
+-- Ifaces : Elist_Id;
+-- Iface : Elmt_Id;
+--
+-- begin
+-- Collect_Interfaces
+-- (T => Typ,
+-- Ifaces_List => Ifaces,
+-- Exclude_Parents => True,
+-- Use_Full_View => True);
+--
+-- loop
+-- Iface := First_Elmt (Ifaces);
+-- exit when Iface = No_Elmt;
+-- Add_Invariants (Node (Iface), Inherit => True);
+-- Remove_Elmt (Ifaces, Iface);
+-- end loop;
+-- end;
+
+ -- Build the procedure if we generated at least one Check pragma
+
+ if Stmts /= No_List then
+
+ -- Build procedure declaration
+
+ SId :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Typ), "Invariant"));
+ Set_Invariant_Procedure (Typ, SId);
+
+ Spec :=
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => SId,
+ Parameter_Specifications => New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier =>
+ Make_Defining_Identifier (Loc,
+ Chars => Object_Name),
+ Parameter_Type =>
+ New_Occurrence_Of (Typ, Loc))));
+
+ PDecl :=
+ Make_Subprogram_Declaration (Loc,
+ Specification => Spec);
+
+ -- Build procedure body
+
+ SId :=
+ Make_Defining_Identifier (Loc,
+ Chars => New_External_Name (Chars (Typ), "Invariant"));
+
+ Spec :=
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name => SId,
+ Parameter_Specifications => New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier =>
+ Make_Defining_Identifier (Loc,
+ Chars => Object_Name),
+ Parameter_Type =>
+ New_Occurrence_Of (Typ, Loc))));
+
+ PBody :=
+ Make_Subprogram_Body (Loc,
+ Specification => Spec,
+ Declarations => Empty_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Stmts));
+ end if;
+ end Build_Invariant_Procedure;
+
-----------------------------------
-- Check_Constant_Address_Clause --
-----------------------------------
-- order is specified and there is at least one component clause. Adjusts
-- component positions according to either Ada 95 or Ada 2005 (AI-133).
+ procedure Build_Invariant_Procedure
+ (Typ : Entity_Id;
+ PDecl : out Node_Id;
+ PBody : out Node_Id);
+ -- If Typ has Invariants (indicated by Has_Invariants being set for Typ,
+ -- indicating the presence of Pragma Invariant entries on the rep chain,
+ -- note that Invariant aspects are converted to pragma Invariant), then
+ -- this procedure builds the spec and body for the corresponding Invariant
+ -- procedure, returning themn in PDecl and PBody. In some error situations
+ -- no procedure is built, in which case PDecl/PBody are empty on return.
+
procedure Check_Record_Representation_Clause (N : Node_Id);
-- This procedure completes the analysis of a record representation clause
-- N. It is called at freeze time after adjustment of component clause bit
Generate_Definition (T);
+ -- For other than Ada 2012, just enter the name in the current scope
+
if Ada_Version < Ada_2012 then
Enter_Name (T);
Set_Is_Controlled (Derived_Type, Is_Controlled (Parent_Type));
Set_Is_Tagged_Type (Derived_Type, Is_Tagged_Type (Parent_Type));
+ -- Propagate invariant information. The new type has invariants if
+ -- they are inherited from the parent type, and these invariants can
+ -- be further inherited, so both flags are set.
+
+ if Has_Inheritable_Invariants (Parent_Type) then
+ Set_Has_Inheritable_Invariants (Derived_Type);
+ Set_Has_Invariants (Derived_Type);
+ end if;
+
-- The derived type inherits the representation clauses of the parent.
-- However, for a private type that is completed by a derivation, there
-- may be operation attributes that have been specified already (stream
elsif Ekind (Prev) = E_Incomplete_Type
and then (Ada_Version < Ada_2012
- or else No (Full_View (Prev))
- or else not Is_Private_Type (Full_View (Prev)))
+ or else No (Full_View (Prev))
+ or else not Is_Private_Type (Full_View (Prev)))
then
-- Indicate that the incomplete declaration has a matching full
-- A return statement for a build-in-place function returning a
-- synchronized type also introduces an unchecked conversion.
- when N_Type_Conversion | N_Unchecked_Type_Conversion =>
+ when N_Type_Conversion |
+ N_Unchecked_Type_Conversion =>
return not Comes_From_Source (Exp)
and then
OK_For_Limited_Init_In_05
(Typ, Expression (Original_Node (Exp)));
- when N_Indexed_Component | N_Selected_Component |
- N_Explicit_Dereference =>
+ when N_Indexed_Component |
+ N_Selected_Component |
+ N_Explicit_Dereference =>
return Nkind (Exp) = N_Function_Call;
-- A use of 'Input is a function call, hence allowed. Normally the
-- If the private view has user specified stream attributes, then so has
-- the full view.
+ -- Why the test, how could these flags be already set in Full_T ???
+
if Has_Specified_Stream_Read (Priv_T) then
Set_Has_Specified_Stream_Read (Full_T);
end if;
+
if Has_Specified_Stream_Write (Priv_T) then
Set_Has_Specified_Stream_Write (Full_T);
end if;
+
if Has_Specified_Stream_Input (Priv_T) then
Set_Has_Specified_Stream_Input (Full_T);
end if;
+
if Has_Specified_Stream_Output (Priv_T) then
Set_Has_Specified_Stream_Output (Full_T);
end if;
+
+ -- Deal with invariants
+
+ if Has_Invariants (Full_T)
+ or else
+ Has_Invariants (Priv_T)
+ then
+ Set_Has_Invariants (Full_T);
+ Set_Has_Invariants (Priv_T);
+ end if;
+
+ if Has_Inheritable_Invariants (Full_T)
+ or else
+ Has_Inheritable_Invariants (Priv_T)
+ then
+ Set_Has_Inheritable_Invariants (Full_T);
+ Set_Has_Inheritable_Invariants (Priv_T);
+ end if;
+
+ -- This is where we build the invariant procedure if needed
+
+ if Has_Invariants (Priv_T) then
+ declare
+ PDecl : Entity_Id;
+ PBody : Entity_Id;
+ Packg : constant Node_Id := Declaration_Node (Scope (Priv_T));
+
+ begin
+ Build_Invariant_Procedure (Full_T, PDecl, PBody);
+
+ -- Error defense, normally these should be set
+
+ if Present (PDecl) and then Present (PBody) then
+
+ -- Spec goes at the end of the public part of the package.
+ -- That's behind us, so we have to manually analyze the
+ -- inserted spec.
+
+ Append_To (Visible_Declarations (Packg), PDecl);
+ Analyze (PDecl);
+
+ -- Body goes at the end of the private part of the package.
+ -- That's ahead of us so it will get analyzed later on when
+ -- we come to it.
+
+ Append_To (Private_Declarations (Packg), PBody);
+
+ -- Copy Invariant procedure to private declaration
+
+ Set_Invariant_Procedure (Priv_T, Invariant_Procedure (Full_T));
+ end if;
+ end;
+ end if;
end Process_Full_View;
-----------------------------------
-- conditions for the body and assembling and inserting the _postconditions
-- procedure. N is the node for the subprogram body and Body_Id/Spec_Id are
-- the entities for the body and separate spec (if there is no separate
- -- spec, Spec_Id is Empty).
+ -- spec, Spec_Id is Empty). Note that invariants also provide a source
+ -- of postconditions, which are also handled in this procedure.
procedure Set_Formal_Validity (Formal_Id : Entity_Id);
-- Formal_Id is an formal parameter entity. This procedure deals with
if Nkind (N) = N_Function_Specification then
Set_Ekind (Designator, E_Function);
Set_Mechanism (Designator, Default_Mechanism);
-
else
Set_Ekind (Designator, E_Procedure);
Set_Etype (Designator, Standard_Void_Type);
elsif Nkind (N) = N_Function_Specification then
Push_Scope (Designator);
-
Analyze_Return_Type (N);
-
End_Scope;
end if;
+ -- Function case
+
if Nkind (N) = N_Function_Specification then
+
+ -- Deal with operator symbol case
+
if Nkind (Designator) = N_Defining_Operator_Symbol then
Valid_Operator_Definition (Designator);
end if;
Error_Msg_N
("function that returns abstract type must be abstract", N);
- -- Ada 2012 (AI-0073): extend this test to subprograms with an
+ -- Ada 2012 (AI-0073): Extend this test to subprograms with an
-- access result whose designated type is abstract.
elsif Nkind (Result_Definition (N)) = N_Access_Definition
procedure List_Inherited_Pre_Post_Aspects (E : Entity_Id) is
begin
- if Opt.List_Inherited_Pre_Post
+ if Opt.List_Inherited_Aspects
and then (Is_Subprogram (E) or else Is_Generic_Subprogram (E))
then
declare
is
Loc : constant Source_Ptr := Sloc (N);
Prag : Node_Id;
- Subp : Entity_Id;
Parms : List_Id;
+ Designator : Entity_Id;
+ -- Subprogram designator, set from Spec_Id if present, else Body_Id
+
Precond : Node_Id := Empty;
-- Set non-Empty if we prepend precondition to the declarations. This
-- is used to hook up inherited preconditions (adding the condition
-- Precondition inherited from parent subprogram
Inherited : constant Subprogram_List :=
- Inherited_Subprograms (Spec_Id);
- -- List of subprograms inherited by this subprogram, null if no Spec_Id
+ Inherited_Subprograms (Spec_Id);
+ -- List of subprograms inherited by this subprogram
Plist : List_Id := No_List;
-- List of generated postconditions
-- references to parameters of the inherited subprogram to point to the
-- corresponding parameters of the current subprogram.
+ function Invariants_Present return Boolean;
+ -- Determines if any invariants are present for any OUT or IN OUT
+ -- parameters of the subprogram, or (for a function) for the return.
+
--------------
-- Grab_PPC --
--------------
begin
Map := New_Elmt_List;
PF := First_Formal (Pspec);
- CF := First_Formal (Spec_Id);
+ CF := First_Formal (Designator);
while Present (PF) loop
Append_Elmt (PF, Map);
Append_Elmt (CF, Map);
return CP;
end Grab_PPC;
+ ------------------------
+ -- Invariants_Present --
+ ------------------------
+
+ function Invariants_Present return Boolean is
+ Formal : Entity_Id;
+
+ begin
+ -- Check function return result
+
+ if Ekind (Designator) /= E_Procedure
+ and then Has_Invariants (Etype (Designator))
+ then
+ return True;
+ end if;
+
+ -- Check parameters
+
+ Formal := First_Formal (Designator);
+ while Present (Formal) loop
+ if Ekind (Formal) /= E_In_Parameter
+ and then Has_Invariants (Etype (Formal))
+ then
+ return True;
+ end if;
+
+ Next_Formal (Formal);
+ end loop;
+
+ return False;
+ end Invariants_Present;
+
-- Start of processing for Process_PPCs
begin
+ -- Capture designator from spec if present, else from body
+
+ if Present (Spec_Id) then
+ Designator := Spec_Id;
+ else
+ Designator := Body_Id;
+ end if;
+
-- Grab preconditions from spec
if Present (Spec_Id) then
-- pragma Check (Postcondition, condition [,message]);
-- pragma Check (Postcondition, condition [,message]);
-- ...
+ -- Invariant_Procedure (_Result) ...
+ -- Invariant_Procedure (Arg1)
+ -- ...
-- end;
-- First we deal with the postconditions in the body
-- Now deal with any postconditions from the spec
if Present (Spec_Id) then
- declare
+ Spec_Postconditions : declare
procedure Process_Post_Conditions
(Spec : Node_Id;
Class : Boolean);
end loop;
end Process_Post_Conditions;
+ -- Start of processing for Spec_Postconditions
+
begin
if Present (Spec_PPC_List (Spec_Id)) then
Process_Post_Conditions (Spec_Id, Class => False);
Process_Post_Conditions (Inherited (J), Class => True);
end if;
end loop;
- end;
+ end Spec_Postconditions;
end if;
- -- If we had any postconditions and expansion is enabled, build
- -- the _Postconditions procedure.
+ -- If we had any postconditions and expansion is enabled, or if the
+ -- procedure has invariants, then build the _Postconditions procedure.
- if Present (Plist)
+ if (Present (Plist) or else Invariants_Present)
and then Expander_Active
then
- Subp := Defining_Entity (N);
+ if No (Plist) then
+ Plist := Empty_List;
+ end if;
+
+ -- Special processing for function case
+
+ if Ekind (Designator) /= E_Procedure then
+ declare
+ Rent : constant Entity_Id :=
+ Make_Defining_Identifier (Loc,
+ Chars => Name_uResult);
+ Ftyp : constant Entity_Id := Etype (Designator);
+
+ begin
+ Set_Etype (Rent, Ftyp);
+
+ -- Add argument for return
+
+ Parms :=
+ New_List (
+ Make_Parameter_Specification (Loc,
+ Parameter_Type => New_Occurrence_Of (Ftyp, Loc),
+ Defining_Identifier => Rent));
+
+ -- Add invariant call if returning type with invariants
+
+ if Present (Invariant_Procedure (Etype (Rent))) then
+ Append_To (Plist,
+ Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
+ end if;
+ end;
+
+ -- Procedure rather than a function
- if Etype (Subp) /= Standard_Void_Type then
- Parms := New_List (
- Make_Parameter_Specification (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier (Loc,
- Chars => Name_uResult),
- Parameter_Type => New_Occurrence_Of (Etype (Subp), Loc)));
else
Parms := No_List;
end if;
+ -- Add invariant calls for parameters. Note that this is done for
+ -- functions as well, since in Ada 2012 they can have IN OUT args.
+
+ declare
+ Formal : Entity_Id;
+
+ begin
+ Formal := First_Formal (Designator);
+ while Present (Formal) loop
+ if Ekind (Formal) /= E_In_Parameter
+ and then Present (Invariant_Procedure (Etype (Formal)))
+ then
+ Append_To (Plist,
+ Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)));
+ end if;
+
+ Next_Formal (Formal);
+ end loop;
+ end;
+
+ -- Build and insert postcondition procedure
+
declare
Post_Proc : constant Entity_Id :=
- Make_Defining_Identifier (Loc,
- Chars => Name_uPostconditions);
+ Make_Defining_Identifier (Loc,
+ Chars => Name_uPostconditions);
-- The entity for the _Postconditions procedure
begin
-- If this is a procedure, set the Postcondition_Proc attribute on
-- the proper defining entity for the subprogram.
- if Etype (Subp) = Standard_Void_Type then
- if Present (Spec_Id) then
- Set_Postcondition_Proc (Spec_Id, Post_Proc);
- else
- Set_Postcondition_Proc (Body_Id, Post_Proc);
- end if;
+ if Ekind (Designator) = E_Procedure then
+ Set_Postcondition_Proc (Designator, Post_Proc);
end if;
end;
- if Present (Spec_Id) then
- Set_Has_Postconditions (Spec_Id);
- else
- Set_Has_Postconditions (Body_Id);
- end if;
+ Set_Has_Postconditions (Designator);
end if;
end Process_PPCs;
declare
Orig_Spec : constant Node_Id := Specification (Orig_Decl);
Save_Priv : constant List_Id := Private_Declarations (Orig_Spec);
-
begin
Set_Private_Declarations (Orig_Spec, Empty_List);
Save_Global_References (Orig_Decl);
procedure New_Private_Type (N : Node_Id; Id : Entity_Id; Def : Node_Id) is
begin
+ -- For other than Ada 2012, enter tha name in the current scope
+
if Ada_Version < Ada_2012 then
Enter_Name (Id);
else
declare
Prev : Entity_Id;
-
begin
Prev := Find_Type_Name (N);
-
pragma Assert (Prev = Id
or else (Ekind (Prev) = E_Incomplete_Type
- and then Present (Full_View (Prev))
- and then Full_View (Prev) = Id));
+ and then Present (Full_View (Prev))
+ and then Full_View (Prev) = Id));
end;
end if;
if Nkind (Expression (Arg1)) = N_Null then
Analyze (Expression (Arg1));
+
+ -- This is an odd case, this is not really an expression, so
+ -- we don't have a type for it. So just set the type to Empty.
+
Set_Etype (Expression (Arg1), Empty);
- -- It's not really an expression, and we have no type for it
-- Case of Default_Storage_Pool (storage_pool_NAME);
end loop;
end Interrupt_State;
+ ---------------
+ -- Invariant --
+ ---------------
+
+ -- pragma Invariant
+ -- ([Entity =>] type_LOCAL_NAME,
+ -- [Check =>] EXPRESSION
+ -- [,[Message =>] String_Expression]);
+
+ when Pragma_Invariant => Invariant : declare
+ Type_Id : Node_Id;
+ Typ : Entity_Id;
+
+ Discard : Boolean;
+ pragma Unreferenced (Discard);
+
+ begin
+ GNAT_Pragma;
+ Check_At_Least_N_Arguments (2);
+ Check_At_Most_N_Arguments (3);
+ Check_Optional_Identifier (Arg1, Name_Entity);
+ Check_Optional_Identifier (Arg2, Name_Check);
+
+ if Arg_Count = 3 then
+ Check_Optional_Identifier (Arg3, Name_Message);
+ Check_Arg_Is_Static_Expression (Arg3, Standard_String);
+ end if;
+
+ Check_Arg_Is_Local_Name (Arg1);
+
+ Type_Id := Get_Pragma_Arg (Arg1);
+ Find_Type (Type_Id);
+ Typ := Entity (Type_Id);
+
+ if Typ = Any_Type then
+ return;
+
+ elsif not Ekind_In (Typ, E_Private_Type,
+ E_Record_Type_With_Private,
+ E_Limited_Private_Type)
+ then
+ Error_Pragma_Arg
+ ("pragma% only allowed for private type", Arg1);
+ end if;
+
+ -- Note that the type has at least one invariant, and also that
+ -- it has inheritable invariants if we have Invariant'Class.
+
+ Set_Has_Invariants (Typ);
+
+ if Class_Present (N) then
+ Set_Has_Inheritable_Invariants (Typ);
+ end if;
+
+ -- The remaining processing is simply to link the pragma on to
+ -- the rep item chain, for processing when the type is frozen.
+ -- This is accomplished by a call to Rep_Item_Too_Late.
+
+ Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
+ end Invariant;
+
----------------------
-- Java_Constructor --
----------------------
Pragma_Interrupt_Handler => -1,
Pragma_Interrupt_Priority => -1,
Pragma_Interrupt_State => -1,
+ Pragma_Invariant => -1,
Pragma_Java_Constructor => -1,
Pragma_Java_Interface => -1,
Pragma_Keep_Names => 0,
Set_Entity_With_Style_Check (N, E);
Eval_Entity_Name (N);
- -- Allow use of subtype only if it is a concurrent type where we are
- -- currently inside the body. This will eventually be expanded into a
- -- call to Self (for tasks) or _object (for protected objects). Any
- -- other use of a subtype is invalid.
+ -- Case of subtype name appearing as an operand in expression
elsif Is_Type (E) then
+
+ -- Allow use of subtype if it is a concurrent type where we are
+ -- currently inside the body. This will eventually be expanded into a
+ -- call to Self (for tasks) or _object (for protected objects). Any
+ -- other use of a subtype is invalid.
+
if Is_Concurrent_Type (E)
and then In_Open_Scopes (E)
then
null;
+
+ -- Allow reference to type specifically marked as being OK in this
+ -- context (this is used for example for type names in invariants).
+
+ elsif OK_To_Reference (E) then
+ null;
+
+ -- Any other use is an eror
+
else
Error_Msg_N
("invalid use of subtype mark in expression or call", N);
Elab_Warnings := True;
Implementation_Unit_Warnings := True;
Ineffective_Inline_Warnings := True;
- List_Inherited_Pre_Post := True;
+ List_Inherited_Aspects := True;
Warn_On_Ada_2005_Compatibility := True;
Warn_On_Ada_2012_Compatibility := True;
Warn_On_All_Unread_Out_Parameters := True;
Warn_On_Overlap := False;
when 'l' =>
- List_Inherited_Pre_Post := True;
+ List_Inherited_Aspects := True;
when 'L' =>
- List_Inherited_Pre_Post := False;
+ List_Inherited_Aspects := False;
when 'm' =>
Warn_On_Suspicious_Modulus_Value := True;
Elab_Warnings := False;
Implementation_Unit_Warnings := False;
Ineffective_Inline_Warnings := True;
- List_Inherited_Pre_Post := False;
+ List_Inherited_Aspects := False;
Warn_On_Ada_2005_Compatibility := True;
Warn_On_Ada_2012_Compatibility := True;
Warn_On_All_Unread_Out_Parameters := False;
Constant_Condition_Warnings := True;
Implementation_Unit_Warnings := True;
Ineffective_Inline_Warnings := True;
- List_Inherited_Pre_Post := True;
+ List_Inherited_Aspects := True;
Warn_On_Ada_2005_Compatibility := True;
Warn_On_Ada_2012_Compatibility := True;
Warn_On_Assertion_Failure := True;
Elab_Warnings := False;
Implementation_Unit_Warnings := False;
Ineffective_Inline_Warnings := False;
- List_Inherited_Pre_Post := False;
+ List_Inherited_Aspects := False;
Warn_On_Ada_2005_Compatibility := False;
Warn_On_Ada_2012_Compatibility := False;
Warn_On_All_Unread_Out_Parameters := False;
-- Names of aspects for which there are no matching pragmas or attributes
-- so that they need to be included for aspect specification use.
- Name_Invariant : constant Name_Id := N + $;
Name_Post : constant Name_Id := N + $;
Name_Pre : constant Name_Id := N + $;
Name_Predicate : constant Name_Id := N + $;
Name_Interface_Name : constant Name_Id := N + $; -- GNAT
Name_Interrupt_Handler : constant Name_Id := N + $;
Name_Interrupt_Priority : constant Name_Id := N + $;
+ Name_Invariant : constant Name_Id := N + $; -- GNAT
Name_Java_Constructor : constant Name_Id := N + $; -- GNAT
Name_Java_Interface : constant Name_Id := N + $; -- GNAT
Name_Keep_Names : constant Name_Id := N + $; -- GNAT
Pragma_Interface_Name,
Pragma_Interrupt_Handler,
Pragma_Interrupt_Priority,
+ Pragma_Invariant,
Pragma_Java_Constructor,
Pragma_Java_Interface,
Pragma_Keep_Names,
Print_Eol;
end if;
+ if Field_Present (Field29 (Ent)) then
+ Print_Str (Prefix);
+ Write_Field29_Name (Ent);
+ Write_Str (" = ");
+ Print_Field (Field29 (Ent));
+ Print_Eol;
+ end if;
+
Write_Entity_Flags (Ent, Prefix);
end Print_Entity_Info;
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2007, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2010, 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- --
IEEES_Model_Epsilon : constant := 2#1.0#E-23;
IEEEL_Model_Epsilon : constant := 2#1.0#E-52;
IEEEX_Model_Epsilon : constant := 2#1.0#E-63;
- VAXFF_Model_Epsilon : constant := 16#0.1000_000#E-4;
- VAXDF_Model_Epsilon : constant := 16#0.4000_0000_0000_000#E-7;
- VAXGF_Model_Epsilon : constant := 16#0.4000_0000_0000_00#E-12;
+ VAXFF_Model_Epsilon : constant := 2#1.0#E-23;
+ VAXDF_Model_Epsilon : constant := 2#1.0#E-55;
+ VAXGF_Model_Epsilon : constant := 2#1.0#E-52;
AAMPS_Model_Epsilon : constant := 2#1.0#E-23;
AAMPL_Model_Epsilon : constant := 2#1.0#E-39;
IEEES_Model_Small : constant := 2#1.0#E-126;
IEEEL_Model_Small : constant := 2#1.0#E-1022;
- IEEEX_Model_Small : constant := 2#1.0#E-16381;
- VAXFF_Model_Small : constant := 16#0.8000_000#E-21;
- VAXDF_Model_Small : constant := 16#0.8000_0000_0000_000#E-31;
- VAXGF_Model_Small : constant := 16#0.8000_0000_0000_00#E-51;
- AAMPS_Model_Small : constant := 16#0.8000_000#E-21;
- AAMPL_Model_Small : constant := 16#0.8000_0000_000#E-31;
+ IEEEX_Model_Small : constant := 2#1.0#E-16382;
+ VAXFF_Model_Small : constant := 2#1.0#E-128;
+ VAXDF_Model_Small : constant := 2#1.0#E-128;
+ VAXGF_Model_Small : constant := 2#1.0#E-1024;
+ AAMPS_Model_Small : constant := 2#1.0#E-128;
+ AAMPL_Model_Small : constant := 2#1.0#E-128;
IEEES_Safe_First : constant := -16#0.FFFF_FF#E+32;
IEEEL_Safe_First : constant := -16#0.FFFF_FFFF_FFFF_F8#E+256;
IEEES_Safe_Small : constant := 2#1.0#E-126;
IEEEL_Safe_Small : constant := 2#1.0#E-1022;
- IEEEX_Safe_Small : constant := 2#1.0#E-16381;
- VAXFF_Safe_Small : constant := 16#0.1000_000#E-31;
- VAXDF_Safe_Small : constant := 16#0.1000_0000_0000_000#E-31;
- VAXGF_Safe_Small : constant := 16#0.1000_0000_0000_00#E-255;
- AAMPS_Safe_Small : constant := 16#0.1000_000#E-31;
- AAMPL_Safe_Small : constant := 16#0.1000_0000_000#E-31;
+ IEEEX_Safe_Small : constant := 2#1.0#E-16382;
+ VAXFF_Safe_Small : constant := 2#1.0#E-128;
+ VAXDF_Safe_Small : constant := 2#1.0#E-128;
+ VAXGF_Safe_Small : constant := 2#1.0#E-1024;
+ AAMPS_Safe_Small : constant := 2#1.0#E-128;
+ AAMPL_Safe_Small : constant := 2#1.0#E-128;
----------------------
-- Typed Attributes --
IEEEL_Last : constant := 16#0.FFFF_FFFF_FFFF_F8#E+256;
IEEEX_Last : constant := 16#0.FFFF_FFFF_FFFF_FFFF#E+4096;
VAXFF_Last : constant := 16#0.7FFF_FF8#E+32;
- VAXDF_Last : constant := 16#0.7FFF_FFFF_FFFF_FC0#E+32;
+ VAXDF_Last : constant := 16#0.7FFF_FFFF_FFFF_FF8#E+32;
VAXGF_Last : constant := 16#0.7FFF_FFFF_FFFF_FC#E+256;
AAMPS_Last : constant := 16#0.7FFF_FF8#E+32;
AAMPL_Last : constant := 16#0.7FFF_FFFF_FF8#E+32;
"elaboration pragma");
Write_Line (" L* turn off warnings for missing " &
"elaboration pragma");
- Write_Line (" .l* turn on info messages for inherited pre/" &
- "postconditions");
- Write_Line (" .L turn off info messages for inherited pre/" &
- "postconditions");
+ Write_Line (" .l* turn on info messages for inherited aspects");
+ Write_Line (" .L turn off info messages for inherited aspects");
Write_Line (" m+ turn on warnings for variable assigned " &
"but not read");
Write_Line (" M* turn off warnings for variable assigned " &
OSDN Git Service
