Patchwork [Ada] pragmas Loop_Invariant and Loop_Variant

login
register
mail settings
Submitter Arnaud Charlet
Date Dec. 5, 2012, 10:55 a.m.
Message ID <20121205105553.GA14079@adacore.com>
Download mbox | patch
Permalink /patch/203844/
State New
Headers show

Comments

Arnaud Charlet - Dec. 5, 2012, 10:55 a.m.
This patch splits pragma Loop_Assertion into two distinct pragmas. They have
the following syntax:

   pragma Loop_Invariant ( boolean_EXPRESSION );

   pragma Loop_Variant
          ( LOOP_VARIANT_ITEM {, LOOP_VARIANT_ITEM } );

   LOOP_VARIANT_ITEM ::= CHANGE_DIRECTION => discrete_EXPRESSION

   CHANGE_DIRECTION ::= Increases | Decreases

The pragmas must appear inside a loop statement and occur immediately within
the statements of the loop. Both pragmas must have at least one argument.

The expression of pragma Loop_Invariant is checked at each iteration of the
related loop. The loop_variant_items of pragma Loop_Variant are checked in
lexicographic order starting from the first such argument and proceeding in
order of declarations at the second and all subsequent iterations of the loop.
A comparison is made between the old values of the expressions from the
previous iteration and the current values. If the growth pattern does not
follow the proper change mode, an assertion failure is raised.

------------
-- Source --
------------

--  counters.ads

package Counters is
   type Change_Mode is
     (Increase, Increase_Then_Decrease, Same, Decrease, Decrease_Then_Increase);

   type Counter (Mode : Change_Mode; Ticks : Natural) is private;

   procedure Tick (C : in out Counter);
   function Value (C : Counter) return Integer;
private
   type Counter (Mode : Change_Mode; Ticks : Natural) is record
      C : Integer := 0;
      T : Natural := 0;
   end record;
end Counters;

--  counters.adb

package body Counters is
   procedure Tick (C : in out Counter) is
      M : Change_Mode renames C.Mode;
   begin
      C.T := C.T + 1;
      if M = Increase then
         C.C := C.C + 1;
      elsif M = Increase_Then_Decrease then
         if C.T >= C.Ticks then
            C.C := C.C - 1;
         else
            C.C := C.C + 1;
         end if;
      elsif M = Decrease then
         C.C := C.C - 1;
      elsif M = Decrease_Then_Increase then
         if C.T >= C.Ticks then
            C.C := C.C + 1;
         else
            C.C := C.C - 1;
         end if;
      end if;
   end Tick;

   function Value (C : Counter) return Integer is
   begin
      return C.C;
   end Value;
end Counters;

--  main.adb

with Ada.Text_IO; use Ada.Text_IO;
with Counters;    use Counters;

procedure Main is
   function Factorial (Val : Natural) return Natural is
   begin
      if Val = 1 then
         return 1;
      else
         return Factorial (Val - 1) * Val;
      end if;
   end Factorial;
