while 循环-Polyspace 可能出现运行时错误答案

【问题标题】：Possible runtime error with while loop-Polyspacewhile 循环-Polyspace 可能出现运行时错误
【发布时间】：2018-09-27 00:16:20
【问题描述】：

我正在使用嵌入式 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

任何建议将不胜感激。

【问题讨论】：

"它在 While 循环中发现了一个错误" 消息是什么？你怎么知道这是一个错误？
“无限循环或运行时错误”。没有编译器或链接器错误。
为了准确回答你，你能添加ADDR_SWR4_BEGIN和ADDR_ARAM_BEGIN的定义吗？顺便说一句，您看到的是红色检查还是橙色检查（您使用的是“警告”一词）？
@codetest ：您需要在问题中提供准确的逐字诊断，而不是在 cmets 中解释它。编辑问题，复制并粘贴诊断。
@AlexDeba 我编辑我的帖子。我希望它能让问题更清楚。

标签： memory embedded runtime-error dynamic-analysis

【解决方案1】：

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;

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

【讨论】：

你的解释很有道理。我将在下周进行更改并运行测试。谢谢你的回答:)

【解决方案2】：

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

【讨论】：

但是，请注意assert 的使用经常被编码标准禁止。在这种情况下，最好使用标准 C static_assert，因为无论如何检查都是无稽之谈和混乱。 Polyspace 是否支持标准 C？
@Lundin ：我认为你可以为 PolySpace 指定一个“自定义断言”——它不需要做任何事情，它只需要被识别为一个“保证”。例如，您可以将PSASSERT( x) 定义为空宏，但告诉 PolySpace 将其视为保证。或者您可能已经有一个可以使用的自定义断言包装器。带有虚拟定义的强制包含选项通常更可取，因为如果您根本没有断言，它不会使真实代码混乱 - 在任何情况下它也是定义虚拟断言的合适位置。

【解决方案3】：

代码总体上很可疑。

错误

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 是什么？
@Clifford 又是一个充满误报的静态分析器。一个工作工具不应该假设声明不可见，它应该需要一个项目范围的设置。虽然 OP 给人的印象是诊断来自动态分析，这更没有意义。
@Lundin：PolySpace 不是传统的静态分析器。它使用 abstract execution 来捕获您在动态分析中可能会发现的那种错误，除非通过碰巧执行错误路径来“走运”。它不仅（实际上很少）用于整个系统，而且可以用于测试部分系统。在这种情况下，它说“此代码将因未知变量或参数的某些值而失败”这是真的 - 代码本身是不安全的，而在上下文中它可能永远不会失败。工具没有坏，而是结果没有被理解。
@Lundin ：这里的问题是缺乏对工具的理解，而不是工具错误。该工具只是对与用户或您认为被询问的问题不同的问题给出答案。例如，它不执行与 -Wconversion 相同的检查。认为这是误解了该工具的作用。事实上，静态分析最好与 PolySpace 结合使用，而不是代替它。