I am a beginner who is interested in Polyspace tool.
On page 63 of the Polyspace® Code Prover ™ Getting Started Guide, Code Prover says there are no false negatives.
However, as a result of static analysis of a part of NIST Juliet Test Suite for C / C ++ using Polyspace Code Prover, false negatives existed in the following CWE ID.
- CWE 126 (Buffer Over-read)
- CWE 561 (Dead Code)
- CWE 674 (Uncontrolled Recursion)
- CWE 835 (Loop with Unreachable Exit Condition ('Infinite Loop'))
I've analyzed the code, but I'm asking because I can't figure out why false negatives are occurring.
- Example of CWE 561 True Positive(Code Prover detects it.)
void CWE561_Dead_Code__return_before_code_01_bad ()
/ * FLAW: code after the 'return' * /
- Example of CWE 561 False Negative(Code Prover cannot be detected)
static void helperBad ()
printLine ("helperBad ()");
There is no call to helperBad function anywhere.