手动配置 Polyspace 多任务分析
使用 Polyspace®，您可以分析并发运行多个线程的程序。在某些情况下，Polyspace 可以自动检测代码中的线程创建和临界区。请参阅Auto-Detection of Thread Creation and Critical Section in Polyspace。
如果您的代码具有用于并发执行但系统无法自动检测到的函数，则必须在分析之前指定这些函数。如果这些函数对某个共用变量进行操作，则还必须为这些操作指定保护机制。
有关多任务代码分析工作流，请参阅Analyze Multitasking Programs in Polyspace。
指定用于多任务分析的选项
使用以下选项指定周期任务、中断以及对共享变量的保护。在 Polyspace 桌面端产品的用户界面中，相应选项位于配置窗格的多任务节点中。以下选项在 Bug Finder 和 Code Prover 分析中都可使用：
任务 (-entry-points)：指定非周期入口函数。不要指定
main。Polyspace 会隐式将main视为入口函数。临界区详细信息 (-critical-section-begin -critical-section-end)：指定开始和结束临界区的函数。时序互斥任务 (-temporal-exclusions-file)：指定时序互斥的函数组。
Polyspace 分析支持四个级别的任务优先级。也就是说，分析可以考虑这样一个事实，即某些任务不能被优先级较低的任务中断。您可以使用以下选项来指示任务优先级：
周期任务 (-cyclic-tasks)：指定按周期性间隔调度的函数。中断 (-interrupts)：指定可以异步运行的函数，例如中断处理程序或信号处理程序。-preemptable-interrupts：指定优先级低于中断但高于任务（可抢占或不可抢占）的函数。-non-preemptable-tasks：指定优先级高于任务但低于中断（可抢占或不可抢占）的函数。禁用所有中断 (-routine-disable-interrupts -routine-enable-interrupts)：指定用于禁用和重新启用中断的函数。
有关使用优先级的示例，请参阅Protections for Shared Variables in Multitasking Code。
针对 Code Prover 多任务分析改写代码
Code Prover 中的多任务分析能够更详尽地查找潜在的未受保护共享变量，因此它需要遵循严格的模式。
任务和中断必须是 void(void) 函数。
您指定为任务和中断的函数必须具有以下原型：
void func(void);
假设您希望指定一个函数 func，该函数采用 int 参量且返回类型为 int：
int func(int);
func 的包装器 void-void 函数。将此包装函数指定为任务或中断。void func_wrapper() {
volatile int arg;
(void)func(arg);
}main 函数必须结束。
Code Prover 假设 main 函数在所有任务和中断开始前结束。如果 main 函数包含无限循环或运行时错误，则系统不会分析任务和中断。如果您发现您的任务和中断中没有检查项，请查找带有红色虚线下划线的标记来查明 main 函数中的问题。请参阅Reasons for Unchecked Code。
假设您要将 main 函数指定为周期任务。
void performTask1Cycle(void);
void performTask2Cycle(void);
void main() {
while(1) {
performTask1Cycle();
}
}
void task2() {
while(1) {
performTask2Cycle();
}
}请将 main 的定义替换为：
#ifdef POLYSPACE
void main() {
}
void task1() {
while(1) {
performTask1Cycle();
}
}
#else
void main() {
while(1) {
performTask1Cycle();
}
}
#endifmain，并且如果定义了 POLYSPACE 宏，则会将 main 的内容放置到另一个函数 task1 中。使用预处理器定义 (-D) 选项定义 POLYSPACE 宏，并为任务 (-entry-points) 选项指定 task1。此假设不适用于自动检测到的线程。例如，main 函数可以使用 pthread_create 创建线程。
Polyspace 多任务分析假设任务或中断不能中断自己。
所有任务和中断都可以按任何顺序运行任意次数。
Code Prover 分析认为所有任务和中断都可以按任何顺序运行任意次数。
在下方示例中，假设您将 reset 和 inc 指定为周期任务。分析显示 var+=2 运算中有一个溢出。
void reset(void) {
var=0;
}
void inc(void) {
var+=2;
}
假设您希望对任务的调度进行建模，使 reset 在 inc 执行五次后执行。您需要编写一个实现此序列的包装函数。将此新函数指定为周期任务而不是 reset 和 inc。
void task() {
volatile int randomValue = 0;
while(randomValue) {
inc();
inc();
inc();
inc();
inc();
reset();
}
}假设您希望对任务的调度进行建模，使 reset 在 inc 执行零到五次后执行。您需要编写一个实现此序列的包装函数。将此新函数指定为周期任务而不是 reset 和 inc。
void task() {
volatile int randomValue = 0;
while(randomValue) {
if(randomValue)
inc();
if(randomValue)
inc();
if(randomValue)
inc();
if(randomValue)
inc();
if(randomValue)
inc();
reset();
}
}
