How should I verify ”overlapping” results from Code Prover and Bug Finder?

At my company, we use Bug Finder in tandem with Code Prover to check for potential bugs/violations of coding standards and some specific run-time errors.

Normally, I skip through some of the Bug Finder check results (namely zero-division, integers overflow, out-of-bound-access pointers/arrays/loops, etecera) if there's already "overlapping" checkers from Code Prover to save time. For example, if I had confirmed the validity for all Code Prover's overflow checks against a piece of code (which also produced another set of overflow check results in Bug Finder as well), then regardless of whether the Bug Finder results are duplicates or different checks from Code Prover, I'd automatically assume those are not defects and ignore them totally.

My question are as following:

1. What is your approach when verifying results of categories that are checked in both tools?
2. Is it safe to justify only the result from Coder Prover and totally ignore the "less" exhaustive check results from Bug Finder in such cases where both tools offer the same check? If not, then what are potential risks if I only rely on Code Prover results for run-time errors detection? (As stated in the offical documents, Bug Finder's main usage is to quickly detect and rectify bugs and it might not detect all the possible causes for run-time errors, which is one of Coder Prover's strong points so I think it's would be fine to just solely rely on Code Prover)

Thanks in advance for reading and it would be great if someone can give some pointers!

Answer 1

[Anirban]

1. The recommended approach is to use Bug Finder first (and more frequently), and fix the simpler bugs found. Then, use Code Prover to perform the more exhaustive checks. If you have Polyspace as You Code, it can be run even prior to running Bug Finder.
2. You can skip the checkers of Bug Finder if you review the results of the equivalent checkers in Code Prover. In general, if a Bug Finder checker can find an issue, the equivalent checker in Code Prover can also find the issue (as long as the same options are used for the Bug Finder and Code Prover analysis - for instance, if the tools are run on the same project in the UI or using the same options file). Of course, as you know, Bug Finder can also find many, many other types of issues that Code Prover does not even look for (because finding those issues do not require mathematical proof). But I am assuming that in this question, you were only asking about those checkers of Bug Finder that overlap with Code Prover.

[ドゥック・ミン]

Hi Anirban! Thanks for the detailed answer!

Just to clarify a bit on the workflow that I'm doing: Our company have licenses for both Polyspace Code Prover and Bug Finder, and we actively use both tools to perform checks for C-lang codes. I'm also aware of the fact that some Bug Finder checks aren't implemented in Code Prover. However, to my best knowledge, most of these checks are to promote secure/robust coding and also to reduce maintenance cost. Since we do not require full compliance for secure coding for our particular projects, most of the times we do the minimal verification for Bug Finder check results while putting a lot of effort on checking Code Prover check results since those provide a better overall coverage.

With the aforementioned context in mind, I'd like to verify my understanding after reading your answers and provide an additional questions:

You can skip the checkers of Bug Finder if you review the results of the equivalent checkers in Code Prover. In general, if a Bug Finder checker can find an issue, the equivalent checker in Code Prover can also find the issue (as long as the same options are used for the Bug Finder and Code Prover analysis - for instance, if the tools are run on the same project in the UI or using the same options file)

So my question is whether the above answer still applies in the following case: Bug Finder and Code Prover both checked for "out-of-bound access to array" with same setting options, however, Bug Finder produced an ID(s) which does not correspond to any ID(s) from Code Prover results. However, all ID(s) produced by Code Prover are proved to be false (equals no defects in category "out-of-bound access to array" as far as Code Prover can check). Can I totally ignore all those ID(s) from Bug Finder? (since Code Prover checked the same category and I've verified all IDs from Code Prover)

(To clarify, I've never encountered this case before, and Code Prover's coverage is better anyway, so it's kind of pointless to even think about this. But if possible I still want to know what's the correct approach here).

[Anirban]

I am not sure what you mean by 'ID'-s here. If you mean the contents of the 'ID' column in Bug Finder results, I am not sure they are related to the contents of the 'ID' column in Code Prover results. The 'ID'-s are calculated differently for the two products. I am guessing that by ID, you mean a type of result in a file on a certain line and column.

I am guessing what you are asking is the following: if you run the Code Prover check Out of bounds array index and you review all the orange results from this check and find they are false positives, do you also need to review the results of the Bug Finder check Array access out of bounds? In general, no.

In fact, the way Bug Finder works, if all of your results from Code Prover are genuine false positives, Bug Finder should not even show them in most cases. Code Prover tries to be sound and flags all cases where it cannot prove the presence of a run-time error in orange. These cases are suspect and need manual review. Bug Finder tries to minimize false positives and only shows cases where the likelihood of a run-time error is high (but it can miss some cases whereas Code Prover follows a very precise and exhaustive logic and tries not to miss any case).

[ドゥック・ミン]

"I am guessing that by ID, you mean a type of result in a file on a certain line and column."

-> Yes, this is exactly what I meant by "IDs". Sorry for the confusing question, I wasn't able to elaborate it in a better way.

"I am guessing what you are asking is the following: if you run the Code Prover check Out of bounds array index and you review all the orange results from this check and find they are false positives, do you also need to review the results of the Bug Finder check Array access out of bounds? In general, no"

"In fact, the way Bug Finder works, if all of your results from Code Prover are genuine false positives, Bug Finder should not even show them in most cases. Code Prover tries to be sound and flags all cases where it cannot prove the presence of a run-time error in orange. These cases are suspect and need manual review. Bug Finder tries to minimize false positives and only shows cases where the likelihood of a run-time error is high (but it can miss some cases whereas Code Prover follows a very precise and exhaustive logic and tries not to miss any case)."

-> Also yes, that's what it boils down to in my question. Basically:

① If Code Prover uses real input data to try to find all defects including ones that could not/might not be found otherwise with static checking, then maybe there's not much of a reason to review Bug Finder results after all results of the equivalent checker in Code Prover were proven to be false positives.

② After having done manual review for Code Prover results, only need to review Bug Finder results of the equivalent category if defect-flagging conditions on Bug Finder are different (from Code Prover's). While I've read some of the official documentations, I was not able to find any conclusive evidence that flagging conditions on any common defect categories, for example out-of-bound-access, are implemented differently on both tools. I'll be very appreciated if you can offer some pointers here. It would be a day-night difference in my workflow if I know that all common defect categories on both tools share the same underlying flagging conditions.

I kind of expect to be assured by a staff on this matter, and so far your answers pretty much reflected on my thoughts as well.

Anyway, looking forward to hear your thoughts. Many thanks!

[Anirban]

(1) Yes.

I would add some caveats: it can be sometimes easier to review Bug Finder results. For instance, in Bug Finder, a lot of results are supported by an event traceback showing one path leading to an issue. So, you might incorrectly mark something as a false positive in Code Prover, but when you see it in Bug Finder, it would be clear it's not a false positive. But if you are sure that the results you marked as false positives in Code Prover are indeed false positives, then yes, there's not much reason to review the results of the equivalent Bug Finder checkers.

(2) I am not sure to understand what you mean by 'defect flagging conditions'. So I will give a two-part answer (I think the second part will be useful to you, but I am not sure):

• For Code Prover to find the same things as Bug Finder (and then some more), the analysis options used must be the same. More precisely, the options in the categories Target & Compiler, Macros, Environment Settings, Inputs & Stubbing must be the same. One easy way to make sure the options are same is to run Bug Finder and Code Prover on the same project (or using the same options file).
• For the subset of checkers that are common to Bug Finder and Code Prover, essentially the same analysis algorithms are used, except that in Bug Finder, certain heuristics are used to minimize false positives and minimize the analysis time. These heuristics prevent certain things from being shown in Bug Finder while they appear as orange checks in Code Prover (the orange checks might be real issues, especially the critical orange checks, or false positives). So yes, for the equivalent checkers, the issues found by Code Prover should be a superset of the ones found by Bug Finder.

[ドゥック・ミン]

Hi Anirban,

1. We deliberately check for Code Prover results preceeding Bug Finder's, that is due to the requirement from our client. In our case, checking Bug Finder results is requested later and this is supposed to be more of a supplementary check. Furthermore, we tend to check Code Prover results often since each result provides a detailed line and column, which is sometimes missing from Bug Finder check.

Regardless, we have never encountered an instance of Bug Finder results negating the equivalent Code Prover results so it is probably not a problem for our codes but I will make sure to keep this in mind.

2. I meant "checking conditions", but you got it right so no issue here,

"For Code Prover to find the same things as Bug Finder (and then some more), the analysis options used must be the same. More precisely, the options in the categories Target & Compiler, Macros, Environment Settings, Inputs & Stubbing must be the same. One easy way to make sure the options are same is to run Bug Finder and Code Prover on the same project (or using the same options file)."

→ I am not well-informed on these settings one-by-one since we had our team develop in-house tool to automate the Code Prover/Bug Finder analysis not on the Polyspace interface but rather from inside MATLAB interface. However, I do know that we use some options for our tool so I will make sure to forward this part of your reply to our team for further investigation.

"For the subset of checkers that are common to Bug Finder and Code Prover, essentially the same analysis algorithms are used, except that in Bug Finder, certain heuristics are used to minimize false positives and minimize the analysis time. These heuristics prevent certain things from being shown in Bug Finder while they appear as orange checks in Code Prover (the orange cahecks might be real issues, especially the critical orange checks, or false positives). So yes, for the equivalent checkers, the issues found by Code Prover should be a superset of the ones found by Bug Finder. "

→ Except for orange checks related to floating-point overflow and some other obscure checks, we do review all remaining orange check results very carefully, and lastly, Bug Finder results. If the checking conditions found in Code Prover for a particular category is a superset of those found in Bug Finder, then I think my current checking routine should not be affected in anyway. As you pointed out, this part of your answer would be of tremendously helpful to form our baseline for reviewing codes and inquiry sessions with our client.

For the time being, all of my questions were answered and I don't have any further follow-up question so I will mark your answer as the solution.

Thank you again for taking your time to answer! I wish you a good day and take care!