7.2.6.1. Messages reported by Proof

The following table shows all check messages reported by proof.

Message Kind	CWE	Explanation
run-time checks
divide by zero	CWE 369	Check that the second operand of the division, mod or rem operation is different from zero.
index check	CWE 119	Check that the given index is within the bounds of the array.
overflow check	CWE 190	Check that the result of the given integer arithmetic operation is within the bounds of the base type.
fp_overflow check	CWE 739	Check that the result of the given floating point operation is within the bounds of the base type.
range check	CWE 682	Check that the given value is within the bounds of the expected scalar subtype.
predicate check	CWE 682	Check that the given value respects the applicable type predicate.
predicate check on default value	CWE 682	Check that the default value for the type respects the applicable type predicate.
null pointer dereference	CWE 476	Check that the given pointer is not null so that it can be dereferenced.
null exclusion		Check that the subtype_indication of the allocator does not specify a null_exclusion
dynamic accessibility check		Check that the accessibility level of the result of a traversal function call is not deeper than the accessibility level of its traversed parameter.
resource or memory leak	CWE 772	Check that the assignment does not lead to a resource or memory leak
resource or memory leak at end of scope	CWE 772	Check that the declaration does not lead to a resource or memory leak
unchecked union restriction		Check restrictions imposed on expressions of an unchecked union type
length check		Check that the given array is of the length of the expected array subtype.
discriminant check	CWE 136	Check that the discriminant of the given discriminated record has the expected value. For variant records, this can happen for a simple access to a record field. But there are other cases where a fixed value of the discriminant is required.
tag check	CWE 136	Check that the tag of the given tagged object has the expected value.
ceiling priority in Interrupt_Priority		Check that the ceiling priority specified for a protected object containing a procedure with an aspect Attach_Handler is in Interrupt_Priority.
use of an uninitialized variable	CWE 457	Check that a variable is initialized
interrupt is reserved		Check that the interrupt specified by Attach_Handler is not reserved.
invariant check		Check that the given value respects the applicable type invariant.
invariant check on default value		Check that the default value for the type respects the applicable type invariant.
ceiling priority protocol		Check that the ceiling priority protocol is respected, i.e., when a task calls a protected operation, the active priority of the task is not higher than the priority of the protected object (Ada RM Annex D.3).
task termination		Check that the task does not terminate, as required by Ravenscar.
assertions
initial condition		Check that the initial condition of a package is true after elaboration.
default initial condition		Check that the default initial condition of a type is true after default initialization of an object of the type.
precondition	CWE 628	Check that the precondition aspect of the given call evaluates to True.
precondition of main	CWE 628	Check that the precondition aspect of the given main procedure evaluates to True after elaboration.
postcondition	CWE 682	Check that the postcondition aspect of the subprogram evaluates to True.
refined postcondition	CWE 682	Check that the refined postcondition aspect of the subprogram evaluates to True.
contract case	CWE 682	Check that all cases of the contract case evaluate to true at the end of the subprogram.
disjoint contract cases		Check that the cases of the contract cases aspect are all mutually disjoint.
complete contract cases		Check that the cases of the contract cases aspect cover the state space that is allowed by the precondition aspect.
exceptional case	CWE 682	Check that all cases of the exceptional cases evaluate to true on exceptional exits.
loop invariant		Check that the loop invariant evaluates to True on all iterations of the loop.
loop invariant in first iteration		Check that the loop invariant evaluates to True on the first iteration of the loop.
loop invariant after first iteration		Check that the loop invariant evaluates to True at each further iteration of the loop.
loop variant	CWE 835	Check that the given loop variant decreases/increases as specified during each iteration of the loop. This implies termination of the loop.
subprogram variant		Check that the given subprogram variant decreases/increases as specified during each recursive call. This implies there will be no infinite recursion.
assertion		Check that the given assertion evaluates to True.
assertion step		Check that the side-condition of a cut operation evaluates to True.
assertion premise		Check that the premise of an assertion with cut operations evaluates to True.
raised exception		Check that raise expressions can never be reached and that all exceptions raised by raise statement and procedure calls are expected.
feasible function		Check that an abstract function or access-to-function type is feasible.
Inline_For_Proof or Logical_Equal annotation		Check that an Annotate pragma with the Inline_For_Proof or Logical_Equal identifier is correct.
Container_Aggregates annotation		Check the invariants used to translate container aggregates using the primitives provided by the Aggregate aspect and the Container_Aggregates annotation.
reclamation annotation		Check that confirming annotations on hidden types which need reclamation are consistent with their full view.
termination check		Check the termination of subprograms annotated with an Always_Terminates aspect whose value is not known at compile time and of calls to such subprograms.
unchecked conversion source check	CWE 843	Check that a source type in an unchecked conversion can safely be used for such conversions. This means that the memory occupied by objects of this type is fully used by the object.
unchecked conversion target check	CWE 843	Check that a target type in an unchecked conversion can safely be used for such conversions. This means that the memory occupied by objects of this type is fully used by the object, and no invalid bitpatterns occur.
unchecked conversion size check	CWE 843	Check that the two types in an unchecked conversion instance are of the same size.
alignment check		Check that the first object’s alignment is an integral multiple of the second object’s alignment.
volatile overlay check		Check that, if an object has an address clause that is not simply the address of another object, it is volatile
Liskov Substitution Principle
precondition weaker than class-wide precondition		Check that the precondition aspect of the subprogram is weaker than its class-wide precondition.
precondition not True while class-wide precondition is True		Check that the precondition aspect of the subprogram is True if its class-wide precondition is True.
postcondition stronger than class-wide postcondition		Check that the postcondition aspect of the subprogram is stronger than its class-wide postcondition.
class-wide precondition weaker than overridden one		Check that the class-wide precondition aspect of the subprogram is weaker than its overridden class-wide precondition.
class-wide postcondition stronger than overridden one		Check that the class-wide postcondition aspect of the subprogram is stronger than its overridden class-wide postcondition.
precondition of the source weaker than precondition of the target		Check that the precondition aspect of the access-to-subprogram type used as the target of a conversion implies the precondition of the source.
postcondition of the source stronger than postcondition of the target		Check that the postcondition aspect of the access-to-subprogram type used as the target of a conversion is implied by the postcondition of the source.

The following table shows all warning messages reported by proof when using switch --proof-warnings=on.

Message Kind	CWE	Explanation
precondition always False	CWE 570	Warn if precondition is found to be always False
postcondition always False	CWE 570	Warn if postcondition is found to be always False
pragma Assume always False	CWE 570	Warn if pragma Assume is found to be always False
unreachable branch	CWE 561	Warn if branch is found to be unreachable
unreachable code	CWE 561	Warn if code is found to be unreachable