[Ada] pragmas Loop_Invariant and Loop_Variant

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.

[Ada] pragmas Loop_Invariant and Loop_Variant

Commit Message

Patch