Page History

Partially checked

Besides direct rule violations, Astrée reports all (resulting) out-of-bound array accesses.

BAD_SIZEOF

CERT_C-ARR39-a
CERT_C-ARR39-b
CERT_C-ARR39-c

Avoid accessing arrays out of bounds
Pointer arithmetic should not be used
Do not add or subtract a scaled integer to a pointer

CERT C: Rule ARR39-C

Checks for:

• Incorrect pointer scaling
• Pointer access out of bounds
• Possible misuse of sizeof

Rule partially covered.

2930, 2931, 2932, 2933, 2934,

Exhaustively detects undefined behavior (see one compliant and one non-compliant example).