False Negative when using Polyspace Code Prover

10 views (last 30 days)
HONGJUN CHOI
HONGJUN CHOI on 1 May 2020
Commented: HONGJUN CHOI on 18 May 2020
This question was flagged by Christian Bard
Hello.
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.
  1. CWE 126 (Buffer Over-read)
  2. CWE 561 (Dead Code)
  3. CWE 674 (Uncontrolled Recursion)
  4. 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 ()
{
     return;
     / * FLAW: code after the 'return' * /
     printLine ("Hello");
}
- Example of CWE 561 False Negative(Code Prover cannot be detected)
static void helperBad ()
{
     printLine ("helperBad ()");
}
There is no call to helperBad function anywhere.
  1 Comment
Matt Rhodes
Matt Rhodes on 11 May 2020
Hi Hongjun,
Dead code is a very ambiguous term. You can have logically unreacheable code (which is the primary check for Code Prover) and uncalled functions (functions in your code base that are not called by anything). Code prover will find both, without false negatives, within the scope of the assumptions provided for the proof.
In this second example case, what you have might be an uncalled function, if it is called nowhere else in the code base. And, this instance could point to an incorrect behavior, but all the code presented is actually logically reachable.
For this kind of issue, if it is important to you, you are better off with a heuristic search to find all of the cases of function calls in string literals. The difficult aspect of this is that, without knowing your requirements, it is impossible to know whether it is intentional to just have a string literal refering to a function, or to have a value returned to be included in the string. The context might provide some clues too. In this contrived example, I would question the validity of any proving tool that claimed it found this to be dead code.

Sign in to comment.

Accepted Answer

Anirban
Anirban on 7 May 2020
Hi Hongjun,
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.
For all options related to tuning Code Prover checks, see the sections Check Behavior and Verification Assumptions.
  4 Comments
HONGJUN CHOI
HONGJUN CHOI on 18 May 2020
Hi Anirban,
Sorry I didn't see that it was caused by not specifying the main function entry point.
Thanks for the kind explanation!

Sign in to comment.

More Answers (0)

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Translated by