begin
   declare
      C1 : Counter (Same, 3);
      C2 : Counter (Increase_Then_Decrease, 2);
      C3 : Counter (Increase, 3);
   begin
      for J in 1 .. 3 loop
         Put_Line ("Iteration:" & J'Img);
         Tick (C1);
         Tick (C2);
         Tick (C3);
         pragma Loop_Variant
           (Invariant => Factorial (4) = 24,
            Increases => Value (C1),
            Increases => Value (C2),
            Increases => Value (C3));
      end loop;
      Put_Line ("ERROR: should not get here");
   exception
      when others => Put_Line ("OK");
   end;
end Main;

----------------------------
-- Compilation and output --
----------------------------

$ gnatmake -q -gnata -gnatd.V main.adb
$ ./main
$ 1
$ 2
$ OK

Tested on x86_64-pc-linux-gnu, committed on trunk

2012-12-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_prag.adb (Expand_N_Pragma): Add a call to expand
	pragma Loop_Variant.
	(Expand_Pragma_Loop_Assertion): Removed.
	(Expand_Pragma_Loop_Variant): New routine.
	* par-prag.adb: Remove Pragma_Loop_Assertion and add two new
	Pragma_Loop_Invariant and Pragma_Loop_Variant entries.
	* sem_attr.adb (Analyze_Attribute): Update the code which
	locates the enclosing pragma.
	* sem_prag.adb (Analyze_Pragma): Remove the code which analyzes
	pragma Loop_Assertion as the pragma is now obsolete. Add the
	machinery to checks the semantics of pragmas Loop_Invariant
	and Loop_Variant.
	(Check_Loop_Invariant_Variant_Placement): New routine.
	* snames.ads-tmpl: Remove name Loop_Assertion. Add new names
	Loop_Invariant and Loop_Variant.  Rename Name_Decreasing
	to Name_Decreases and Name_Increasing to Name_Increases.
	Remove the pragma Id for Loop_Assertion and add two new Ids for
	Loop_Invariant and Loop_Variant.

Patch

Index: exp_prag.adb
===================================================================
--- exp_prag.adb	(revision 194188)
+++ exp_prag.adb	(working copy)
@@ -69,7 +69,7 @@ 
    procedure Expand_Pragma_Import_Export_Exception (N : Node_Id);
    procedure Expand_Pragma_Inspection_Point        (N : Node_Id);
    procedure Expand_Pragma_Interrupt_Priority      (N : Node_Id);
-   procedure Expand_Pragma_Loop_Assertion          (N : Node_Id);
+   procedure Expand_Pragma_Loop_Variant            (N : Node_Id);
    procedure Expand_Pragma_Psect_Object            (N : Node_Id);
    procedure Expand_Pragma_Relative_Deadline       (N : Node_Id);
 
@@ -191,8 +191,8 @@ 
             when Pragma_Interrupt_Priority =>
                Expand_Pragma_Interrupt_Priority (N);
 
-            when Pragma_Loop_Assertion =>
-               Expand_Pragma_Loop_Assertion (N);
+            when Pragma_Loop_Variant =>
+               Expand_Pragma_Loop_Variant (N);
 
             when Pragma_Psect_Object =>
                Expand_Pragma_Psect_Object (N);
@@ -795,20 +795,19 @@ 
       end if;
    end Expand_Pragma_Interrupt_Priority;
 
-   ----------------------------------
-   -- Expand_Pragma_Loop_Assertion --
-   ----------------------------------
+   --------------------------------
+   -- Expand_Pragma_Loop_Variant --
+   --------------------------------
 
-   --  Pragma Loop_Assertion is expanded in the following manner:
+   --  Pragma Loop_Variant is expanded in the following manner:
 
    --  Original code
 
    --     for | while ... loop
    --        <preceding source statements>
-   --        pragma Loop_Assertion
-   --           (Invariant => Invar_Expr,
-   --            Variant   => (Increasing => Incr_Expr,
-   --                          Decreasing => Decr_Expr));
+   --        pragma Loop_Variant
+   --                 (Increases => Incr_Expr,
+   --                  Decreases => Decr_Expr);
    --        <succeeding source statements>
    --     end loop;
 
@@ -823,8 +822,6 @@ 
    --     for | while ... loop
    --        <preceding source statements>
 
-   --        pragma Assert (<Invar_Expr>);
-
    --        if Flag then
    --           Old_1 := Curr_1;
    --           Old_2 := Curr_2;
@@ -846,7 +843,9 @@ 
    --        <succeeding source statements>
    --     end loop;
 
-   procedure Expand_Pragma_Loop_Assertion (N : Node_Id) is
+   procedure Expand_Pragma_Loop_Variant (N : Node_Id) is
+      Last_Var    : constant Node_Id    :=
+                      Last (Pragma_Argument_Associations (N));
       Loc         : constant Source_Ptr := Sloc (N);
       Curr_Assign : List_Id   := No_List;
       Flag_Id     : Entity_Id := Empty;
@@ -854,27 +853,23 @@ 
       Loop_Scop   : Entity_Id;
       Loop_Stmt   : Node_Id;
       Old_Assign  : List_Id   := No_List;
+      Variant     : Node_Id;
 
-      procedure Process_Increase_Decrease
-        (Variant : Node_Id;
-         Is_Last : Boolean);
+      procedure Process_Variant (Variant : Node_Id; Is_Last : Boolean);
       --  Process a single increasing / decreasing termination variant. Flag
       --  Is_Last should be set when processing the last variant.
 
-      -------------------------------
-      -- Process_Increase_Decrease --
-      -------------------------------
+      ---------------------
+      -- Process_Variant --
+      ---------------------
 
-      procedure Process_Increase_Decrease
-        (Variant : Node_Id;
-         Is_Last : Boolean)
-      is
+      procedure Process_Variant (Variant : Node_Id; Is_Last : Boolean) is
          function Make_Op
            (Loc      : Source_Ptr;
             Curr_Val : Node_Id;
             Old_Val  : Node_Id) return Node_Id;
          --  Generate a comparison between Curr_Val and Old_Val depending on
-         --  the argument name (Increases / Decreases).
+         --  the change mode (Increases / Decreases) of the variant.
 
          -------------
          -- Make_Op --
@@ -885,12 +880,11 @@ 
             Curr_Val : Node_Id;
             Old_Val  : Node_Id) return Node_Id
          is
