曾经在公众号中介绍过优秀的软件验证工具Polyspace，有好多猿友在交流群里咨询这个软件的问题，今天我们就典型的如何处理中断来给大家介绍下。
在嵌入式软件工程中，一定会有中断处理程序，但是Polyspace不认识interrupt，那么问题来了，肿么办？当然是必须另辟蹊径使Polyspace认识interrupt，重新写一个函数来调用中断函数，并在polyspace的配置界面填入这个函数的入口，在多入口配置处填入我们重新包装的中断函数名polys_it,函数名可以随便起。这样中断也就作为一个入口被polyspace验证。假设我们完成的函数名为polys_it如下图所示：
如何修改代码？
代码语言：javascript复制#ifdef POLYSPACE
externvolatileint rnd;
#endif
void polys_it(void)
{
#ifdef POLYSPACE
while(rnd)
{
#else
while(1)
{
#endif
ISR();
}
}
staticvoid interrupt ISR(void)
{
……
}同时需要在Polyspace的宏配置界面填入POLYSPACE
按照以上修改完代码后，保存编译，生成报告。怎么样就是这么简单，就可以处理中断函数被Polyspace识别。有兴趣的可以动手试一试。
