Isabelle中install-C-file加载C代码时数组转指针报错的解决方法

问题原因 #

报错attempt to cause decay to pointer on array without an address出现在调用GetName(a.name)时，是因为Isabelle的Formal C parser对结构体成员数组的指针衰减处理更严格，无法自动识别栈上结构体数组成员的地址转换逻辑。

可行解决方案 #

方案1：显式传递数组首地址 #

修改PartitionInit函数中的调用语句，通过取数组首元素地址的方式显式触发指针转换：

void PartitionInit() {
    Attribute a;    
    GetName(&a.name[0]);
}

也可以用强制类型转换替代：

GetName((char*)a.name);

方案2：调整函数参数为指针类型 #

标准C中char result[32]会被隐式视为char*，但Formal C parser可能对数组形式的参数存在解析差异，直接将GetName的参数改为指针形式：

void GetName(char *result) {
    // 原有函数逻辑保持不变
}

方案3：改用静态存储的结构体变量 #

将局部结构体变量改为静态存储，让数组拥有更明确的地址标识，帮助parser识别：

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

验证效果 #

采用任一方案修改代码后，重新使用install-C-file加载即可完成解析。

内容的提问来源于stack exchange，提问作者riiiiyueeeejiiiiiiuzhao