[polyspace code prover] How to fix the link errors ?

Hello All,

I am using polyspace Code Prover R2014b; and I want to fix the link errors detected ,

i want to know also if the polyspace continue with the analysis when he detect the links errors or not ?

i have also tryed to surround the link errors with polyspace bug finder R2015b with the declarations mismatch option but i didn't find any errors

thank you very much

Answer 1

[Alexandre De Barros]

Hello,

Link errors with Code Prover will stop the verification process because they represent an inconsistency in the source code that Code Prover cannot bypass.

Let's take the example of a function which is supposed to return an int in one file

 int foo(void);

but that returns a float in another file

 float foo(void) { ... }

What is the return type that Polyspace Code Prover should consider? It is not possible for a tool that proves code correctness to continue in this situation. That's why Polyspace stops and display a message showing the inconsistency.

See this link on how to interpret and fix this kind of errors: http://www.mathworks.com/help/codeprover/ug/compilation-error-overview.html?searchHighlight=link#bu7wiec

Another page that can help you: http://www.mathworks.com/help/codeprover/troubleshooting-in-polyspace-code-prover.html (paragraph Compilation and Linking)

Best regards,

Alexandre

[dakhlaoui zina]

thank you very much