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?
采纳的回答
Jack
2025-4-1
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.
更多回答（0 个）
类别
在 帮助中心 和 File Exchange 中查找有关 Generate Report 的更多信息
Translated by 