-            Modif : constant Node_Id := First (Choices (Variant));
          begin
-            if Chars (Modif) = Name_Increasing then
+            if Chars (Variant) = Name_Increases then
                return Make_Op_Gt (Loc, Curr_Val, Old_Val);
 
-            else pragma Assert (Chars (Modif) = Name_Decreasing);
+            else pragma Assert (Chars (Variant) = Name_Decreases);
                return Make_Op_Lt (Loc, Curr_Val, Old_Val);
             end if;
          end Make_Op;
@@ -898,13 +892,14 @@ 
          --  Local variables
 
          Expr     : constant Node_Id := Expression (Variant);
+         Expr_Typ : constant Entity_Id := Etype (Expr);
          Loc      : constant Source_Ptr := Sloc (Expr);
          Loop_Loc : constant Source_Ptr := Sloc (Loop_Stmt);
          Curr_Id  : Entity_Id;
          Old_Id   : Entity_Id;
          Prag     : Node_Id;
 
-      --  Start of processing for Process_Increase_Decrease
+      --  Start of processing for Process_Variant
 
       begin
          --  All temporaries generated in this routine must be inserted before
@@ -959,8 +954,7 @@ 
          Insert_Action (Loop_Stmt,
            Make_Object_Declaration (Loop_Loc,
              Defining_Identifier => Curr_Id,
-             Object_Definition   =>
-               New_Reference_To (Etype (Expr), Loop_Loc)));
+             Object_Definition   => New_Reference_To (Expr_Typ, Loop_Loc)));
 
          --  Generate:
          --    Old : <type of Expr>;
@@ -970,8 +964,7 @@ 
          Insert_Action (Loop_Stmt,
            Make_Object_Declaration (Loop_Loc,
              Defining_Identifier => Old_Id,
-             Object_Definition   =>
-               New_Reference_To (Etype (Expr), Loop_Loc)));
+             Object_Definition   => New_Reference_To (Expr_Typ, Loop_Loc)));
 
          --  Restore original scope after all temporaries have been analyzed
 
@@ -1066,13 +1059,8 @@ 
                     Right_Opnd => New_Reference_To (Old_Id, Loc)),
                 Then_Statements => New_List (Prag)));
          end if;
-      end Process_Increase_Decrease;
+      end Process_Variant;
 
-      --  Local variables
-
-      Arg   : Node_Id;
-      Invar : Node_Id := Empty;
-
    --  Start of processing for Expand_Pragma_Loop_Assertion
 
    begin
@@ -1093,76 +1081,29 @@ 
 
       Loop_Scop := Entity (Identifier (Loop_Stmt));
 
-      --  Process all pragma arguments
+      --  Create the circuitry which verifies individual variants
 
