[Ada] Disabled invariants and preconditions and _Postconditions

[Arnaud Charlet <charlet at adacore dot com>]

This patch disables the generation of internal procedure _Postconditions when
invariants and preconditions are disabled.

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

--  main.adb

procedure Main is
   X : Integer := 0;
   type R is new Integer with Predicate => X > 0;
   package Pack is
      type T is tagged private;
      procedure P (Arg1 : in out T; Arg2 : in out R) with
        Post       => X > 0,
        Post'Class => X > 0;
   private
      type T is tagged null record with Invariant => X > 0;
   end Pack;
   package body Pack is
      procedure P (Arg1 : in out T; Arg2 : in out R) is
      begin
         null;
      end P;
   end Pack;
   use Pack;
   Y : T;
   Z : R := 2;
begin
   P (Y, Z);
end Main;

-----------------
-- Compilation --
-----------------

$ gcc -c -gnat12 -gnatd.V -gnatDG main.adb
$ grep "postconditions" main.adb.dg

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

2013-04-24  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch6.adb (Expand_Actuals): Add a predicate check on an
	actual the related type has a predicate function.
	* sem_ch3.adb (Constant_Redeclaration): Ensure that the related
	type has an invariant procedure before building a call to it.
	* sem_ch6.adb (Append_Enabled_Item): New routine.
	(Check_Access_Invariants): Use routine
	Append_Enabled_Item to chain onto the list of postconditions.
	(Contains_Enabled_Pragmas): Removed.
	(Expand_Contract_Cases): Use routine Append_Enabled_Item to chain onto
	the list of postconditions.
	(Invariants_Or_Predicates_Present): Removed.
	(Process_PPCs): Partially reimplemented.

Attachment: difs
Description: Text document