How to verify C functions with array parameters using Isabelle

I am using Isabelle to verify a C program. During the verification process, I used the c-parser install-C-file to load the code, but the following issue occurred：

attempt to cause decay to pointer on array without an address

The c code is as follows

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);
}

The line of code that caused the error is GetName(a.name);

How can I make install-C-file load this file properly?

The error message in Isabelle is as follows.

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

Solution

The diagnostic is indeed surprising: function GetName is defined as taking a pointer to char as an argument and you are passing an array of char which decays to a pointer to its first element. No problem at all. The prototype void GetName(char result[32]) is equivalent to void GetName(char *result) and the call GetName(a.name) is equivalent to GetName(&a.name[0]).

The diagnostic wording is incorrect too: passing a.name effectively causes decay to pointer of the array a.name, but this array does have an address as a has been defined as a local object with automatic storage. The object a is instantiated by the compiler upon entering the function body and the address of a.name is the same as that of a itself. No bug there.

The array length 32 in the prototype is meaningless, it is ignored. Specifying a length in the prototype is confusing and may indicate a misconception by the programmer. C99 introduced a new syntax to specify a minimum length of the array pointed to by a pointer received as an argument, which might be what the programmer intended to convey. The syntax is

void GetName(char result[static 32])

Isabelle might be complaining about this potential confusion, but the diagnostic is incomprehensible,

You can try these modifications to see where Isabelle's confusion comes from:

try changing the prototype of GetName to
```
void GetName(char result[])
```
try changing the prototype of GetName to
```
void GetName(char *result)
```
try changing the prototype of GetName to
```
void GetName(char result[static 32])
```
which is not equivalent to the posted one but more consistent with the requirement that result point to an array of at least 32 bytes.
try intializing the Attribute object in PartitionInit:
```
Attribute a = { "" };
```