difference between code prover & bug finder

what are the differences between POLYSPACE code prover & Bug finder.which one is suitable for development process ?

Answer 1

[Lucas Lebert]

Hi Shaku, the main goal of the Code Prover is the verification of the code, which means proving the absence of run-time errors. Furthermore the Code Prover can give insight into the runtime behaviour and the data ranges of the code. To visualize this, the Code Prover highlights the code either in red (proven runtime error) orange (possible runtime error) and green (proven absence of runtime errors). Furthermore the Code Prover highlights unreachable code in grey.

This can not be done by the Bug Finder. Its main goal is to find bugs through exhaustive testing. The bugs found in the code are highlighted in red. Compared to the Code Prover, the Bug Finder is trading the depth of analysis for speed.

Both the bug finder and the Code Prover are explicitly designed during the development process. Many customers use the Bug Finder during the implementation of the code and both products for the unit tests, integration tests and acceptance tests.

Answer 2

[Jay Abraham]

You can learn about the differences between Polyspace Bug Finder and Polyspace Code Prover in the documentation of these products. Follow the link below for the detailed explanation.

https://www.mathworks.com/help/bugfinder/gs/use-bug-finder-and-code-prover.html

Excerpt from documentation ... “Polyspace® Bug Finder™ and Polyspace Code Prover™ detect run-time errors through static analysis. Though the products have a similar user interface and the mathematics underlying the analysis can sometimes be the same, the goals of the two products are different.

Bug Finder quickly analyzes your code and detects many types of defects. Code Prover checks every operation in your code for a set of possible run-time errors and tries to prove the absence of the error for all execution paths. For instance, for every division in your code, a Code Prover analysis tries to prove that the denominator cannot be zero. Bug Finder does not perform such exhaustive verification. For instance, Bug Finder also checks for a division by zero error, but it might not find all operations that can cause the error.”