-      Arg := First (Pragma_Argument_Associations (N));
-      while Present (Arg) loop
+      Variant := First (Pragma_Argument_Associations (N));
+      while Present (Variant) loop
+         Process_Variant (Variant, Is_Last => Variant = Last_Var);
 
-         --  Termination variants appear as components in an aggregate
-
-         if Chars (Arg) = Name_Variant then
-            declare
-               Variants : constant Node_Id := Expression (Arg);
-               Last_Var : constant Node_Id :=
-                            Last (Component_Associations (Variants));
-               Variant  : Node_Id;
-
-            begin
-               Variant := First (Component_Associations (Variants));
-               while Present (Variant) loop
-                  Process_Increase_Decrease
-                    (Variant => Variant,
-                     Is_Last => Variant = Last_Var);
-
-                  Next (Variant);
-               end loop;
-            end;
-
-         --  Invariant
-
-         else
-            Invar := Expression (Arg);
-         end if;
-
-         Next (Arg);
+         Next (Variant);
       end loop;
 
-      --  Verify the invariant expression, generate:
-      --    pragma Assert (<Invar>);
-
-      --  Use the Sloc of the invariant for better error reporting
-
-      if Present (Invar) then
-         declare
-            Invar_Loc : constant Source_Ptr := Sloc (Invar);
-         begin
-            Insert_Action (N,
-              Make_Pragma (Invar_Loc,
-                Chars                        => Name_Assert,
-                Pragma_Argument_Associations => New_List (
-                  Make_Pragma_Argument_Association (Invar_Loc,
-                    Expression => Relocate_Node (Invar)))));
-         end;
-      end if;
-
       --  Construct the segment which stores the old values of all expressions.
       --  Generate:
       --    if Flag then
       --       <Old_Assign>
       --    end if;
 
-      if Present (Old_Assign) then
-         Insert_Action (N,
-           Make_If_Statement (Loc,
-             Condition       => New_Reference_To (Flag_Id, Loc),
-             Then_Statements => Old_Assign));
-      end if;
+      Insert_Action (N,
+        Make_If_Statement (Loc,
+          Condition       => New_Reference_To (Flag_Id, Loc),
+          Then_Statements => Old_Assign));
 
       --  Update the values of all expressions
 
-      if Present (Curr_Assign) then
-         Insert_Actions (N, Curr_Assign);
-      end if;
+      Insert_Actions (N, Curr_Assign);
 
       --  Add the assertion circuitry to test all changes in expressions.
       --  Generate:
@@ -1172,22 +1113,20 @@ 
       --       Flag := True;
       --    end if;
 
-      if Present (If_Stmt) then
-         Insert_Action (N,
-           Make_If_Statement (Loc,
-             Condition       => New_Reference_To (Flag_Id, Loc),
-             Then_Statements => New_List (If_Stmt),
-             Else_Statements => New_List (
-               Make_Assignment_Statement (Loc,
-                 Name       => New_Reference_To (Flag_Id, Loc),
-                 Expression => New_Reference_To (Standard_True, Loc)))));
-      end if;
+      Insert_Action (N,
+        Make_If_Statement (Loc,
+          Condition       => New_Reference_To (Flag_Id, Loc),
+          Then_Statements => New_List (If_Stmt),
+          Else_Statements => New_List (
+            Make_Assignment_Statement (Loc,
+              Name       => New_Reference_To (Flag_Id, Loc),
+              Expression => New_Reference_To (Standard_True, Loc)))));
 
       --  Note: the pragma has been completely transformed into a sequence of
       --  corresponding declarations and statements. We leave it in the tree
       --  for documentation purposes. It will be ignored by the backend.
 
-   end Expand_Pragma_Loop_Assertion;
+   end Expand_Pragma_Loop_Variant;
 
    --------------------------------
    -- Expand_Pragma_Psect_Object --
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 194199)
+++ sem_prag.adb	(working copy)
@@ -618,6 +618,10 @@ 
       --  Common processing for first argument of pragma Interrupt_Handler or
       --  pragma Attach_Handler.
 
