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
