Patchwork [Ada] Crash when processing attribute Loop_Entry

login
register
mail settings
Submitter Arnaud Charlet
Date Feb. 6, 2013, 10:20 a.m.
Message ID <20130206102021.GA23863@adacore.com>
Download mbox | patch
Permalink /patch/218532/
State New
Headers show

Comments

Arnaud Charlet - Feb. 6, 2013, 10:20 a.m.
This patch suppresses the resolution of the prefix of attribute Loop_Entry. The
resolution still takes place after Loop_Entry has been transformed into the
initialization expression of a constant. The delay ensures that any generated
checks or temporaries are inserted before the relocated prefix.

-------------
-- Sources --
-------------

--  main.adb:

with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
   type Int_Array is array (Natural range <>) of Natural;

   procedure Process_Array (Obj : Int_Array) is
      Var : Natural := 0;
   begin
      for Index in Natural range Obj'Range loop
         Var := Var + 1;
         pragma Loop_Invariant (Obj (Obj'First + Var)'Loop_Entry >= 10);
      end loop;
      Put_Line (Integer'Image (Var));
   end Process_Array;

   X : Int_Array (1 .. 0);
begin
   Process_Array (X);
end Main;

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

$ gnatmake -q -gnat12 -gnata -gnatd.V main.adb
$ ./main
 0

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

2013-02-06  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_attr.adb (Resolve_Attribute): Do not resolve the prefix of
	Loop_Entry, instead wait until the attribute has been expanded. The
	delay ensures that any generated checks or temporaries are inserted
	before the relocated prefix.

Patch

Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 195784)
+++ sem_attr.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, 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- --
@@ -9821,6 +9821,18 @@ 
          when Attribute_Enabled =>
             null;
 
+         ----------------
+         -- Loop_Entry --
+         ----------------
+
+         --  Do not resolve the prefix of Loop_Entry, instead wait until the
+         --  attribute has been expanded (see Expand_Loop_Entry_Attributes).
+         --  The delay ensures that any generated checks or temporaries are
+         --  inserted before the relocated prefix.
+
+         when Attribute_Loop_Entry =>
+            null;
+
          --------------------
          -- Mechanism_Code --
          --------------------