+      procedure Check_Loop_Invariant_Variant_Placement;
+      --  Verify whether pragma Loop_Invariant or pragma Loop_Variant appear
+      --  immediately within the statements of the related loop.
+
       procedure Check_Is_In_Decl_Part_Or_Package_Spec;
       --  Check that pragma appears in a declarative part, or in a package
       --  specification, i.e. that it does not occur in a statement sequence
@@ -1912,6 +1916,44 @@ 
          end if;
       end Check_Interrupt_Or_Attach_Handler;
 
+      --------------------------------------------
+      -- Check_Loop_Invariant_Variant_Placement --
+      --------------------------------------------
+
+      procedure Check_Loop_Invariant_Variant_Placement is
+         Loop_Stmt : Node_Id;
+
+      begin
+         --  Locate the enclosing loop statement (if any)
+
+         Loop_Stmt := N;
+         while Present (Loop_Stmt) loop
+            if Nkind (Loop_Stmt) = N_Loop_Statement then
+               exit;
+
+            --  Prevent the search from going too far
+
+            elsif Nkind_In (Loop_Stmt, N_Entry_Body,
+                                       N_Package_Body,
+                                       N_Package_Declaration,
+                                       N_Protected_Body,
+                                       N_Subprogram_Body,
+                                       N_Task_Body)
+            then
+               Error_Pragma ("pragma % must appear inside a loop statement");
+               return;
+
+            else
+               Loop_Stmt := Parent (Loop_Stmt);
+            end if;
+         end loop;
+
+         if List_Containing (N) /= Statements (Loop_Stmt) then
+            Error_Pragma
+              ("pragma % must occur immediately in the statements of a loop");
+         end if;
+      end Check_Loop_Invariant_Variant_Placement;
+
       -------------------------------------------
       -- Check_Is_In_Decl_Part_Or_Package_Spec --
       -------------------------------------------
@@ -11453,74 +11495,62 @@ 
          end Long_Float;
 
          --------------------
-         -- Loop_Assertion --
+         -- Loop_Invariant --
          --------------------
 
-         --  pragma Loop_Assertion
-         --        (  [Invariant =>] boolean_Expression );
-         --     |  ( [[Invariant =>] boolean_Expression ,]
-         --            Variant   =>
-         --              ( TERMINATION_VARIANT {, TERMINATION_VARIANT ) );
+         --  pragma Loop_Invariant ( boolean_EXPRESSION );
 
-         --  TERMINATION_VARIANT ::= CHANGE_MODIFIER => discrete_EXPRESSION
+         when Pragma_Loop_Invariant => Loop_Invariant : declare
+         begin
+            GNAT_Pragma;
+            S14_Pragma;
+            Check_Arg_Count (1);
+            Check_Loop_Invariant_Variant_Placement;
 
-         --  CHANGE_MODIFIER ::= Increasing | Decreasing
+            --  Completely ignore if disabled
 
-         when Pragma_Loop_Assertion => Loop_Assertion : declare
-            procedure Check_Variant (Arg : Node_Id);
-            --  Verify the legality of a variant
+            if Check_Disabled (Pname) then
+               Rewrite (N, Make_Null_Statement (Loc));
+               Analyze (N);
+               return;
+            end if;
 
-            -------------------
-            -- Check_Variant --
-            -------------------
+            Preanalyze_And_Resolve (Expression (Arg1), Any_Boolean);
 
-            procedure Check_Variant (Arg : Node_Id) is
-               Expr : constant Node_Id := Expression (Arg);
+            --  Transform pagma Loop_Invariant into an equivalent pragma Check.
+            --  Generate:
+            --    pragma Check (Loop_Invaraint, Arg1);
 
-            begin
-               --  Variants appear in aggregate form
+            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))));
 
-               if Nkind (Expr) = N_Aggregate then
-                  declare
-                     Comp  : Node_Id;
-                     Extra : Node_Id;
-                     Modif : Node_Id;
+            Analyze (N);
+         end Loop_Invariant;
 
-                  begin
-                     Comp := First (Component_Associations (Expr));
-                     while Present (Comp) loop
-                        Modif := First (Choices (Comp));
-                        Extra := Next (Modif);
+         ------------------
+         -- Loop_Variant --
+         ------------------
 
