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.
