...
Tool | Version | Checker | Description | ||||||
---|---|---|---|---|---|---|---|---|---|
Astrée |
| Supported: Astrée reports potential infinite loops. | |||||||
CodeSonar |
| LANG.STRUCT.LOOP.HR | High risk loop | ||||||
Compass/ROSE | |||||||||
LDRA tool suite |
| 510 S | Partially implemented | ||||||
PC-lint Plus |
| 440, 442, 443, | Partially supported | ||||||
Polyspace Bug Finder |
| Checks for loop bounded with tainted value (rec. partially covered) | |||||||
PVS-Studio |
| V621 |
...