Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

Supported: Astrée reports undefined behavior.

Tool

Version

Checker

Description

Astrée
Include Page
Astrée_V
Astrée_V

array-index-range
dangling-pointer-use
field-overflow-upon-dereference
float-division-by-zero
function-pointer-incompatible-return-type
incompatible-argument-type
int-division-by-zero
int-modulo-by-zero
int-undefined-modulo
internal-and-external-linkage
invalid-function-pointer
invalid-pointer-arithmetics
left-shift-negative-first-argument
misaligned-dereference
null-dereferencing
offset-overflow
overflow-upon-dereference
pointer-comparison
pointer-subtraction
return-implicit
temporary-object-modification
undefined-shift-width
uninitialized-variable-use
write-to-constant-memory

Partially checked + soundly supported
Helix QAC

Include Page
Helix QAC_V
Helix QAC_V

C0160, C0161, C0162, C0163, C0164, C0165, C0166, C0167, C0168, C0169, C0170, C0171, C0172, C0173, C0174, C0175, C0176, C0177, C0178, C0179, C0184, C0185, C0186, C0190, C0191, C0192, C0193, C0194, C0195, C0196, C0197, C0198, C0199, C0200, C0201, C0203, C0204, C0206, C0207, C0208, C0235, C0275, C0301, C0302, C0304, C0307, C0309, C0323, C0327, C0337, C0400, C0401, C0402, C0403, C0475, C0543, C0544, C0545, C0602, C0603, C0623, C0625, C0626, C0630, C0632, C0636, C0654, C0658, C0661, C0667, C0668, C0672, C0676, C0678, C0680, C0706, C0745, C0777, C0779, C0813, C0814, C0821, C0836, C0837, C0848, C0853, C0854, C0864, C0865, C0867, C0872, C0874, C0885, C0887, C0888, C0914, C0915, C0942, C1509, C1510, C3113, C3114, C3239, C3311, C3312, C3319, C3437, C3438


LDRA tool suite
Include Page
LDRA_V
LDRA_V

48 D, 63 D, 84 D, 113 D, 5 Q, 64 S, 65 S, 100 S, 109 S, 156 S, 296 S, 324 S, 335 S, 336 S, 339 S, 412 S, 427 S, 465 S, 482 S, 497 S, 545 S, 587 S, 608 S, 642 S, 62 X, 63 X

Partially implemented
Parasoft C/C++test
Include Page
Parasoft_V
Parasoft_V
CERT_C-MSC15-a
CERT_C-MSC15-b

Evaluation of constant unsigned integer expressions should not lead to wrap-around
Evaluation of constant unsigned integer expressions in preprocessor directives should not lead to wraparound

Polyspace Bug Finder

Include Page
Polyspace Bug Finder_V
Polyspace Bug Finder_V

CERT C: Rec. MSC15-C


Checks for undefined behavior (rec. partially covered)

PVS-Studio

Include Page
PVS-Studio_V
PVS-Studio_V

V772
RuleChecker

Include Page
RuleChecker_V
RuleChecker_V

internal-and-external-linkage
pointer-comparison
pointer-subtraction
return-implicit
temporary-object-modification

Partially checked

Related Vulnerabilities

Search for vulnerabilities resulting from the violation of this rule on the CERT website.

...