False Negative when using Polyspace Code Prover
3 views (last 30 days)
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.
Anirban on 7 May 2020
For the two specific examples you give, you have to turn on the checks Function not called and Function not reachable. Often users are not interested in these two checks, for instance, because they are running Code Prover on units and some functions might be uncalled within an unit but eventually will get called from another unit. So these two checks are disabled by default. To enable them, use this option.