+@item -gnatw.t
+@emph{Activate warnings on suspicious contracts.}
+@cindex @option{-gnatw.t} (@command{gcc})
+This switch activates warnings on suspicious postconditions (whether a
+pragma @code{Postcondition} or a @code{Post} aspect in Ada 2012). A
+function postcondition is suspicious when it does not mention the result
+of the function. A procedure postcondition is suspicious when it only
+refers to the pre-state of the procedure, because in that case it should
+rather be expressed as a precondition.
+
+@item -gnatw.T
+@emph{Suppress warnings on suspicious contracts.}
+@cindex @option{-gnatw.T} (@command{gcc})
+This switch suppresses warnings on suspicious postconditions.
+