7.2.6.2. Messages reported by Flow Analysis
The following table shows all flow analysis messages, (E)rrors, (W)arnings and (C)hecks.
Message Kind |
Class |
CWE |
Explanation |
---|---|---|---|
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 |
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 |
An unsynchronized global object is accessed concurrently. |
wrong Default_Initial_Condition aspect |
C |
CWE 457 |
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 |
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 |
A subprogram with aspect Always_Terminates may not terminate. |
use of an uninitialized variable |
C |
CWE 457 |
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 |
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 |
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 |
A parameter or locally declared object is never used. |
initial value of an object is not used |
W |
CWE 563 |
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.