Polyspace如何检测simulink生成的代码

1、在Simulink中将模型运行后，生成代码。在模型所在的文件夹中会自动生成两个文件夹

2、在simulink菜单栏中：Code-->Polyspace-->Verify Code Generated For-->Model

在模型所在的文件夹中会自动生成两个文件夹

3、打开results_xxxx文件夹，如果有后缀名为.psprj的文件，则下一步打开Polyspace，否则，重新生成代码(删除多出来的文件和文件夹)

4、在Polyspace菜单栏中，File-->Open(Ctrl+O),打开.psprj的文件

5、选中result中的delay [Failed],点击run code prove

6、在圆形图中，绿色代表目标满足，橙色代表目标未定，红色代表目标不满足，灰色代表目标不可达/死代码

图中由于模型简单，所以都是绿色的

7、也可以通过Simulink直接打开Polyspace。

simulink菜单:Cold-->Polyspace-->Open Result-->For Generated Code