Polyspace不认识Interrupt，肿么办？

曾经在公众号中介绍过优秀的软件验证工具Polyspace，有好多猿友在交流群里咨询这个软件的问题，今天我们就典型的如何处理中断来给大家介绍下。

在嵌入式软件工程中，一定会有中断处理程序，但是Polyspace不认识interrupt，那么问题来了，肿么办？当然是必须另辟蹊径使Polyspace认识interrupt，重新写一个函数来调用中断函数，并在polyspace的配置界面填入这个函数的入口，在多入口配置处填入我们重新包装的中断函数名polys_it,函数名可以随便起。这样中断也就作为一个入口被polyspace验证。假设我们完成的函数名为polys_it如下图所示：

如何修改代码？

#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识别。有兴趣的可以动手试一试。