如何使用 Isabelle 验证带有数组参数的 C 函数

Question

我正在使用 Isabelle 来验证 C 程序。在验证过程中，我使用c-parser install-C-file加载代码，但是出现了以下问题：

attempt to cause decay to pointer on array without an address

c代码如下

void GetName(char result[32])
{
    static const char cv[11] = {'m','a','i','n','_','t','h','r','e','a','d'};
    long b_i;
    long i;
    for (i = 0; i < 32; i++) {
        result[i] = '\0';
    }
    i = 1;
    for (b_i = 0; b_i < 11; b_i++) {
        i = b_i + 1;
        result[b_i] = cv[b_i];
    }
    result[i] = '\0';
}

typedef struct Attribute {
    char name[32];
} Attribute;

void PartitionInit() {
    Attribute a;    
    GetName(a.name);
}

导致错误的代码行是

GetName(a.name);

如何让 install-C-file 正确加载此文件？

Isabelle 中的错误消息如下 。

1704726218: Added external decl for SetDiff with 3 args.
1704726218: Added external decl for GLOBAL Init with 0 args.
1704726218: Added external decl for GetProcessIndex with 2 args.
1704726218: Added external decl for SYS CREATE PROCESS with 4 args.
1704726218: Translating function Partition Init
/home/xxx/formal-c/Partition Init.c:43.10-43.24: Attempting to cause decay to pointer on array without an address

Answer 1

诊断确实令人惊讶：函数

GetName

被定义为将指向

char

的指针作为参数，并且您传递一个

char

数组，该数组衰减为指向其第一个元素的指针。完全没问题。原型

void GetName(char result[32])

相当于

void GetName(char *result)

，调用

GetName(a.name)

相当于

GetName(&a.name[0])

。

诊断措辞也不正确：传递

a.name

实际上会导致数组

a.name

的指针衰减，但该数组确实有一个地址，因为

a

已被定义为具有自动存储功能的本地对象。对象

a

在进入函数体时由编译器实例化，

a.name

的地址与

a

本身的地址相同。没有错误。

原型中的

array长度32

没有意义，被忽略。
在原型中指定长度会令人困惑，并且可能表明程序员存在误解。 C99 引入了一种新语法来指定作为参数接收的指针所指向的数组的最小长度，这可能是程序员想要传达的内容。语法是

void GetName(char result[static 32]) 伊莎贝尔可能会抱怨这种潜在的混乱，但诊断结果难以理解，

你可以尝试这些修改，看看伊莎贝尔的困惑从何而来：

• 尝试将

  GetName

  的原型更改为

  void GetName(char result[])
• 尝试将

  GetName

  的原型更改为

  void GetName(char *result)
• 尝试将

  GetName

  的原型更改为

  void GetName(char result[static 32]) 这并不等同于发布的，但更符合

  result

  指向至少32字节数组的要求。

• 尝试在

  Attribute

   中初始化 

  PartitionInit

   对象：

  Attribute a = { "" };