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.