-                        Check_Arg_Is_One_Of
-                          (Modif, Name_Decreasing, Name_Increasing);
+         --  pragma Loop_Variant
+         --         ( LOOP_VARIANT_ITEM {, LOOP_VARIANT_ITEM } );
 
-                        if Present (Extra) then
-                           Error_Pragma_Arg
-                             ("only one modifier allowed in argument", Expr);
-                        end if;
+         --  LOOP_VARIANT_ITEM ::= CHANGE_DIRECTION => discrete_EXPRESSION
 
-                        Preanalyze_And_Resolve
-                          (Expression (Comp), Any_Discrete);
+         --  CHANGE_DIRECTION ::= Increases | Decreases
 
-                        Next (Comp);
-                     end loop;
-                  end;
-               else
-                  Error_Pragma_Arg
-                    ("expression on variant must be an aggregate", Expr);
-               end if;
-            end Check_Variant;
+         when Pragma_Loop_Variant => Loop_Variant : declare
+            Variant : Node_Id;
 
-            --  Local variables
-
-            Stmt : Node_Id;
-
-         --  Start of processing for Loop_Assertion
-
          begin
             GNAT_Pragma;
             S14_Pragma;
+            Check_At_Least_N_Arguments (1);
+            Check_Loop_Invariant_Variant_Placement;
 
             --  Completely ignore if disabled
 
@@ -11530,57 +11560,22 @@ 
                return;
             end if;
 
-            --  Verify that the pragma appears inside a loop
+            --  Process all increasing / decreasing expressions
 
-            Stmt := N;
-            while Present (Stmt) and then Nkind (Stmt) /= N_Loop_Statement loop
-               Stmt := Parent (Stmt);
-            end loop;
+            Variant := First (Pragma_Argument_Associations (N));
+            while Present (Variant) loop
+               if Chars (Variant) /= Name_Decreases
+                 and then Chars (Variant) /= Name_Increases
+               then
+                  Error_Pragma_Arg ("wrong change modifier", Variant);
+               end if;
 
-            if No (Stmt) then
-               Error_Pragma ("pragma % must appear inside a loop");
-            end if;
+               Preanalyze_And_Resolve (Expression (Variant), Any_Discrete);
 
-            Check_At_Least_N_Arguments (1);
-            Check_At_Most_N_Arguments  (2);
+               Next (Variant);
+            end loop;
+         end Loop_Variant;
 
-            --  Process the first argument
-
-            if Chars (Arg1) = Name_Variant then
-               Check_Variant (Arg1);
-
-            elsif Chars (Arg1) = No_Name
-              or else Chars (Arg1) = Name_Invariant
-            then
-               Preanalyze_And_Resolve (Expression (Arg1), Any_Boolean);
-
-            else
-               Error_Pragma_Arg ("argument not allowed in pragma %", Arg1);
-            end if;
-
-            --  Process the second argument
-
-            if Present (Arg2) then
-               if Chars (Arg2) = Name_Variant then
-                  if Chars (Arg1) = Name_Variant then
-                     Error_Pragma ("only one variant allowed in pragma %");
-                  else
-                     Check_Variant (Arg2);
-                  end if;
-
-               elsif Chars (Arg2) = Name_Invariant then
-                  if Chars (Arg1) = Name_Variant then
-                     Error_Pragma_Arg ("invariant must precede variant", Arg2);
-                  else
-                     Error_Pragma ("only one invariant allowed in pragma %");
-                  end if;
-
-               else
-                  Error_Pragma_Arg ("argument not allowed in pragma %", Arg2);
-               end if;
-            end if;
-         end Loop_Assertion;
-
          -----------------------
          -- Machine_Attribute --
          -----------------------
@@ -15707,7 +15702,8 @@ 
       Pragma_Lock_Free                      => -1,
       Pragma_Locking_Policy                 => -1,
       Pragma_Long_Float                     => -1,
