while 循环多边形空间可能出现运行时错误

我正在使用嵌入式C语言，最近为整个项目运行了MathWorks Polyspace Code Proover(形式化方法静态分析)以检查关键的运行时错误。它在 While 循环中发现了一个错误(红色发现)，我正在通过内存寄存器将一些 ROM 数据复制到 RAM 中。代码工作正常，符合预期，但我想问是否有任何解决方案可以安全地删除此警告。请在下面找到代码示例：

register int32 const *source;
uint32 i=0;
uint32 *dest;
source= (int32*)&ADDR_SWR4_BEGIN;
dest = (uint32*)&ADDR_ARAM_BEGIN;
if ( source != NULL )
{
while ( i < 2048 )
{
dest[i] = (uint32)source[i];
i++;
}
}

我的猜测是ADDR_SWR4_BEGIN和ADDR_ARAM_BEGIN是在链接器脚本中定义的，而 polyspace 没有编译和链接项目，这就是为什么它抱怨可能的运行时错误或无限循环。

ADDR_SWR4_BEGIN和ADDR_ARAM_BEGIN在各自的头文件中定义为 extern。

extern uint32_t ADDR_SWR4_BEGIN;
extern uint32_t ADDR_ARAM_BEGIN;

警告为红色，确切警告如下：

Check:    Non-terminating Loop
Detail:   The Loop is infinite or contains a run-time error
Severity: Unset

任何建议将不胜感激。

代码总体上很可疑。

错误

if ( source != NULL ).您只需将此指针设置为指向地址，因此它显然不会指向 NULL。这行是多余的。
您在访问寄存器/内存时没有使用volatile，因此如果多次执行此代码，编译器可能会做出各种奇怪的假设。这可能是诊断消息的原因。

不良的样式/代码异味(应修复)

使用register关键字是可疑的。这曾经是 1980 年代的事情，当时编译器很糟糕，无法正确优化代码。如今，他们可以做到这一点，而且比程序员要好得多，因此新源代码中存在的任何register都是可疑的。
int32访问寄存器或内存位置，然后将其强制转换为无符号类型根本没有任何意义。如果数据没有签名，那么为什么首先使用签名类型。
使用自制uint32类型而不是stdint.h风格不佳。

吹毛求疵(小评论)

(int32*)演员应const合格。
循环是不必要的丑陋，可以用一个 for 循环代替：
```
for(uint32_t i=0; i<2048; i++)
{
dest[i] = source[i];
}
```

Polyspace在这里给出红色错误的原因是source和dest是指向uint32的指针。事实上，当你写：

source= (int32*)&ADDR_SWR4_BEGIN

您获取变量ADDR_SWR4_BEGIN的地址并将其分配给source。

因此，两个指针都仅指向 4 个字节的缓冲区。这样就不可能像 2048 个元素的数组那样使用这些指针。您还应该看到一个橙色复选标记，source[i]为您提供有关指针source发生的情况的信息。

似乎ADDR_SWR4_BEGIN和ADDR_SWR4_BEGIN实际上包含地址。在这种情况下，代码应该是：

source = (uint32*)ADDR_SWR4_BEGIN;
dest   = (uint32*)ADDR_ARAM_BEGIN;

如果在代码中执行此更改，红色错误将消失。

如果PolySpace不知道ADDR_ARAM_BEGIN的值，它将假定它可能是NULL(或其类型的任何其他值值)。当您显式测试source为 NULL 时，您不会对dest执行相同的操作。

由于source和dest都是从链接器常量分配的，并且在正常情况下都不应该为 NULL，因此没有必要在控制流中显式测试 NULL，最好使用assert()- PolySPace 识别断言，并将在后续分析中应用约束，但在定义NDEBUG时assert()不解决任何问题(通常在发布版本中)，因此不会施加不必要的开销：

const uint32_t* source = (const uint32_t*)&ADDR_SWR4_BEGIN ;
uint32_t* dest = (uint32_t*)&ADDR_ARAM_BEGIN;
// PolySpace constraints asserted
assert( source != NULL ) ;
assert( dest != NULL ) ;
for( int i = 0; i < 2048; i++ )
{
dest[i] = source[i] ;
}

另一种方法是为PolySpace提供"强制包含"(-include选项)以提供明确的定义，以便PolySpace不会认为所有可能的值在其分析中都是有效的。这可能还会产生加速分析的效果。

相关内容

最新更新

热门标签：