Patchwork [Ada] Compiler crash processing postcondition

mail settings
Submitter Arnaud Charlet
Date Aug. 1, 2011, 4:10 p.m.
Message ID <>
Download mbox | patch
Permalink /patch/107779/
State New
Headers show


Arnaud Charlet - Aug. 1, 2011, 4:10 p.m.
The compiler crashed processing Ada 2012 pre/post conditions
because internally generated declarations associated with the
evaluation of the preconditions located in a package spec were
not propagated to the corresponding routine in the body of the
package. After this patch the following program compiles without

package Pack is
   type Node_Id is new Integer;
   type Node_Kind is (Case_1, Case_2);
   type Node (Kind : Node_Kind := Case_1) is record
      case Kind is
         when Case_1 => null;
         when Case_2 => Case_2_Data : Node_Id;
      end case;
   end record;
end Pack;

with Ada.Containers.Vectors;
package Pack.Tables is
   function Get_Node (Id : Node_Id) return Node;
   function Get_Kind (Id : Node_Id) return Node_Kind;
   package Node_Tables is
     new Ada.Containers.Vectors (Index_Type   => Node_Id,
                                 Element_Type => Node,
                                 "="          => "=");
   Node_Table : Node_Tables.Vector;
   function Get_Node (Id : Node_Id) return Node is
      (Node_Tables.Element (Node_Table, Id));
   function Get_Kind (Id : Node_Id) return Node_Kind is
      (Get_Node (Id).Kind);
end Pack.Tables;

with Pack.Tables; use Pack.Tables;
package Pack.Fields is
   function Get_External (Id : Node_Id) return Node_Id;
   pragma Postcondition
     (case Get_Kind (Id) is
        when Case_2 => Get_External'Result = Get_Node (Id).Case_2_Data,
        when others => False);
end Pack.Fields;

package body Pack.Fields is
   function Get_External (Id : Node_Id) return Node_Id is
      N : Node_Id;
      return N;
end Pack.Fields;

Command: gcc -c -gnat12 -gnatws pack-fields.adb

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

2011-08-01  Javier Miranda  <>

	* exp_ch4.adb (Expand_N_Case_Expression): Propagate to the expanded
	code declarations inserted by Insert_Actions in each alternative of the
	N_Case_Expression node.


Index: exp_ch4.adb
--- exp_ch4.adb	(revision 177053)
+++ exp_ch4.adb	(working copy)
@@ -4018,6 +4018,11 @@ 
             Aloc : constant Source_Ptr := Sloc (Aexp);
+            --  Propagate declarations inserted in the node by Insert_Actions
+            --  (for example, temporaries generated to remove side effects).
+            Append_List_To (Actions, Sinfo.Actions (Alt));
             if not Is_Scalar_Type (Typ) then
                Aexp :=
                  Make_Attribute_Reference (Aloc,