The C Standard, Annex J (184) [ISO/IEC 9899:20112024], states that the behavior of a program is undefined when
...
Tool | Version | Checker | Description | ||||||
---|---|---|---|---|---|---|---|---|---|
Astrée |
| invalid-free | Fully checked | ||||||
Axivion Bauhaus Suite |
| CertC-MEM34 | Can detect memory deallocations for stack objects | ||||||
Clang |
| clang-analyzer-unix.Malloc | Checked by clang-tidy ; can detect some instances of this rule, but does not detect all | ||||||
CodeSonar |
| ALLOC.TM | Type Mismatch | ||||||
Compass/ROSE | Can detect some violations of this rule | ||||||||
| BAD_FREE | Identifies calls to | |||||||
Cppcheck |
| autovarInvalidDeallocation mismatchAllocDealloc | Partially implemented | ||||||
Cppcheck Premium |
| autovarInvalidDeallocation mismatchAllocDealloc | Partially implemented | ||||||
Helix QAC |
| DF2721, DF2722, DF2723 | |||||||
Klocwork |
| FNH.MIGHT FNH.MUST | |||||||
LDRA tool suite |
| 407 S, 483 S, 644 S, 645 S, 125 D | Partially implemented | ||||||
Parasoft C/C++test |
| CERT_C-MEM34-a | Do not free resources using invalid pointers | ||||||
Parasoft Insure++ | Runtime analysis | ||||||||
PC-lint Plus |
| 424, 673 | Fully supported | ||||||
Polyspace Bug Finder |
| Checks for:
Rule fully covered. | |||||||
PVS-Studio |
| V585, V726 | |||||||
RuleChecker |
| invalid-free | Partially checked | ||||||
TrustInSoft Analyzer |
| unclassified ("free expects a free-able address") | Exhaustively verified (see one compliant and one non-compliant example). |
...
Bibliography
[ISO/IEC 9899:20112024] | Subclause J.2, "Undefined Behavior" |
[Seacord 2013b] | Chapter 4, "Dynamic Memory Management" |
...