+2013-04-24 Robert Dewar <dewar@adacore.com>
+
+ * sem_ch3.adb, sem_ch7.adb: Minor reformatting.
+ * gnat_rm.texi: Document pragma Loop_Invariant.
+ * sem_attr.adb (Analyze_Attribute, case Loop_Entry): This is
+ no longer an S14_Attribute.
+ * sem_prag.adb (Analyze_Pragma, case Loop_Invariant): Combine
+ processing with Assert, allow message parameter, remove call
+ to S14_Pragma.
+
+2013-04-24 Thomas Quinot <quinot@adacore.com>
+
+ * exp_ch4.adb: Minor reformatting.
+
2013-04-24 Ed Schonberg <schonberg@adacore.com>
* sem_ch7.adb (Swap_Private_Dependents): New internal routine
-- Local variables
- Dtyp : constant Entity_Id := Available_View (Designated_Type (PtrT));
+ Dtyp : constant Entity_Id := Available_View (Designated_Type (PtrT));
Desig : Entity_Id;
Nod : Node_Id;
Pool : Entity_Id;
* Pragma Linker_Destructor::
* Pragma Linker_Section::
* Pragma Long_Float::
+* Pragma Loop_Invariant::
* Pragma Loop_Optimize::
* Pragma Loop_Variant::
* Pragma Machine_Attribute::
* Pragma Linker_Destructor::
* Pragma Linker_Section::
* Pragma Long_Float::
+* Pragma Loop_Invariant::
* Pragma Loop_Optimize::
* Pragma Loop_Variant::
* Pragma Machine_Attribute::
@cite{DEC Ada Language Reference Manual}, section 3.5.7b. Note that to use
this pragma, the standard runtime libraries must be recompiled.
+@node Pragma Loop_Invariant
+@unnumberedsec Pragma Loop_Invariant
+@findex Loop_Invariant
+@noindent
+Syntax:
+@smallexample @c ada
+pragma Loop_Invariant ( boolean_EXPRESSION );
+
+@end smallexample
+
+@noindent
+The effect of this pragma is similar to that of pragma @code{Assert},
+except that in an @code{Assertion_Policy} pragma, the identifier
+@code{Loop_Invariant} is used to control whether it is ignored or checked
+(or disabled).
+
+@code{Loop_Invariant} can only appear as one of the items in the sequence
+of statements of a loop body. The intention is that it be used to
+represent a "loop invariant" assertion, i.e. something that is true each
+time through the loop, and which can be used to show that the loop is
+achieving its purpose.
+
+To aid in writing such invariants, the special attribute @code{Loop_Entry}
+may be used to refer to the value of an expression on entry to the loop. This
+attribute can only be used within the expression of a @code{Loop_Invariant}
+pragma. For full details, see documentation of attribute @code{Loop_Entry}.
+
@node Pragma Loop_Optimize
@unnumberedsec Pragma Loop_Optimize
@findex Loop_Optimize
procedure S14_Attribute;
-- Called for all attributes defined for formal verification to check
-- that the S14_Extensions flag is set.
+ -- Bad name ???
+ -- No such thing as S14_Extensions flag ???
procedure Standard_Attribute (Val : Int);
-- Used to process attributes whose prefix is package Standard which
-- expression list. Instead, all available expressions are stored as
-- indexed components.
- S14_Attribute;
-
-- When the attribute is part of an indexed component, find the first
-- expression as it will determine the semantics of 'Loop_Entry.
Set_Known_To_Have_Preelab_Init
(Def_Id, Known_To_Have_Preelab_Init (T));
- -- private subtypes may have private dependents.
+ -- Private subtypes may have private dependents
Set_Private_Dependents (Def_Id, New_Elmt_List);
-- same for its private dependents under proper visibility conditions.
-- When compiling a grand-chid unit this needs to be done recursively.
+ -----------------------------
+ -- Swap_Private_Dependents --
+ -----------------------------
+
procedure Swap_Private_Dependents (Priv_Deps : Elist_Id) is
Deps : Elist_Id;
Priv : Entity_Id;
begin
Priv_Elmt := First_Elmt (Priv_Deps);
-
while Present (Priv_Elmt) loop
Priv := Node (Priv_Elmt);
- -- Before the exchange, verify that the presence of the
- -- Full_View field. It will be empty if the entity has already
- -- been installed due to a previous call.
+ -- Before the exchange, verify that the presence of the Full_View
+ -- field. This field will be empty if the entity has already been
+ -- installed due to a previous call.
if Present (Full_View (Priv))
and then Is_Visible_Dependent (Priv)
Is_Priv := False;
end if;
- -- For each subtype that is swapped, we also swap the
- -- reference to it in Private_Dependents, to allow access
- -- to it when we swap them out in End_Package_Scope.
+ -- For each subtype that is swapped, we also swap the reference
+ -- to it in Private_Dependents, to allow access to it when we
+ -- swap them out in End_Package_Scope.
Replace_Elmt (Priv_Elmt, Full_View (Priv));
Exchange_Declarations (Priv);
Set_Is_Potentially_Use_Visible
(Priv, Is_Potentially_Use_Visible (Node (Priv_Elmt)));
- -- Within a child unit, recurse.
+ -- Within a child unit, recurse
if Is_Priv
and then Is_Child_Unit (Cunit_Entity (Current_Sem_Unit))
end loop;
end Swap_Private_Dependents;
+ -- Start processing for Install_Private_Declarations
+
begin
-- First exchange declarations for private types, so that the full
-- declaration is visible. For each private type, we check its
-- Private_Dependents list and also exchange any subtypes of or derived
-- types from it. Finally, if this is a Taft amendment type, the
-- incomplete declaration is irrelevant, and we want to link the
- -- eventual full declaration with the original private one so we also
- -- skip the exchange.
+ -- eventual full declaration with the original private one so we
+ -- also skip the exchange.
Id := First_Entity (P);
while Present (Id) and then Id /= First_Private_Entity (P) loop
and then Scope (Full_View (Id)) = Scope (Id)
and then Ekind (Full_View (Id)) /= E_Incomplete_Type
then
- -- If there is a use-type clause on the private type, set the
- -- full view accordingly.
+ -- If there is a use-type clause on the private type, set the full
+ -- view accordingly.
Set_In_Use (Full_View (Id), In_Use (Id));
Full := Full_View (Id);
-- from another private type which is not private anymore. This
-- can only happen in a package nested within a child package,
-- when the parent type is defined in the parent unit. At this
- -- point the current type is not private either, and we have to
- -- install the underlying full view, which is now visible. Save
- -- the current full view as well, so that all views can be
+ -- point the current type is not private either, and we have
+ -- to install the underlying full view, which is now visible.
+ -- Save the current full view as well, so that all views can be
-- restored on exit. It may seem that after compiling the child
-- body there are not environments to restore, but the back-end
-- expects those links to be valid, and freeze nodes depend on
else
declare
Prev : Entity_Id;
-
begin
Prev := Find_Type_Name (N);
pragma Assert (Prev = Id
end if;
end Annotate;
- ----------------------------------
- -- Assert/Assert_And_Cut/Assume --
- ----------------------------------
+ -------------------------------------------------
+ -- Assert/Assert_And_Cut/Assume/Loop_Invariant --
+ -------------------------------------------------
-- pragma Assert
-- ( [Check => ] Boolean_EXPRESSION
-- ( [Check => ] Boolean_EXPRESSION
-- [, [Message =>] Static_String_EXPRESSION]);
+ -- pragma Loop_Invariant
+ -- ( [Check => ] Boolean_EXPRESSION
+ -- [, [Message =>] Static_String_EXPRESSION]);
+
when Pragma_Assert |
Pragma_Assert_And_Cut |
- Pragma_Assume =>
+ Pragma_Assume |
+ Pragma_Loop_Invariant =>
Assert : declare
Expr : Node_Id;
Newa : List_Id;
begin
+ -- Assert is an Ada 2005 RM-defined pragma
+
if Prag_Id = Pragma_Assert then
Ada_2005_Pragma;
- else -- Pragma_Assert_And_Cut
+
+ -- The remaining ones are GNAT pragmas
+
+ else
GNAT_Pragma;
end if;
Check_Arg_Order ((Name_Check, Name_Message));
Check_Optional_Identifier (Arg1, Name_Check);
- -- We treat pragma Assert[_And_Cut] as equivalent to:
+ -- Special processing for Loop_Invariant
- -- pragma Check (Assert[_And_Cut], condition [, msg]);
+ if Prag_Id = Pragma_Loop_Invariant then
- -- So rewrite pragma in this manner, transfer the message
- -- argument if present, and analyze the result
+ -- Check restricted placement, must be within a loop
- -- Pragma Assert_And_Cut is treated exactly like pragma Assert by
- -- the frontend. Formal verification tools may use it to "cut" the
- -- paths through the code, to make verification tractable. When
- -- dealing with a semantically analyzed tree, the information that
- -- a Check node N corresponds to a source Assert_And_Cut pragma
- -- can be retrieved from the pragma kind of Original_Node(N).
+ Check_Loop_Pragma_Placement;
+
+ -- Do preanalyze to deal with embedded Loop_Entry attribute
+
+ Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean);
+ end if;
+
+ -- Implement Assert[_And_Cut]/Assume/Loop_Invariant by generating
+ -- a corresponding Check pragma:
+
+ -- pragma Check (name, condition [, msg]);
+
+ -- Where name is the identifier matching the pragma name. So
+ -- rewrite pragma in this manner, transfer the message argument
+ -- if present, and analyze the result
+
+ -- Note: When dealing with a semantically analyzed tree, the
+ -- information that a Check node N corresponds to a source Assert,
+ -- Assume, or Assert_And_Cut pragma can be retrieved from the
+ -- pragma kind of Original_Node(N).
Expr := Get_Pragma_Arg (Arg1);
Newa := New_List (
Set_Standard_Fpt_Formats;
end Long_Float;
- --------------------
- -- Loop_Invariant --
- --------------------
-
- -- pragma Loop_Invariant ( boolean_EXPRESSION );
-
- when Pragma_Loop_Invariant => Loop_Invariant : declare
- begin
- GNAT_Pragma;
- S14_Pragma;
- Check_Arg_Count (1);
- Check_Loop_Pragma_Placement;
-
- Preanalyze_Assert_Expression (Expression (Arg1), Any_Boolean);
-
- -- Transform pragma Loop_Invariant into equivalent pragma Check
- -- Generate:
- -- pragma Check (Loop_Invaraint, Arg1);
-
- Rewrite (N,
- Make_Pragma (Loc,
- Chars => Name_Check,
- Pragma_Argument_Associations => New_List (
- Make_Pragma_Argument_Association (Loc,
- Expression => Make_Identifier (Loc, Name_Loop_Invariant)),
- Relocate_Node (Arg1))));
-
- Analyze (N);
- end Loop_Invariant;
-
-------------------
-- Loop_Optimize --
-------------------
projects / gcc.git / commitdiff