How to verify C functions with array parameters using Isabelle

Question

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

Answer 1

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 = { "" };