手动配置 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);

定义一个使用 volatile 值调用 func 的包装器 void-void 函数。将此包装函数指定为任务或中断。

void func_wrapper() {
  volatile int arg;
  (void)func(arg);
}

您可以将包装函数定义连同原始函数的声明保存在一个单独的文件中，并将此文件添加到分析中。

main 函数必须结束。

Code Prover 假设 main 函数在所有任务和中断开始前结束。如果 main 函数包含无限循环或运行时错误，则系统不会分析任务和中断。如果您发现您的任务和中断中没有检查项，请查找带有红色虚线下划线的标记来查明 main 函数中的问题。请参阅Reasons for Unchecked Code (Polyspace Code Prover)。

假设您要将 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();
  } 
}
#endif

这些替换内容定义了一个空的 main，并且如果定义了 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();
   }
 }