Miscellaneous warnings reported by GNATprove
--------------------------------------------

The following table shows default warnings reported by GNATprove outside of flow analysis and proof.

.. tabularcolumns:: |p{2in}|p{3in}|

.. csv-table::
   :header: "Message Kind", "Explanation"
   :widths: 1, 4

    "address to access conversion", "call to conversion function is assumed to return a valid access designating a valid value"
    "volatile and atomic status of aliases", "aliased objects should both be volatile or non-volatile, and both be atomic or non-atomic"
    "volatile properties of aliases", "aliased objects should have the same volatile properties"
    "attribute Valid always True", "attribute Valid is assumed to return True"
    "initialization of alias", "initialization of object is assumed to have no effects on other non-volatile objects"
    "function Is_Valid always return True", "function Is_Valid is assumed to return True"
    "procedure not terminating normally nor abnormally", "procedure which does not return normally nor raises an exception cannot always terminate"
    "no check message justified", "no check message justified by this pragma"
    "proved check message justified", "only proved check messages justified by this pragma"
    "Terminating deprecated", "Terminating, Always_Return, and Might_Not_Return annotations are ignored"
    "External Axiomatizations not supported", "External Axiomatizations are not supported anymore, ignored"
    "pragma ignored", "pragma is ignored (it is not yet supported)"
    "Overflow_Mode ignored", "pragma Overflow_Mode in code is ignored"
    "precondition statically False", "precondition is statically False"
    "unreferenced function", "analyzing unreferenced function"
    "unreferenced procedure", "analyzing unreferenced procedure"
    "useless Relaxed_Initialization aspect on function result", "function result annotated with Relaxed_Initialization cannot be partially initialized"
    "useless Relaxed_Initialization aspect on object", "object annotated with Relaxed_Initialization cannot be partially initialized"
    "variant not recursive", "no recursive call visible on subprogram with Subprogram_Variant"

The following table shows warnings guaranteed to be reported by GNATprove.

.. tabularcolumns:: |p{2in}|p{3in}|

.. csv-table::
   :header: "Message Kind", "Explanation"
   :widths: 1, 4

    "assumed Always_Terminates", "no Always_Terminates aspect available for subprogram, subprogram is assumed to always terminate"
    "assumed Global null", "no Global contract available for subprogram, null is assumed"
    "imprecisely supported address specification", "object with an imprecisely supported address specification: non-atomic objects should not be accessed concurrently, volatile properties should be correct, indirect writes to object to and through potential aliases are ignored, and reads should be valid"

The following table shows warnings reported by GNATprove when using switch ``--pedantic``.

.. tabularcolumns:: |p{2in}|p{3in}|

.. csv-table::
   :header: "Message Kind", "Explanation"
   :widths: 1, 4

    "string attribute length", "string attribute has an implementation-defined length"
    "operator reassociation", "possible operator reassociation due to missing parentheses"
    "representation attribute value", "representation attribute has an implementation-defined value"