Code prover polyspace_end_of_init not found

When performing running Code Prover with "verify whole application" selected, I receive the error:

Pragma polyspace_end_of_init not found in main.

I am unable to find any documentation on this error. Can someone help resolve this issue?

Answer 1

[Jack]

This error means that Code Prover expected to see a pragma indicating the end of your initialization section in main, but it wasn’t found. When verifying the whole application, Code Prover distinguishes between initialization code and the rest of your program using special pragmas like:

/* polyspace_end_of_init */

To resolve the error, add this pragma at the end of your initialization code in your main function. For example:

int main() {
    // Your initialization code here

    /* polyspace_end_of_init */

    // The rest of your program
}

Alternatively, if you don't want to mark the end of initialization explicitly, you may adjust Code Prover settings to disable this check, but adding the pragma is the recommended solution.

Follow me so you can message me anytime with future questions. If this helps, please accept the answer and upvote it as well.

[gary]

Thanks for the reply Jack. All of this makes sense.

To anyone working at Mathworks: Why is this not mentioned in any of the documentation (if it is, I couldn't find it)?