Versions Compared

Key

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

...

Tool

Version

Checker

Description

Astrée
Include Page
Astrée_V
Astrée_V

Supported, but no explicit checker
CodeSonar
Include Page
CodeSonar_V
CodeSonar_V
(customization)Users can add a custom check for allocator calls with size argument 0 (this includes literal 0, underconstrained tainted values, and computed values). 
Compass/ROSE



Can detect some violations of this rule. In particular, it warns when the argument to malloc() is a variable that has not been compared against 0 or that is known at compile time to be 0

Polyspace Bug Finder

Include Page
Polyspace Bug Finder_V
Polyspace Bug Finder_V

Tainted sign change conversion

Tainted size of variable length array

Variable length array with nonpositive size

Value from an unsecure source changes sign

Size of the variable-length array (VLA) is from an unsecure source and may be zero, negative, or too large


Size of variable-length array is zero or negative

...