Polyspace Code Prover 结果中未被检查的代码的原因

问题

如果程序执行流的早期出现编译错误或红色检查，Polyspace^® Code Prover™ 将不会分析程序的剩余部分。验证后，您会发现很大一部分代码未经过运行时错误检查。本主题列出了经 Code Prover 分析的代码占比偏低的各种可能原因。

例如，运行时检查仪表板上的下图显示，多达 60% 的函数未经过运行时错误检查。

可能的原因：编译错误

仅对不存在编译错误的文件进行完整分析。在包含编译错误的文件中，根据编译错误的性质，有些函数可能不会被分析：

要检查是否有一些文件未编译，请查看分析日志。有关详细信息，请参阅View Compilation Errors When Running Polyspace Static Analysis。

可能的原因：早期红色或灰色检查

靠近函数调用层次结构的起始位置存在红色或灰色检查。红色或灰色检查会导致后续代码不被检查。

如果您从未被检查的代码块中调用函数，验证也不会检查这些函数。如果靠近调用层次结构的起始位置存在红色或灰色检查，层次结构中更深层次的函数可能不会被检查。最终会导致大量代码未被检查。

例如，在以下代码中，4 个函数里只有 1 个被检查。函数 func_called_from_unreachable_1、func_called_from_unreachable_2 和 func_called_after_red 未被检查。只检查了 main。

void func_called_from_unreachable_1(void) {
}

void func_called_from_unreachable_2(void) {     
}

void func_called_after_red(void) {
}

int glob_var;

void main(void) {
     int loc_var;
     double res;
     
     glob_var=0;
     glob_var++;
     
     if (glob_var!=1) {
           func_called_from_unreachable_1();
           func_called_from_unreachable_2();
     }
     
     res=0;
     /* Division by zero occurs in for loop */
     for(loc_var=-10;loc_var<10;loc_var++) {
	          res += 1/loc_var;
     }
     
     func_called_after_red();
}

可能的原因：选项不正确

您未指定必要的分析选项。以下选项指定不正确时会导致代码不会被检查：

可能的原因：main 函数无法终止

此原因仅适用于多任务代码中整个入口函数未被检查的情况。

如果您手动配置多任务选项，则必须遵守 Polyspace 多任务模型的限制。尤其是，main 函数不能包含无限循环或运行时错误。否则，将不会检查入口函数。

例如，在此示例中，即使您将 task2 指定为入口函数，它也不会被检查。原因是 main 函数中存在无限循环。

void performTask1Cycle(void);
void performTask2Cycle(void);

void main() {
 while(1) {
    performTask1Cycle();
  } 
}

void task2() {
 while(1) {
    performTask2Cycle();
  }
}

您会看到 main 函数中的 while 关键字带有红色虚线下划线。工具提示指出该循环可能无法终止。

同样，如果发生运行时错误，导致运行时错误的函数调用会带有红色虚线下划线并附带工具提示。