Page History

Partially checked

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

LANG.MEM.BO
LANG.MEM.BU
LANG.MEM.TBA
LANG.MEM.TO
LANG.MEM.TU
LANG.STRUCT.PARITH
LANG.STRUCT.PBB
LANG.STRUCT.PPE
BADFUNC.BO.*

Buffer overrun
Buffer underrun
Tainted buffer access
Type overrun
Type underrun
Pointer Arithmetic
Pointer before beginning of object
Pointer past end of object
A collection of warning classes that report uses of library functions prone to internal buffer overflows.

BAD_SIZEOF

DF4955, DF4956, DF4957

MISRA.PTR.ARITH.2012

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 (rule fully covered).

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