曾经在公众号中介绍过优秀的软件验证工具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识别。有兴趣的可以动手试一试。