...
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 |
| 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 |
...