[Ada] Subprogram contracts on generics

This is a multi purpose patch concerning the contracts on subprograms.

  * The patch implements "instantiatable contracts", in other words SPARK-
  related contract annotations can now appear on generic subprogram and be
  instantiated as part of the subprogram instantiation.

  * The patch removes multiple kludges for ASIS.

  * The patch removes multiple kludges concerning the analysis and global
  reference storage for contracts related to generic subprograms.

  * The patch fixes multiple issies with respect to contracts on subprograms
  and subprogram bodies that act as compilation units.

  * The patch cleans up a lot of dubious and fragmented code.

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

--  body_and_spec.ads

with Refs;

function Body_And_Spec (Input : Integer) return Integer
  with Pre  => Input + Refs.External_Zero > 1,
       Post => Body_And_Spec'Result + Refs.External_Zero > 5;

--  body_and_spec.adb

function Body_And_Spec (Input : Integer) return Integer is
begin
   return Input + 1;
end Body_And_Spec;

--  body_and_spec_pragmas.ads

with Refs;

function Body_And_Spec_Pragmas (Input : Integer) return Integer;
pragma Precondition  (Input + Refs.External_Zero > 1);
pragma Postcondition (Body_And_Spec_Pragmas'Result + Refs.External_Zero > 5);

--  body_and_spec_pragmas.adb

function Body_And_Spec_Pragmas (Input : Integer) return Integer is
   pragma Precondition  (Input + Refs.External_Zero > 2);
   pragma Postcondition (Body_And_Spec_Pragmas'Result + Refs.External_Zero > 4);
begin
   return Input + 1;
end Body_And_Spec_Pragmas;

--  body_only.adb

with Refs;

function Body_Only (Input : Integer) return Integer
  with Pre  => Input + Refs.External_Zero > 2,
       Post => Body_Only'Result + Refs.External_Zero > 4
is
begin
   return Input + 1;
end Body_Only;

--  body_only_pragmas.adb

function Body_Only_Pragmas (Input : Integer) return Integer is
   pragma Pre  (Input > 2);
   pragma Post (Body_Only_Pragmas'Result > 4);
begin
   return Input + 1;
end Body_Only_Pragmas;

--  gen_body_and_spec.ads

with Refs;

generic
   Zero : Integer;

function Gen_Body_And_Spec (Input : Integer) return Integer
  with Pre  => Input + Zero + Refs.External_Zero > 1,
       Post => Gen_Body_And_Spec'Result + Zero + Refs.External_Zero > 5;

--  gen_body_and_spec.adb

function Gen_Body_And_Spec (Input : Integer) return Integer is
begin
   return Input + 1;
end Gen_Body_And_Spec;

--  gen_body_and_spec_pragmas.ads

with Refs;

generic
   Zero : Integer;

function Gen_Body_And_Spec_Pragmas (Input : Integer) return Integer;
pragma Precondition (Input + Zero + Refs.External_Zero > 1);
pragma Postcondition
  (Gen_Body_And_Spec_Pragmas'Result + Zero + Refs.External_Zero > 5);

--  gen_body_and_spec_pragmas.adb

function Gen_Body_And_Spec_Pragmas (Input : Integer) return Integer is
   pragma Precondition (Input + Zero + Refs.External_Zero > 2);
   pragma Postcondition
     (Gen_Body_And_Spec_Pragmas'Result + Zero + Refs.External_Zero > 4);
begin
   return Input + 1;
end Gen_Body_And_Spec_Pragmas;

--  gen_pack.ads

with Refs;

generic
   Zero : Integer;

package Gen_Pack is
   function Func (Input : Integer) return Integer
     with Pre  => Input + Zero + Refs.External_Zero > 1,
          Post => Func'Result + Zero + Refs.External_Zero  > 5;
end Gen_Pack;

--  gen_pack.adb

package body Gen_Pack is
   function Func (Input : Integer) return Integer is
   begin
      return Input + 1;
   end Func;
end Gen_Pack;

--  gen_pack_gen.ads

with Refs;

generic
   Zero : Integer;

package Gen_Pack_Gen is
   generic
      Local_Zero : Integer;

   function Func (Input : Integer) return Integer
     with Pre  => Input + Zero + Local_Zero + Refs.External_Zero > 1,
          Post => Func'Result + Zero + Local_Zero + Refs.External_Zero  > 5;
end Gen_Pack_Gen;

--  gen_pack_gen.adb

package body Gen_Pack_Gen is
   function Func (Input : Integer) return Integer is
   begin
      return Input + 1;
   end Func;
end Gen_Pack_Gen;

--  gen_pack_gen_pragmas.ads

with Refs;

generic
   Zero : Integer;

package Gen_Pack_Gen_Pragmas is
   generic
      Local_Zero : Integer;

   function Func (Input : Integer) return Integer;
   pragma Precondition (Input + Zero + Local_Zero + Refs.External_Zero > 1);
   pragma Postcondition
     (Func'Result + Zero + Local_Zero + Refs.External_Zero  > 5);
end Gen_Pack_Gen_Pragmas;

--  gen_pack_gen_pragmas.adb

package body Gen_Pack_Gen_Pragmas is
   function Func (Input : Integer) return Integer is
      pragma Precondition (Input + Zero + Local_Zero + Refs.External_Zero > 2);
      pragma Postcondition
        (Func'Result + Zero + Local_Zero + Refs.External_Zero  > 4);
   begin
      return Input + 1;
   end Func;
end Gen_Pack_Gen_Pragmas;

--  gen_pack_pragmas.ads

with Refs;

generic
   Zero : Integer;

package Gen_Pack_Pragmas is
   function Func (Input : Integer) return Integer;
   pragma Precondition  (Input + Zero + Refs.External_Zero > 1);
   pragma Postcondition (Func'Result + Zero + Refs.External_Zero  > 5);
end Gen_Pack_Pragmas;

--  gen_pack_pragmas.adb

package body Gen_Pack_Pragmas is
   function Func (Input : Integer) return Integer is
      pragma Precondition  (Input + Zero + Refs.External_Zero > 2);
      pragma Postcondition (Func'Result + Zero + Refs.External_Zero  > 4);
   begin
      return Input + 1;
   end Func;
end Gen_Pack_Pragmas;

--  pack.ads

with Refs;

package Pack is
   function Func (Input : Integer) return Integer
     with Pre  => Input + Refs.External_Zero > 1,
          Post => Func'Result + Refs.External_Zero > 5;
end Pack;

--  pack.adb

package body Pack is
   function Func (Input : Integer) return Integer is
   begin
      return Input + 1;
   end Func;
end Pack;

--  pack_gen.ads

with Refs;

package Pack_Gen is
   generic
      Zero : Integer;

   function Func (Input : Integer) return Integer
     with Pre  => Input + Zero + Refs.External_Zero > 1,
          Post => Func'Result + Zero + Refs.External_Zero > 5;
end Pack_Gen;

--  pack_gen.adb

package body Pack_Gen is
   function Func (Input : Integer) return Integer is
   begin
      return Input + 1;
   end Func;
end Pack_Gen;

--  pack_gen_pragmas.ads

with Refs;

package Pack_Gen_Pragmas is
   generic
      Zero : Integer;

   function Func (Input : Integer) return Integer;
   pragma Precondition  (Input + Zero + Refs.External_Zero > 1);
   pragma Postcondition (Func'Result + Zero + Refs.External_Zero > 5);
end Pack_Gen_Pragmas;

--  pack_gen_pragmas.adb

package body Pack_Gen_Pragmas is
   function Func (Input : Integer) return Integer is
      pragma Precondition  (Input + Zero + Refs.External_Zero > 2);
      pragma Postcondition (Func'Result + Zero + Refs.External_Zero > 4);
   begin
      return Input + 1;
   end Func;
end Pack_Gen_Pragmas;

--  pack_pragmas.ads

with Refs;

package Pack_Pragmas is
   function Func (Input : Integer) return Integer;
   pragma Precondition  (Input + Refs.External_Zero > 1);
   pragma Postcondition (Func'Result + Refs.External_Zero > 5);
end Pack_Pragmas;

--  pack_pragmas.adb

package body Pack_Pragmas is
   function Func (Input : Integer) return Integer is
      pragma Precondition  (Input + Refs.External_Zero > 2);
      pragma Postcondition (Func'Result + Refs.External_Zero > 4);
   begin
      return Input + 1;
   end Func;
end Pack_Pragmas;

--  refs.ads

package Refs is
   External_Zero : Integer := 0;
end Refs;

--  main.adb

with Ada.Assertions; use Ada.Assertions;
with Ada.Exceptions; use Ada.Exceptions;
with Ada.Text_IO;    use Ada.Text_IO;
with Body_And_Spec;
with Body_And_Spec_Pragmas;
with Body_Only;
with Body_Only_Pragmas;
with Gen_Body_And_Spec;
with Gen_Body_And_Spec_Pragmas;
with Gen_Pack;
with Gen_Pack_Pragmas;
with Gen_Pack_Gen;
with Gen_Pack_Gen_Pragmas;
with Pack;
with Pack_Pragmas;
with Pack_Gen;
with Pack_Gen_Pragmas;

procedure Main is
   Fail_Spec_Pre  : constant Integer := 1;
   Fail_Body_Pre  : constant Integer := 2;
   Fail_Body_Post : constant Integer := 3;
   Fail_Spec_Post : constant Integer := 4;
   OK             : constant Integer := 5;

   Result : Integer;

begin
   --  Aspects, body + spec

   begin
      Result := Body_And_Spec (Fail_Spec_Pre);
      Put_Line ("ERROR 1: spec precondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 1 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 1: unexpected exception");
   end;

   begin
      Result := Body_And_Spec (Fail_Spec_Post);
      Put_Line ("ERROR 2: spec postcondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 2 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 2: unexpected exception");
   end;

   begin
      Result := Body_And_Spec (OK);
      Put_Line ("OK 3");
   exception
      when others => Put_Line ("ERROR 3: unexpected exception");
   end;

   --  Pragmas, body + spec

   begin
      Result := Body_And_Spec_Pragmas (Fail_Spec_Pre);
      Put_Line ("ERROR 4: spec precondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 4 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 4: unexpected exception");
   end;

   begin
      Result := Body_And_Spec_Pragmas (Fail_Body_Pre);
      Put_Line ("ERROR 5: body precondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 5 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 5: unexpected exception");
   end;

   begin
      Result := Body_And_Spec_Pragmas (Fail_Body_Post);
      Put_Line ("ERROR 6: body postcondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 6 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 6: unexpected exception");
   end;

   begin
      Result := Body_And_Spec_Pragmas (Fail_Spec_Post);
      Put_Line ("ERROR 7: spec postcondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 7 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 7: unexpected exception");
   end;

   begin
      Result := Body_And_Spec_Pragmas (OK);
      Put_Line ("OK 8");
   exception
      when others => Put_Line ("ERROR 8: unexpected exception");
   end;

   --  Aspects, body

   begin
      Result := Body_Only (Fail_Body_Pre);
      Put_Line ("ERROR 9: body precondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 9 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 9: unexpected exception");
   end;

   begin
      Result := Body_Only (Fail_Body_Post);
      Put_Line ("ERROR 10: body postcondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 10 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 10: unexpected exception");
   end;

   begin
      Result := Body_Only (OK);
      Put_Line ("OK 11");
   exception
      when others => Put_Line ("ERROR 11: unexpected exception");
   end;

   --  Pragmas, body

   begin
      Result := Body_Only_Pragmas (Fail_Body_Pre);
      Put_Line ("ERROR 12: body precondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 12 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 12: unexpected exception");
   end;

   begin
      Result := Body_Only_Pragmas (Fail_Body_Post);
      Put_Line ("ERROR 13: body postcondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 13 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 13: unexpected exception");
   end;

   begin
      Result := Body_Only_Pragmas (OK);
      Put_Line ("OK 14");
   exception
      when others => Put_Line ("ERROR 14: unexpected exception");
   end;

   --  Aspects, generic function

   declare
      function Func_Inst is new Gen_Body_And_Spec (0);
   begin
      begin
         Result := Func_Inst (Fail_Spec_Pre);
         Put_Line ("ERROR 15: spec precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 15 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 15: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Spec_Post);
         Put_Line ("ERROR 16: spec postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 16 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 16: unexpected exception");
      end;

      begin
         Result := Func_Inst (OK);
         Put_Line ("OK 17");
      exception
         when others => Put_Line ("ERROR 17: unexpected exception");
      end;
   end;

   --  Pragmas, generic function

   declare
      function Func_Inst is new Gen_Body_And_Spec_Pragmas (0);
   begin
      begin
         Result := Func_Inst (Fail_Spec_Pre);
         Put_Line ("ERROR 18: spec precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 18 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 18: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Body_Pre);
         Put_Line ("ERROR 19: body precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 19 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 19: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Body_Post);
         Put_Line ("ERROR 20: body postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 20 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 20: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Spec_Post);
         Put_Line ("ERROR 21: spec postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 21 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 21: unexpected exception");
      end;

      begin
         Result := Func_Inst (OK);
         Put_Line ("OK 22");
      exception
         when others => Put_Line ("ERROR 22: unexpected exception");
      end;
   end;

   --  Aspects, function in generic package

   declare
      package Pack_Inst is new Gen_Pack (0);
   begin
      begin
         Result := Pack_Inst.Func (Fail_Spec_Pre);
         Put_Line ("ERROR 23: spec precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 23 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 23: unexpected exception");
      end;

      begin
         Result := Pack_Inst.Func (Fail_Spec_Post);
         Put_Line ("ERROR 24: spec postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 24 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 24: unexpected exception");
      end;

      begin
         Result := Pack_Inst.Func (OK);
         Put_Line ("OK 25");
      exception
         when others => Put_Line ("ERROR 25: unexpected exception");
      end;
   end;

   --  Pragmas, function in generic package

   declare
      package Pack_Inst is new Gen_Pack_Pragmas (0);
   begin
      begin
         Result := Pack_Inst.Func (Fail_Spec_Pre);
         Put_Line ("ERROR 26: spec precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 26 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 26: unexpected exception");
      end;

      begin
         Result := Pack_Inst.Func (Fail_Body_Pre);
         Put_Line ("ERROR 27: body precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 27 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 27: unexpected exception");
      end;

      begin
         Result := Pack_Inst.Func (Fail_Body_Post);
         Put_Line ("ERROR 28: body postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 28 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 28: unexpected exception");
      end;

      begin
         Result := Pack_Inst.Func (Fail_Spec_Post);
         Put_Line ("ERROR 29: spec postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 29 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 29: unexpected exception");
      end;

      begin
         Result := Pack_Inst.Func (OK);
         Put_Line ("OK 30");
      exception
         when others => Put_Line ("ERROR 30: unexpected exception");
      end;
   end;

   --  Aspects, generic function in generic package

   declare
      package  Pack_Inst is new Gen_Pack_Gen (0);
      function Func_Inst is new Pack_Inst.Func (0);
   begin
      begin
         Result := Func_Inst (Fail_Spec_Pre);
         Put_Line ("ERROR 31: spec precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 31 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 31: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Spec_Post);
         Put_Line ("ERROR 32: spec postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 32 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 32: unexpected exception");
      end;

      begin
         Result := Func_Inst (OK);
         Put_Line ("OK 33");
      exception
         when others => Put_Line ("ERROR 33: unexpected exception");
      end;
   end;

   --  Pragmas, generic function in generic package

   declare
      package  Pack_Inst is new Gen_Pack_Gen_Pragmas (0);
      function Func_Inst is new Pack_Inst.Func (0);
   begin
      begin
         Result := Func_Inst (Fail_Spec_Pre);
         Put_Line ("ERROR 34: spec precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 34 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 34: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Body_Pre);
         Put_Line ("ERROR 35: body precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 35 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 35: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Body_Post);
         Put_Line ("ERROR 36: body postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 36 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 36: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Spec_Post);
         Put_Line ("ERROR 37: spec postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 37 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 37: unexpected exception");
      end;

      begin
         Result := Func_Inst (OK);
         Put_Line ("OK 38");
      exception
         when others => Put_Line ("ERROR 35: unexpected exception");
      end;
   end;

   --  Aspects, function in package

   begin
      Result := Pack.Func (Fail_Spec_Pre);
      Put_Line ("ERROR 39: spec precondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 39 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 39: unexpected exception");
   end;

   begin
      Result := Pack.Func (Fail_Spec_Post);
      Put_Line ("ERROR 40: spec postcondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 40 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 40: unexpected exception");
   end;

   begin
      Result := Pack.Func (OK);
      Put_Line ("OK 41");
   exception
      when others => Put_Line ("ERROR 41: unexpected exception");
   end;

   --  Pragmas, function in package

   begin
      Result := Pack_Pragmas.Func (Fail_Spec_Pre);
      Put_Line ("ERROR 42: spec precondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 42 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 42: unexpected exception");
   end;

   begin
      Result := Pack_Pragmas.Func (Fail_Body_Pre);
      Put_Line ("ERROR 43: body precondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 43 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 43: unexpected exception");
   end;

   begin
      Result := Pack_Pragmas.Func (Fail_Body_Post);
      Put_Line ("ERROR 44: body postcondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 44 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 44: unexpected exception");
   end;

   begin
      Result := Pack_Pragmas.Func (Fail_Spec_Post);
      Put_Line ("ERROR 45: spec postcondition did not fail");
   exception
      when AE : Assertion_Error =>
         Put_Line ("OK 45 " & Exception_Message (AE));
      when others               =>
         Put_Line ("ERROR 45: unexpected exception");
   end;

   begin
      Result := Pack_Pragmas.Func (OK);
      Put_Line ("OK 46");
   exception
      when others => Put_Line ("ERROR 46: unexpected exception");
   end;

   --  Aspects, generic function in package

   declare
      function Func_Inst is new Pack_Gen.Func (0);
   begin
      begin
         Result := Func_Inst (Fail_Spec_Pre);
         Put_Line ("ERROR 47: spec precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 47 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 47: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Spec_Post);
         Put_Line ("ERROR 48: spec postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 48 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 48: unexpected exception");
      end;

      begin
         Result := Func_Inst (OK);
         Put_Line ("OK 49");
      exception
         when others => Put_Line ("ERROR 41: unexpected exception");
      end;
   end;

   --  Pragmas, generic function in package

   declare
      function Func_Inst is new Pack_Gen_Pragmas.Func (0);
   begin
      begin
         Result := Func_Inst (Fail_Spec_Pre);
         Put_Line ("ERROR 50: spec precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 50 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 50: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Body_Pre);
         Put_Line ("ERROR 51: body precondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 51 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 51: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Body_Post);
         Put_Line ("ERROR 52: body postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 52 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 52: unexpected exception");
      end;

      begin
         Result := Func_Inst (Fail_Spec_Post);
         Put_Line ("ERROR 53: spec postcondition did not fail");
      exception
         when AE : Assertion_Error =>
            Put_Line ("OK 53 " & Exception_Message (AE));
         when others               =>
            Put_Line ("ERROR 53: unexpected exception");
      end;

      begin
         Result := Func_Inst (OK);
         Put_Line ("OK 54");
      exception
         when others => Put_Line ("ERROR 54: unexpected exception");
      end;
   end;
end Main;

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

$ gnatmake -q -gnata main.adb
$ ./main
OK 1 failed precondition from body_and_spec.ads:4
OK 2 failed postcondition from body_and_spec.ads:5
OK 3
OK 4 failed precondition from body_and_spec_pragmas.ads:4
OK 5 failed precondition from body_and_spec_pragmas.adb:2
OK 6 failed postcondition from body_and_spec_pragmas.adb:3
OK 7 failed postcondition from body_and_spec_pragmas.ads:5
OK 8
OK 9 failed precondition from body_only.adb:4
OK 10 failed postcondition from body_only.adb:5
OK 11
OK 12 failed precondition from body_only_pragmas.adb:2
OK 13 failed postcondition from body_only_pragmas.adb:3
OK 14
OK 15 failed precondition from gen_body_and_spec.ads:7 instantiated at
  main.adb:168
OK 16 failed postcondition from gen_body_and_spec.ads:8 instantiated at
  main.adb:168
OK 17
OK 18 failed precondition from gen_body_and_spec_pragmas.ads:7 instantiated at
  main.adb:201
OK 19 failed precondition from gen_body_and_spec_pragmas.adb:2 instantiated at
  main.adb:201
OK 20 failed postcondition from gen_body_and_spec_pragmas.adb:3 instantiated at
  main.adb:201
OK 21 failed postcondition from gen_body_and_spec_pragmas.ads:8 instantiated at
  main.adb:201
OK 22
OK 23 failed precondition from gen_pack.ads:8 instantiated at main.adb:254
OK 24 failed postcondition from gen_pack.ads:9 instantiated at main.adb:254
OK 25
OK 26 failed precondition from gen_pack_pragmas.ads:8 instantiated at
  main.adb:287
OK 27 failed precondition from gen_pack_pragmas.adb:3 instantiated at
  main.adb:287
OK 28 failed postcondition from gen_pack_pragmas.adb:4 instantiated at
  main.adb:287
OK 29 failed postcondition from gen_pack_pragmas.ads:9 instantiated at
  main.adb:287
OK 30
OK 31 failed precondition from gen_pack_gen.ads:11 instantiated at main.adb:341
OK 32 failed postcondition from gen_pack_gen.ads:12 instantiated at
  main.adb:341
OK 33
OK 34 failed precondition from gen_pack_gen_pragmas.ads:11 instantiated at
  main.adb:375
OK 35 failed precondition from gen_pack_gen_pragmas.adb:3 instantiated at
  main.adb:375
OK 36 failed postcondition from gen_pack_gen_pragmas.adb:4 instantiated at
  main.adb:375
OK 37 failed postcondition from gen_pack_gen_pragmas.ads:12 instantiated at
  main.adb:375
OK 38
OK 39 failed precondition from pack.ads:5
OK 40 failed postcondition from pack.ads:6
OK 41
OK 42 failed precondition from pack_pragmas.ads:5
OK 43 failed precondition from pack_pragmas.adb:3
OK 44 failed postcondition from pack_pragmas.adb:4
OK 45 failed postcondition from pack_pragmas.ads:6
OK 46
OK 47 failed precondition from pack_gen.ads:8 instantiated at main.adb:506
OK 48 failed postcondition from pack_gen.ads:9 instantiated at main.adb:506
OK 49
OK 50 failed precondition from pack_gen_pragmas.ads:8 instantiated at
  main.adb:539
OK 51 failed precondition from pack_gen_pragmas.adb:3 instantiated at
  main.adb:539
OK 52 failed postcondition from pack_gen_pragmas.adb:4 instantiated at
  main.adb:539
OK 53 failed postcondition from pack_gen_pragmas.ads:9 instantiated at
  main.adb:539
OK 54

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

2015-03-02  Hristian Kirtchev  <kirtchev@adacore.com>

	* checks.adb (Add_Validity_Check): Change the names of all
	formal parameters to better illustrate their purpose. Update
	the subprogram documentation. Update all occurrences of the
	formal parameters. Generate a pre/postcondition pragma by
	calling Build_Pre_Post_Condition.
	(Build_PPC_Pragma): Removed.
	(Build_Pre_Post_Condition): New routine.
	* einfo.adb Node8 is no longer used as Postcondition_Proc. Node14
	is now used as Postconditions_Proc. Flag240 is now renamed to
	Has_Expanded_Contract.	(First_Formal): The routine can now
	operate on generic subprograms.
	(First_Formal_With_Extras): The routine can now operate on generic
	subprograms.
	(Has_Expanded_Contract): New routine.
	(Has_Postconditions): Removed.
	(Postcondition_Proc): Removed.
	(Postconditions_Proc): New routine.
	(Set_Has_Expanded_Contract): New routine.
	(Set_Has_Postconditions): Removed.
	(Set_Postcondition_Proc): Removed.
	(Set_Postconditions_Proc): New routine.
	(Write_Entity_Flags): Remove the output of Has_Postconditions. Add
	the output of Has_Expanded_Contract.
	(Write_Field8_Name): Remove the output of Postcondition_Proc.
	(Write_Field14_Name): Add the output of Postconditions_Proc.
	* einfo.ads New attributes Has_Expanded_Contract and
	Postconditions_Proc along with occurrences in entities.
	Remove attributes Has_Postconditions and Postcondition_Proc
	along with occurrences in entities.
	(Has_Expanded_Contract): New routine along with pragma Inline.
	(Has_Postconditions): Removed along with pragma Inline.
	(Postcondition_Proc): Removed along with pragma Inline.
	(Postconditions_Proc): New routine along with pragma Inline.
	(Set_Has_Expanded_Contract): New routine along with pragma Inline.
	(Set_Has_Postconditions): Removed along with pragma Inline.
	(Set_Postcondition_Proc): Removed along with pragma Inline.
	(Set_Postconditions_Proc): New routine along with pragma Inline.
	* exp_ch6.adb (Add_Return): Code cleanup. Update the
	generation of the call to the _Postconditions routine of
	the procedure.	(Expand_Non_Function_Return): Reformat the
	comment on usage. Code cleanup.  Update the generation of
	the call to the _Postconditions routine of the procedure or
	entry [family].
	(Expand_Simple_Function_Return): Update the
	generation of the _Postconditions routine of the function.
	(Expand_Subprogram_Contract): Reimplemented.
	* exp_ch6.ads (Expand_Subprogram_Contract): Update the parameter
	profile along the comment on usage.
	* exp_ch9.adb (Build_PPC_Wrapper): Code cleanup.
	(Expand_N_Task_Type_Declaration): Generate pre/postconditions
	wrapper when the entry [family] has a contract with
	pre/postconditions.
	* exp_prag.adb (Expand_Attributes_In_Consequence): New routine.
	(Expand_Contract_Cases): This routine and its subsidiaries now
	analyze all generated code.
	(Expand_Old_In_Consequence): Removed.
	* sem_attr.adb Add with and use clause for Sem_Prag.
	(Analyze_Attribute): Reimplment the analysis of attribute 'Result.
	(Check_Use_In_Test_Case): Use routine Test_Case_Arg to obtain
	"Ensures".
	* sem_ch3.adb (Analyze_Declarations): Analyze the contract of
	a generic subprogram.
	(Analyze_Object_Declaration): Do not create a contract node.
	(Derive_Subprogram): Do not create a contract node.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Do
	not create a contract node.
	(Analyze_Completion_Contract): New routine.
	(Analyze_Function_Return): Alphabetize.
	(Analyze_Generic_Subprogram_Body): Alphabetize. Do not create a
	contract node.	Do not copy pre/postconditions to the original
	generic template.
	(Analyze_Null_Procedure): Do not create a contract node.
	(Analyze_Subprogram_Body_Contract): Reimplemented.
	(Analyze_Subprogram_Body_Helper): Do not mark the enclosing scope
	as having postconditions. Do not create a contract node. Analyze
	the subprogram body contract of a body that acts as a compilation
	unit. Expand the subprogram contract after the declarations have
	been analyzed.
	(Analyze_Subprogram_Contract): Reimplemented.
	(Analyze_Subprogram_Specification): Do not create a contract node.
	(List_Inherited_Pre_Post_Aspects): Code cleanup.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Update the
	comment on usage.
	(Analyze_Subprogram_Contract): Update the
	parameter profile and the comment on usage.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Do not create a
	contract node.
	(Analyze_Package_Declaration): Do not create a
	contract node.
	(Is_Subp_Or_Const_Ref): Ensure that the prefix has an entity.
	* sem_ch8.adb (Analyze_Subprogram_Renaming): Do not create a
	contract node.
	* sem_ch9.adb (Analyze_Entry_Declaration): Do not create a
	contract node.
	* sem_ch10.adb (Analyze_Compilation_Unit): Move local variables to
	their proper section and alphabetize them. Analyze the contract of
	a [generic] subprogram after all Pragmas_After have been analyzed.
	(Analyze_Subprogram_Body_Stub_Contract): Alphabetize.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Do not
	create a contract node.
	(Analyze_Generic_Subprogram_Declaration):
	Alphabetize local variables. Do not create a contract
	node. Do not generate aspects out of pragmas for ASIS.
	(Analyze_Subprogram_Instantiation): Instantiate
	the contract of the subprogram.  Do not create a
	contract node.	(Instantiate_Contract): New routine.
	(Instantiate_Subprogram_Body): Alphabetize local variables.
	(Save_Global_References_In_Aspects): New routine.
	(Save_References): Do not save the global references found within
	the aspects of a generic subprogram.
	* sem_ch12.ads (Save_Global_References_In_Aspects): New routine.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Do not use
	Original_Node for establishing linkages.
	(Insert_Pragma): Insertion in a subprogram body takes precedence over
	the case where the subprogram body is also a compilation unit.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Use
	Get_Argument to obtain the proper expression. Install the generic
	formals when the related context is a generic subprogram.
	(Analyze_Depends_In_Decl_Part): Use Get_Argument to obtain
	the proper expression. Use Corresponding_Spec_Of to obtain
	the spec. Install the generic formal when the related context
	is a generic subprogram.
	(Analyze_Global_In_Decl_Part): Use Get_Argument to obtain the proper
	expression. Use Corresponding_Spec_Of to obtain the spec. Install the
	generic formal when the related context is a generic subprogram.
	(Analyze_Initial_Condition_In_Decl_Part): Use Get_Argument
	to obtain the proper expression. Remove the call to
	Check_SPARK_Aspect_For_ASIS as the analysis is now done
	automatically.
	(Analyze_Pragma): Update all occurrences
	to Original_Aspect_Name. Pragmas Contract_Cases, Depends,
	Extensions_Visible, Global, Postcondition, Precondition and
	Test_Case now carry generic templates when the related context
	is a generic subprogram. The same pragmas are no longer
	forcefully fully analyzed when the context is a subprogram
	that acts as a compilation unit. Pragmas Abstract_State,
	Initial_Condition, Initializes and Refined_State have been clean
	up. Pragmas Post, Post_Class, Postcondition, Pre, Pre_Class
	and Precondition now use the same routine for analysis. Pragma
	Refined_Post does not need to check the use of 'Result or
	the lack of a post-state in its expression. Reimplement the
	analysis of pragma Test_Case.
	(Analyze_Pre_Post_Condition): New routine.
	(Analyze_Pre_Post_Condition_In_Decl_Part):
	Reimplemented.
	(Analyze_Refined_Depends_In_Decl_Part): Use Get_Argument to obtain the
	proper expression.
	(Analyze_Refined_Global_In_Decl_Part): Use Get_Argument to obtain
	the proper expression.
	(Analyze_Test_Case_In_Decl_Part): Reimplemented.
	(Check_Pre_Post): Removed.
	(Check_Precondition_Postcondition): Removed.
	(Check_SPARK_Aspect_For_ASIS): Removed.
	(Check_Test_Case): Removed.
	(Collect_Subprogram_Inputs_Outputs): Use Get_Argument
	to obtain the proper expression. Use Corresponding_Spec_Of to
	find the proper spec.
	(Create_Generic_Template): New routine.
	(Duplication_Error): New routine.
	(Expression_Function_Error): New routine.
	(Find_Related_Subprogram_Or_Body): Moved to the spec
	of Sem_Prag. Emit precise error messages. Account for cases of
	rewritten expression functions, generic instantiations, handled
	sequence of statements and pragmas from aspects.
	(Get_Argument): New routine.
	(Make_Aspect_For_PPC_In_Gen_Sub_Decl): Removed.
	(Preanalyze_CTC_Args): Removed.
	(Process_Class_Wide_Condition): New routine.
	* sem_prag.ads (Analyze_Test_Case_In_Decl_Part): Update
	the parameter profile along with the comment on usage.
	(Find_Related_Subprogram_Or_Body): Moved from the body of Sem_Prag.
	(Make_Aspect_For_PPC_In_Gen_Sub_Decl): Removed.
	(Test_Case_Arg): New routine.
	* sem_util.adb Add with and use clauses for Sem_Ch6.
	(Add_Contract_Item): This routine now creates a contract
	node the first time an item is added. Remove the duplicate
	aspect/pragma checks.
	(Check_Result_And_Post_State): Reimplemented.
	(Corresponding_Spec_Of): New routine.
	(Get_Ensures_From_CTC_Pragma): Removed.
	(Get_Requires_From_CTC_Pragma): Removed.
	(Has_Significant_Contract): New routine.
	(Inherit_Subprogram_Contract): Inherit only if the source
	has a contract.
	(Install_Generic_Formals): New routine.
	(Original_Aspect_Name): Removed.
	(Original_Aspect_Pragma_Name): New routine.
	* sem_util.ads (Check_Result_And_Post_State): Reimplemented.
	(Corresponding_Spec_Of): New routine.
	(Get_Ensures_From_CTC_Pragma): Removed.
	(Get_Requires_From_CTC_Pragma): Removed.
	(Has_Significant_Contract): New routine.
	(Install_Generic_Formals): New routine.
	(Original_Aspect_Name): Removed.
	(Original_Aspect_Pragma_Name): New routine.
	* sem_warn.adb Add with and use clauses for Sem_Prag.
	(Within_Postcondition): Use Test_Case_Arg to extract "Ensures".

[Ada] Subprogram contracts on generics

Commit Message

Patch