Polyspace CodeProver – reanalyze only differences

Hi, May tools have the concepts re-build(take everything from scratch) and build ( look only to the differences).

Can we do something like this in CodeProver?

If not, can we submit such a change request?

Best Regards,

Daniel

Answer 1

[Cindy Solomon]

Hi Daniel,

This functionality is not currently available in Polyspace, but I work for MathWorks and have forwarded your feedback to the appropriate product team. Thank you for the suggestion!

Answer 2

[Alexandre De Barros]

Hi Daniel!

There is no such thing yet because when you want to prove that everything is safe, it is not as easy as it may appear.

Why ? Because even if you change one file, this little change can impact the rest of the application.

For example, it could be a change that would eventually lead to a new function call, and if the call tree changes, the whole application can change (unreachable code can become reachable, global variables can have different values, etc...)

Hence, this feature requires to compute the impact and for that you need to interpret the code, it's not only detecting what has changed since the last verification.

Regards,

Alexandre