...
Tool | Version | Checker | Description | ||||||
---|---|---|---|---|---|---|---|---|---|
Astrée |
| Supported, but no explicit checker | |||||||
CodeSonar |
| (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 | ||||||
Polyspace Bug Finder | R2016a | Tainted sign change conversion | 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 |
...