[Ada] Issue warning on suspicious contract cases when -gnatw.t is set

[Arnaud Charlet <charlet at adacore dot com>]

The warning option -gnatw.t already issued warnings on suspicious
postconditions. This extends it to contract cases, which is a GNAT
pragma/aspect allowing to express fine-grain contracts. GNAT now detects
these cases on the following code:

$ gcc -c -gnatc -gnatw.t -gnat12 p.ads

     1. package P is
     2.    function A_Is_Positive (X : Integer) return Boolean with
     3.      Contract_Case => (Name    => "normal case",
             |
        >>> warning: "Ensures" component refers only to pre-state
        >>> warning: contract cases do not mention result

     4.                        Mode    => Nominal,
     5.                        Ensures => X >= 0);
     6.    procedure A_Incr (X : in Integer; Y : out Integer) with
     7.      Contract_Case => (Name    => "normal case",
             |
        >>> warning: "Ensures" component refers only to pre-state

     8.                        Mode    => Nominal,
     9.                        Ensures => X = X + 1);
    10. end P;

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

2012-03-15  Yannick Moy  <moy@adacore.com>

	* gnat_ugn.texi Document the extension of option -gnatw.t.
	* sem_ch3.adb (Analyze_Declaration): Check for suspicious
	contracts only after contract cases have been semantically
	analyzed.
	* sem_ch6.adb (Check_Subprogram_Contract): Consider also Ensures
	components of contract cases for detecting suspicious contracts.

Attachment: difs
Description: Text document