Messages reported by Flow Analysis
----------------------------------

The following table shows all flow analysis messages, (E)rrors, (W)arnings and (C)hecks.

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

.. csv-table::
   :header: "Message Kind", "Class", "CWE", "Explanation"
   :widths: 1, 1, 1, 6

    "critically incomplete Global or Initializes contract", "E", "", "A Global or Initializes contract fails to mention some objects."
    "volatile function wrongly declared as non-volatile", "E", "", "A volatile function wrongly declared as non-volatile."
    "function with side effects", "E", "", "A function with side effects."
    "aliasing between subprogram parameters", "C", "", "Aliasing between formal parameters or global objects."
    "invalid call in type invariant", "C", "CWE `674 <http://cwe.mitre.org/data/definitions/674.html>`_", "A type invariant calls a boundary subprogram for the type."
    "invalid context for call to Current_Task", "C", "", "Current_Task is called from an invalid context."
    "race condition", "C", "CWE `362 <http://cwe.mitre.org/data/definitions/362.html>`_", "An unsynchronized global object is accessed concurrently."
    "wrong Default_Initial_Condition aspect", "C", "CWE `457 <http://cwe.mitre.org/data/definitions/457.html>`_", "A type is wrongly declared as initialized by default."
    "input item missing from the dependency clause", "C", "", "An input is missing from the dependency clause."
    "output item missing from the dependency clause", "C", "", "An output item is missing from the dependency clause."
    "input item missing from the null dependency clause", "C", "", "An input item is missing from the null dependency clause."
    "extra input item in the dependency clause", "C", "", "Extra input item in the dependency clause."
    "subprogram output depends on a Proof_In global", "C", "", "Subprogram output depends on a Proof_In global."
    "non-ghost output of ghost subprogram", "C", "", "A ghost subprogram has a non-ghost global output."
    "incomplete Global or Initializes contract", "C", "", "A Global or Initializes contract fails to mention some objects."
    "an extra item in the Global or Initializes contract", "C", "", "A Global or Initializes contract wrongly mentions some objects."
    "constants with variable inputs that is not a state constituent", "C", "", "Constants with variable inputs that are not state constituents."
    "illegal write of a global input", "C", "", "Illegal write of a global input."
    "an extra item in the Initializes contract", "C", "", "An object that shall not appear in the Initializes contract."
    "all execution paths raise exceptions or do not return", "C", "", "All execution paths raise exceptions or do not return."
    "illegal write of an object declared as constant after elaboration", "C", "", "Illegal write of an object declared as constant after elaboration."
    "protected operation blocks", "C", "CWE `667 <http://cwe.mitre.org/data/definitions/667.html>`_", "A protected operation may block."
    "illegal reference to a global object in precondition of a protected operation", "C", "", "An illegal reference to global in precondition of a protected operation."
    "constant with no variable inputs as an abstract state's constituent", "C", "", "Constant with no variable inputs as an abstract state's constituent."
    "subprogram with aspect Always_Terminates may not terminate", "C", "CWE `674 <http://cwe.mitre.org/data/definitions/674.html>`_", "A subprogram with aspect Always_Terminates may not terminate."
    "use of an uninitialized variable", "C", "CWE `457 <http://cwe.mitre.org/data/definitions/457.html>`_", "Flow analysis has detected the use of an uninitialized variable."
    "global object is not used", "C", "", "A global object is never used."
    "dead code", "W", "CWE `561 <http://cwe.mitre.org/data/definitions/561.html>`_", "A statement is never executed."
    "a state abstraction that is impossible to initialize", "W", "", "A state abstraction that is impossible to initialize."
    "a statement with no effect on subprogram's outputs", "W", "CWE `1164 <http://cwe.mitre.org/data/definitions/1164.html>`_", "A statement with no effect on subprogram's outputs."
    "an IN OUT parameter or an In_Out global that is not written", "W", "", "An IN OUT parameter or an In_Out global that is not written."
    "loop with stable statement", "W", "", "A loop with stable statement."
    "object is not used", "W", "CWE `563 <http://cwe.mitre.org/data/definitions/563.html>`_", "A parameter or locally declared object is never used."
    "initial value of an object is not used", "W", "CWE `563 <http://cwe.mitre.org/data/definitions/563.html>`_", "The initial value of an object is not used."
    "non-volatile function wrongly declared as volatile", "W", "", "A non-volatile function wrongly declared as volatile."

.. note::
    Certain messages emitted by flow analysis are classified as errors and consequently cannot be suppressed or justified.