0

我正在使用嵌入式 C 语言，最近为整个项目运行 MathWorks Polyspace Code Prover（动态分析）以检查关键的运行时错误。它在 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

任何建议，将不胜感激。

4

3 回答 3

1

代码总体上很可疑。

错误

  • 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];
}
于 2018-04-17T11:56:47.677 回答
0

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;

如果您在代码中进行此更改，红色错误就会消失。

于 2018-04-20T09:12:02.223 回答
0

如果 PolySpace 不知道该值ADDR_ARAM_BEGIN，它将假定它可能是 NULL（或其类型的任何其他值）。当您显式测试是否source为 NULL 时，您不会对dest.

由于source和dest都是从链接器常量分配的，并且在正常情况下都不应该为 NULL，因此没有必要在控制流中显式测试 NULL 并且assert()更可取 - PolySPace 识别断言，并将在后续分析中应用约束，但assert()解析为什么时候NDEBUG没有定义（通常在发布版本中），所以不会强加不必要的开销：

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 在其分析中不会考虑所有可能的值。这也可能会产生加速分析的效果。

于 2018-04-17T16:16:05.750 回答