-      Pragma_Loop_Assertion                 => -1,
+      Pragma_Loop_Invariant                 => -1,
+      Pragma_Loop_Variant                   => -1,
       Pragma_Machine_Attribute              => -1,
       Pragma_Main                           => -1,
       Pragma_Main_Storage                   => -1,
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 194202)
+++ sem_attr.adb	(working copy)
@@ -3795,15 +3795,17 @@ 
          Stmt := N;
          while Present (Stmt) loop
 
-            --  Locate the enclosing Loop_Assertion pragma (if any). Note that
-            --  when Loop_Assertion is expanded, we must look for an Assertion
-            --  pragma.
+            --  Locate the enclosing Loop_Invariant / Loop_Variant pragma (if
+            --  any). Note that when these two are expanded, we must look for
+            --  an Assertion pragma.
 
             if Nkind (Original_Node (Stmt)) = N_Pragma
               and then
                 (Pragma_Name (Original_Node (Stmt)) = Name_Assert
                    or else
-                 Pragma_Name (Original_Node (Stmt)) = Name_Loop_Assertion)
+                 Pragma_Name (Original_Node (Stmt)) = Name_Loop_Invariant
+                   or else
+                 Pragma_Name (Original_Node (Stmt)) = Name_Loop_Variant)
             then
                In_Loop_Assertion := True;
 
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 194199)
+++ par-prag.adb	(working copy)
@@ -1189,7 +1189,8 @@ 
            Pragma_Lock_Free                      |
            Pragma_Locking_Policy                 |
            Pragma_Long_Float                     |
-           Pragma_Loop_Assertion                 |
+           Pragma_Loop_Invariant                 |
+           Pragma_Loop_Variant                   |
            Pragma_Machine_Attribute              |
            Pragma_Main                           |
            Pragma_Main_Storage                   |
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 194199)
+++ snames.ads-tmpl	(working copy)
@@ -405,7 +405,8 @@ 
    Name_License                        : constant Name_Id := N + $; -- GNAT
    Name_Locking_Policy                 : constant Name_Id := N + $;
    Name_Long_Float                     : constant Name_Id := N + $; -- VMS
-   Name_Loop_Assertion                 : constant Name_Id := N + $; -- GNAT
+   Name_Loop_Invariant                 : constant Name_Id := N + $; -- GNAT
+   Name_Loop_Variant                   : constant Name_Id := N + $; -- GNAT
    Name_No_Run_Time                    : constant Name_Id := N + $; -- GNAT
    Name_No_Strict_Aliasing             : constant Name_Id := N + $; -- GNAT
    Name_Normalize_Scalars              : constant Name_Id := N + $;
@@ -671,7 +672,7 @@ 
    Name_Component_Size_4               : constant Name_Id := N + $;
    Name_Copy                           : constant Name_Id := N + $;
    Name_D_Float                        : constant Name_Id := N + $;
-   Name_Decreasing                     : constant Name_Id := N + $;
+   Name_Decreases                      : constant Name_Id := N + $;
    Name_Descriptor                     : constant Name_Id := N + $;
    Name_Disable                        : constant Name_Id := N + $;
    Name_Dot_Replacement                : constant Name_Id := N + $;
@@ -691,7 +692,7 @@ 
    Name_GPL                            : constant Name_Id := N + $;
    Name_IEEE_Float                     : constant Name_Id := N + $;
    Name_Ignore                         : constant Name_Id := N + $;
-   Name_Increasing                     : constant Name_Id := N + $;
+   Name_Increases                      : constant Name_Id := N + $;
    Name_Info                           : constant Name_Id := N + $;
    Name_Internal                       : constant Name_Id := N + $;
    Name_Link_Name                      : constant Name_Id := N + $;
@@ -1686,7 +1687,8 @@ 
       Pragma_License,
       Pragma_Locking_Policy,
       Pragma_Long_Float,
-      Pragma_Loop_Assertion,
+      Pragma_Loop_Invariant,
+      Pragma_Loop_Variant,
       Pragma_No_Run_Time,
       Pragma_No_Strict_Aliasing,
       Pragma_Normalize_Scalars,