分享配置Polyspace分析C代码的方法和简介

Polyspace可以分析C、C++以及Ada代码，本文以嵌入式系统中最为常见的C代码分析为例说明Polyspace配置一个工程的过程和注意事项。

1. 配置语言和处理器类型

C语言由于其灵活性，在不同的编译器中有不同的约束和扩展，会影响最终生成的目标码的行为。Polyspace分析C代码时首先要最大程度和目标编译器的行为保持一致，这样才能保持代码分析的意义。因此在开始创建Polyspace工程时，我们需要配置编译器和处理器类型：

所选用的C语言标准：C90/C99

所用编译器类型：Keil/Tasking/Diab/IAR…

（编译器通常定义了标准C语言之外的扩展，如关键字sfr、sbit等。选定编译器类型相当于告知了Polyspace在遇到此类非标扩展时如何解释其行为。）

目标处理器类型：定义不同数据类型的大小和字节顺序类型，如mpc5xx系列处理器定义如下：

（某些运行时错误检查与此有关，如同一变量在Int定义为16位时会发生溢出，而在Int定义为32位时不会发生溢出。）

其他编译器行为设定：如负除取整方向、有符号数右移逻辑、枚举类型定义方式等。

2.选择验证分析模式

Polyspace有两种基本的验证分析模式：应用级分析和模块级分析，可以分别对应于集成测试和单元测试。

所谓应用级分析指用户待分析的源代码中包含了 main函数，选择应用级分析即分析进程从用户main函数入口，为了更好地模拟实际程序运行和调度情形，有时需要进行多任务（Multitasking）设置，有机会在以后再进一步介绍。

模块级分析通常待分析代码不包含main函数，Polyspace会自动打桩生成main函数并建立待分析函数的调用关系进行分析，并可进一步根据需要细化配置。如对于以下被调函数Function_sub和主调函数Function_top，可以设置为以下两种分析入口形式：

Function_sub(){ ……};

Function_top(){……

Function_sub();

……};

自动生成的main函数中只调用Function_top：在分析Function_top的进程中分析Function_sub，即Function_sub在Function_top的上下文中被分析。

自动生成的main函数中同时调用Function_top和Function_sub：Function_sub除了在Function_top的上下文中被分析，也会在直接在main函数上下文中被分析。对应的可能场景是Function_sub会被其他函数调用，需要更为鲁棒地分析其安全性。

— 总结 —

Polyspace的配置是一个既简单又灵活的过程，通过对编译器行为的模拟和分析模型的选择，我们可以得到更为有意义和更符合需要的结果。

往期 | 代码分析验证

Polyspace应用到软件开发和验证流程

浅谈Polyspace的静态分析